Higher Order Automatic Differentiation of Higher Order Functions
arXiv:2101.06757 · doi:10.46298/lmcs-18(1:41)2022
Abstract
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher-order language with algebraic data types and we characterise it as the unique structure-preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming based on diffeological spaces. We show that it interprets our language and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is in essence a logical relations argument. Throughout we show how the analysis extends to AD methods for computing higher-order derivatives using a Taylor approximation.
arXiv admin note: substantial text overlap with arXiv:2001.02209
References in corpus (15)
- Adam: A Method for Stochastic Optimization
- TensorFlow: A system for large-scale machine learning
- The Stan Math Library: Reverse-Mode Automatic Differentiation in C++
- Tangent spaces and tangent bundles for diffeological spaces
- A Simple Differentiable Programming Language
- Automatic Differentiation in PCF
- Automatic differentiation in ML: Where we are and where we should be going
- Comparative Smootheology
- A Geometric Theory of Higher-Order Automatic Differentiation
- On the Principles of Differentiable Quantum Programming Languages
- A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
- Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
- CHAD for Expressive Total Languages
- Differentiating a Tensor Language
- Four explicit formulas for the prolongations of an infinitesimal Lie symmetry and multivariate Faa di Bruno formulas