Bean: A Language for Backward Error Analysis

TL;DR

Bean addresses the challenge of statically deriving sound backward error bounds for floating-point programs by introducing a typed first-order language that combines graded coeffects with strict linearity. A novel category of backward error lenses (Bel) provides a semantic foundation, and a main soundness theorem connects typing to concrete backward-error guarantees. The authors implement an OCaml prototype that automatically infers per-variable backward error and demonstrate competitive results against worst-case theory and forward-error tools on standard numerical benchmarks. The work demonstrates a compositional, scalable approach to ensuring backward stability in numerical programs, with potential for broader adoption in automated numerical analysis.

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.

Figures (8)

• Figure 1: An illustration of backward error. The function $\tilde{f}$ represents a floating-point implementation of the function $f$. Given the points $\tilde{x} \in \mathbb{R}^n$ and $x \in \mathbb{F}^n \subset \mathbb{R}^n$ such that $\tilde{f}(x) = f(\tilde{x})$, the backward error is the distance $\delta x$ between $x$ and $\tilde{x}$.
• Figure 2: Grammar for $\textsc{Bean}{}$ types and terms.
• Figure 3: Typing rules with $q,r,r_1,r_2 \in \mathbb{R}^{\ge0}$ and fixed parameter $\varepsilon \in \mathbb{R}^{>0}$.
• Figure 4: The backward map $b$ for the composition ${{(f_2,\tilde{f}_2,b_2) \circ (f_1,\tilde{f}_1,b_1)}}$.
• Figure 5: Full typing rules for $\Lambda_S$.

Theorems & Definitions (26)

• Definition 2.1
• Remark 1: Linearity and Completeness
• Theorem 3.1: Backward Error Soundness
• Remark 2: Conditionals and Backward Error
• Theorem 5.1: Algorithmic Soundness
• Theorem 5.2: Algorithmic Completeness
• Definition 5.1: Relative Componentwise Condition Number
• Definition 6.1: Backward Error Lenses
• Definition 6.2
• Theorem 6.1: Backward Error Soundness