Abstract Interpretation for Automatic Differentiation
summary
Static analysis produces sound numeric bounds on derivatives computed by AD, using a synthesized abstract interpreter that encloses nonlinear patterns with a linear approximation plus a computed enclosure term D (solved via efficient nonconvex optimization heuristics). The implementation pado yields orders of magnitude tighter bounds than intervals or zonotopes on Coordinate MLP Lipschitz constants and on sensitivities through ODE solvers, avoids fixed‑point overflow bugs, and a companion domain deep J over Clark generalized Jacobians handles non‑differentiable branches. Higher‑order AD is supported by a metasemantics that preserves dependency for tight certified higher derivatives.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:48About the talk and speaker introduction
- 1:29Automatic differentiation
- 2:12Need for static analysis
- 3:37Precise analysis challenges
- 3:58Past analyzer synthesis
- 5:46PADO’s linear approximation
- 6:51Evaluating PADO on climate models
- 7:11Graphics applications work
- 7:32Non-differentiability with DeepJ
- 8:58Higher-order derivatives
- 10:01Metasemantics for higher derivatives
- 10:23Conclusion
related talks
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
26mAdding AD to Scheme by Differentiating the Interpreter
36mProgramming Languages for Automatic Differentiation: What Now?
17mSynthesizing Precise Static Analyzers for Automatic Differentiation
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
14mNominal Semantics for First-class Automatic Differentiation
05mPartial Evaluation of Forward-Mode Automatic Differentiation
30mAutomatic Differentiation in PCF