Efficient CHAD
summary
Claims that Combinatory Homomorphic AD (CHAD) can be optimized to achieve the expected reverse‑mode complexity with only constant overhead, backed by an Agda formalisation and reusable artifacts. Implements sparse vectors for product derivatives and sparse maps for environment derivatives, lifts backpropagators to monadic state‑passing code to eliminate environment addition, applies closure conversion/defunctionalisation for higher‑order, and swaps sparse maps for mutable arrays to remove log factors. Paper and archive provide the proof and code.
AI-written summary · about
chapters (9)
- 0:00Efficient CHAD intro
- 1:28Reverse mode AD properties
- 3:16CHAD algorithm explained
- 6:07Time complexity challenges
- 8:17Zero and environment derivatives
- 11:05Eliminating env vector addition
- 12:29Cost models for complexity
- 14:32Limitations and future work
- 15:18Q&A
related talks
10mHomomorphic Reverse Differentiation of Iteration
23mEfficient Dual-Numbers Reverse AD via Well-Known Program Transformations
23mContextual source code AD transformations for sum types
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
29mAutomatic Differentiation via Effects and Handlers in OCaml
01h 09mLatent Effects and Handlers + Automatic Differentiation via Effects and Handlers
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
30mAutomatic Differentiation in PCF