Automatic Differentiation in PCF

Abstract

We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of non-identically-zero polynomials.

References in corpus (5)

• TensorFlow: A system for large-scale machine learning
• A Simple Differentiable Programming Language
• Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
• Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
• LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable Models

Cited by in corpus (11)

• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
• Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
• Higher Order Automatic Differentiation of Higher Order Functions
• CHAD for Expressive Total Languages
• Combinatory Adjoints and Differentiation
• Automatic Differentiation for ML-family languages: correctness via logical relations
• A Language for Evaluating Derivatives of Functionals Using Automatic Differentiation
• Using Rewrite Strategies for Efficient Functional Automatic Differentiation
• From Identity to Difference: A Quantitative Interpretation of the Identity Type
• Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages
• Scrutinizing Variables for Checkpoint Using Automatic Differentiation