Bean: A Language for Backward Error Analysis

TL;DR

Bean is a new typed programming language that automatically derives sound backward error bounds for numerical programs, aiding in the validation of their numerical stability with minimal human effort.

Contribution

We introduce Bean, a typed language with a novel categorical semantics that enables automatic, sound derivation of backward error bounds for numerical algorithms.

Findings

Bean's type system accurately infers backward error bounds.

The inferred bounds match worst-case theoretical bounds.

Bean demonstrates practical utility in validating numerical stability.

Abstract

Backward error analysis offers a method for assessing the quality of numerical programs in the presence of floating-point rounding errors. However, techniques from the numerical analysis literature for quantifying backward error require substantial human effort, and there are currently no tools or automated methods for statically deriving sound backward error bounds. To address this gap, we propose Bean, a typed first-order programming language designed to express quantitative bounds on backward error. Bean's type system combines a graded coeffect system with strict linearity to soundly track the flow of backward error through programs. We prove the soundness of our system using a novel categorical semantics, where every Bean program denotes a triple of related transformations that together satisfy a backward error guarantee. To illustrate Bean's potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in Bean, establishing fine-grained backward error bounds via typing in a compositional style. We also develop a prototype implementation of Bean that infers backward error bounds automatically. Our evaluation shows that these inferred bounds match worst-case theoretical relative backward error bounds from the literature, underscoring Bean's utility in validating a key property of numerical programs: numerical stability.