Automatic Differentiation in PCF

on YouTube ↗30m

" summary

Proves that automatic differentiation on PCF with reals (higher-order, Turing-complete) is correct except on a Lebesgue-measure-zero set: forward and reverse AD compute true gradients forward and reverse mode. Builds a functorial program transformation D and shows errors lie among unstable points, characterized as a countable union of zero sets (more generally a quasi-variety) under the hypothesis that primitives form an admissible clone. Gives the ReLU-if counterexample (wrong at 0) and a constructive proof using logical predicates and an extrusion lemma.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 2:38Notation
3. 5:15Part I
4. 14:18Soundness
5. 16:44Hidden Mistake
6. 19:16Our Contribution
7. 19:45Main Result
8. 22:34Proof
9. 23:16Stable and Unstable Points
10. 25:17Proof by Contraposition
11. 26:40Proof by logical predicate
12. 27:34Literature review

" related talks

• 36mProgramming Languages for Automatic Differentiation: What Now?Damiano Mazza · LAFI 2022
• 29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...David Broman, Viktor Palmkvist, Oscar Eriksson · GPCE 2023
• 11mAbstract Interpretation for Automatic DifferentiationGagandeep Singh, Jacob Laurel, Sasa Misailovic, Siyuan Brant Qian · LAFI 2024
• 05mPartial Evaluation of Forward-Mode Automatic DifferentiationDavid Broman, Viktor Palmkvist, Oscar Eriksson · LAFI 2023
• 39mDifferentiable Functional ProgrammingNoel Welsh · Scala Days New York 2018
• 10mHomomorphic Reverse Differentiation of IterationGordon Plotkin, Matthijs I. L. Vákár, Fernando Lucatelli Nunes · LAFI 2024
• 11mPerturbation confusion in forward automatic differentiation of higher-order functionsAlexey Radul, Oleksandr Manzyuk, Barak A. Pearlmutter, David Rush, Jeffrey Mark Siskind · ICFP 2020
• 26mAdding AD to Scheme by Differentiating the InterpreterBarak A. Pearlmutter, Mehrdad Maleki · Scheme 2021