Synthesizing Backward Error Bounds, Backward
summary
Introduces a composable, general alpha-beta stability definition that covers all five primitive floating-point ops (including sqrt) and composes under program composition; formalizes proofs inside a category called Shel (shifted error lenses) so morphisms carry backward maps and error bounds; implements an automated search tool eggshel built on egglog that synthesizes backward-error bounds, handles variable reuse, proves soundness of its algorithm, and succeeds on programs previous tools could not analyze.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:26Backward stability matters
- 3:31Limitations of prior analysis
- 5:16Composable backward stability
- 9:09Category framework for proofs
- 12:41Automated analysis with Eggshell
- 15:50Evaluation and future work
- 16:14Q&A
related talks
24mBean: A Language for Backward Error Analysis
25mA Logic for the Imprecision of Abstract Interpretations
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
19mPanel: Compilation Frameworks
17mBetter Together: Unifying Datalog and Equality Saturation
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
24mA Computational Interpretation of Compact Closed Categories