Synthesizing Precise Static Analyzers for Automatic Differentiation
summary
Pasado synthesizes precise static analyzers that directly abstract the Chain Rule, Product Rule and Quotient Rule in automatic differentiation, producing a single composite abstract transformer (intervals and zonotopes; forward and reverse modes) and proving soundness. It solves a constrained optimization via Hessian analysis to get tight zonotope-style linear bounds, then applies to neural nets and ODE solvers. Results show Pasado yields up to 2750× more precise local Lipschitz bounds and 1.31–2.81× tighter sensitivity bounds for DE and financial models, with sound and reusable artifacts.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:25Research background
- 1:52Why AD static analysis
- 2:55Abstract interpretation of derivatives
- 4:19Core calculus rules in AD
- 5:43Naive domains for nonlinear ops
- 6:44PADO’s linear approximation
- 8:08PADO’s soundness guarantees
- 9:13Climate model sensitivity case
- 10:55Neural network robustness evaluation
- 12:40Deep network monotonicity
- 14:25Conclusion
- 14:49Q&A
related talks
11mAbstract Interpretation for Automatic Differentiation
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
05mPartial Evaluation of Forward-Mode Automatic Differentiation
36mProgramming Languages for Automatic Differentiation: What Now?
15mCoarsening Optimization for Differentiable Programming
29mParallelism-preserving automatic differentiation for second-order array languages
27mA Dual Number Abstraction for Static Analysis of Clarke Jacobians
01h 09mLatent Effects and Handlers + Automatic Differentiation via Effects and Handlers