一句话：提出 Bean 语言及带分级 coeffect 与严格线性的类型系统，静态推导浮点程序后向误差界，并用范畴语义证明可靠性。
后向误差分析可在浮点舍入误差存在时评估数值程序的质量，但现有数值分析技术通常依赖大量人工推导，尚缺乏可靠的自动化静态后向误差界推导工具。本文提出 Bean：一种带类型的一阶编程语言，用于表达后向误差的定量界。Bean 的类型系统结合分级 coeffect 系统与严格线性，以可靠地追踪后向误差在程序中的流动。作者通过一种新的范畴语义证明系统可靠性，其中每个 Bean 程序都表示一组满足后向误差保证的相关变换。为验证其实用性，作者用 Bean 实现多种数值线性代数标准算法，以组合式风格通过类型建立细粒度后向误差界；同时开发原型实现来自动推断后向误差界。评估表明，推断出的界与文献中最坏情况理论相对后向误差界一致，说明 Bean 有助于验证数值程序的关键性质：数值稳定性。
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 .
@article{paperbot3089,
title = {Bean: A Language for Backward Error Analysis},
author = {Ariel E. Kellison and Laura Zielinski and David Bindel and Justin Hsu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729324}
}