Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation

Reference. Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation

Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, Andrew Fitzgibbon · POPL · 2022 · differentiable-programming · PDF · DOI · pldb

In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument.

Cite

Cite as @krawiec-2022-provably (helia, typst) · \cite{krawiec-2022-provably} (LaTeX)

BibTeX

bibtex · 1 line

@article{krawiec-2022-provably, title={Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation}, volume={6}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3498710}, DOI={10.1145/3498710}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Krawiec, Faustyna and Peyton Jones, Simon and Krishnaswami, Neel and Ellis, Tom and Eisenberg, Richard A. and Fitzgibbon, Andrew}, year={2022}, month=Jan, pages={1–30} }

hayagriva YAML (typst)

yaml · 22 lines

krawiec-2022-provably:
  type: article
  title: Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
  author:
  - Krawiec, Faustyna
  - Peyton Jones, Simon
  - Krishnaswami, Neel
  - Ellis, Tom
  - Eisenberg, Richard A.
  - Fitzgibbon, Andrew
  date: 2022-01
  page-range: 1-30
  url: http://dx.doi.org/10.1145/3498710
  serial-number:
    doi: 10.1145/3498710
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 6

Download: krawiec-2022-provably.bib · krawiec-2022-provably.yml

Cites 21 works (0 here)

External (21)

Automatic differentiation in PCF (2021)
λS: computable semantics for differentiable programming with higher-order functions and datatypes (2021)
Reverse AD at Higher Types: Pure, Principled and Denotationally Correct (2021)
ad: Automatic Differentiation (Haskell package) (2021)
Backpropagation in the simply typed lambda-calculus with linear negation (2020)
Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing (2020)
A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation (2020)
A simple differentiable programming language (2020)
Demystifying differentiable programming: shift/reset the penultimate backpropagator (2019)
The simple essence of automatic differentiation (2018)
The enriched effect calculus: syntax and semantics (2012)
Beautiful Differentiation (2009)
Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation (second ed.) (2008)
Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator (2008)
Automatic Differentiation, C++ Templates, and Photogrammetry (2004)
Automatic Differentiation of Algorithms: From Simulation to Optimization (2002)
Functional Differentiation of Computer Programs (1998)
Definitional Interpreters for Higher-Order Programming Languages (1998)
A new characterization of lambda definability (1993)
Notions of Computation and Monads (1991)
A simple automatic derivative evaluation program (1964)