Thu 19 Jan 2023 15:10 - 15:35 at Grand Ballroom A - Automatic Differentiation Chair(s): Ningning Xie

Automatic differentiation (AD) is conventionally understood as a family of distinct algorithms, rooted in two “modes”—forward and reverse—which are typically presented (and implemented) separately. Can there be only one? Following up on the AD systems developed in the JAX and Dex projects, we formalize a decomposition of reverse-mode AD into (i) forward-mode AD followed by (ii) unzipping the linear and non-linear parts and then (iii) transposition of the linear part.

To that end, we define a (substructurally) linear type system that can prove a class of functions are (algebraically) linear. Our main results are that forward-mode AD produces such linear functions, and that we can unzip and transpose any such linear function, conserving cost, size, and linearity. Composing these three transformations recovers reverse-mode AD. This decomposition also sheds light on checkpointing, which emerges naturally from a free choice in unzipping let expressions. As a corollary, checkpointing techniques are applicable to general-purpose partial evaluation, not just AD.

We hope that our formalization will lead to a deeper understanding of automatic differentiation and that it will simplify implementations, by separating the concerns of differentiation proper from the concerns of gaining efficiency (namely, separating the derivative computation from the act of running it backward).

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:10 - 16:25
Automatic DifferentiationPOPL at Grand Ballroom A
Chair(s): Ningning Xie University of Toronto
15:10
25m
Talk
You Only Linearize Once: Tangents Transpose to Gradients
POPL
Alexey Radul Google Research, Adam Paszke Google Research, Roy Frostig Google Research, Matthew J. Johnson Google Research, Dougal Maclaurin Google Research
DOI
15:35
25m
Talk
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
POPL
Tom Smeding Utrecht University, Matthijs Vákár Utrecht University
DOI Pre-print
16:00
25m
Talk
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsDistinguished Paper
POPL
Alexander K. Lew Massachusetts Institute of Technology, Mathieu Huot University of Oxford, Sam Staton University of Oxford, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI Pre-print