Synthesizing Precise Static Analyzers for Automatic Differentiation

Explore a groundbreaking technique for synthesizing precise static analyzers for Automatic Differentiation in this 17-minute conference talk from OOPSLA2 2023. Discover Pasado, an innovative approach that automatically constructs specialized static analyzers for Chain Rule, Product Rule, and Quotient Rule computations in AD. Learn how this method abstracts nonlinear operations simultaneously, resulting in significant precision improvements over prior works. Delve into the soundness proofs and versatility of the approach, which can be applied to different nonlinear functions, abstract domains, and both forward-mode and reverse-mode AD. Examine multiple case studies showcasing Pasado's effectiveness, including computing bounds on neural network Lipschitz constants, bounding financial model sensitivities, certifying monotonicity, and analyzing differential equations in climate science and chemistry. Compare the precision gains achieved by Pasado, with examples of up to 2750× improvement in CNN analysis and 1.31-2.81× enhancement in sensitivity bounds for various applications.