Nominal Semantics for First-class Automatic Differentiation

on YouTube ↗14m

" summary

Formalizes the popular tagged forward-mode AD (used in JAX, Julia, early PyTorch) as a meaning-preserving compiler from a simply typed lambda calculus with first-class differentiation to a target language with runtime name generation, models names in a nominal/Shulman-style topos, and proves correctness by logical relations: compiled programs return the same real values and those results are independent of generated tags, eliminating perturbation confusion for R→R programs.

AI-written summary · about

" chapters (7)

1. 0:00Introduction
2. 0:42First-class automatic differentiation
3. 2:07Dual numbers and perturbation
4. 5:18Tagged forward mode algorithm
5. 6:43Correctness of the algorithm
6. 11:45Correctness theorem and proof
7. 12:26Summary and Q&A

" related talks

• 36mProgramming Languages for Automatic Differentiation: What Now?Damiano Mazza · LAFI 2022
• 11mAbstract Interpretation for Automatic DifferentiationGagandeep Singh, Jacob Laurel, Sasa Misailovic, Siyuan Brant Qian · LAFI 2024
• 39mDifferentiable Functional ProgrammingNoel Welsh · Scala Days New York 2018
• 05mPartial Evaluation of Forward-Mode Automatic DifferentiationDavid Broman, Viktor Palmkvist, Oscar Eriksson · LAFI 2023
• 26mAdding AD to Scheme by Differentiating the InterpreterBarak A. Pearlmutter, Mehrdad Maleki · Scheme 2021
• 29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...David Broman, Viktor Palmkvist, Oscar Eriksson · GPCE 2023
• 11mPerturbation confusion in forward automatic differentiation of higher-order functionsAlexey Radul, Oleksandr Manzyuk, Barak A. Pearlmutter, David Rush, Jeffrey Mark Siskind · ICFP 2020
• 06mDistribution Theoretic Semantics for Non-Smooth Differentiable ProgrammingChristopher Lam · LAFI 2023