Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic
summary
Claims a source to source transformation that produces dual numbers then generalizes to multi dual numbers and a compact symbolic delta representation evaluated in place, preserving sharing by naming subdeltas so evaluation never duplicates work. The pipeline yields a two pass evaluator whose runtime and memory are linear in the original program, supports higher order functions, comes with a Kripke logical relations proof of correctness, and an implementation that matches prior functional reverse approaches though not tuned to large ML frameworks.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 3:02Forward mode AD
- 7:56Reverse mode AD
- 10:29Optimizing gradients
- 13:53Symbolic vectors
- 16:45Preserving sharing
- 19:02Efficiency and correctness
- 20:47Conclusion
- 21:08Q&A
related talks
23mEfficient Dual-Numbers Reverse AD via Well-Known Program Transformations
36mProgramming Languages for Automatic Differentiation: What Now?
25mYou Only Linearize Once: Tangents Transpose to Gradients
05mPartial Evaluation of Forward-Mode Automatic Differentiation
23mContextual source code AD transformations for sum types
29mReverse Automatic Differentiation for Accelerate (Extended Abstract)
29mParallelism-preserving automatic differentiation for second-order array languages
34mDifferentiable Functional Programming