A Simple Differentiable Programming Language

Abstract

Automatic differentiation plays a prominent role in scientific computing and in modern machine learning, often in the context of powerful programming systems. The relation of the various embodiments of automatic differentiation to the mathematical notion of derivative is not always entirely clear---discrepancies can arise, sometimes inadvertently. In order to study automatic differentiation in such programming contexts, we define a small but expressive programming language that includes a construct for reverse-mode differentiation. We give operational and denotational semantics for this language. The operational semantics employs popular implementation techniques, while the denotational semantics employs notions of differentiation familiar from real analysis. We establish that these semantics coincide.

In POPL2020

References in corpus (11)

• PyTorch: An Imperative Style, High-Performance Deep Learning Library
• TensorFlow: A system for large-scale machine learning
• Deep Learning with Differential Privacy
• Dynamic Control Flow in Large-Scale Machine Learning
• TensorFlow Eager: A Multi-Stage, Python-Embedded DSL for Machine Learning
• Developing Bug-Free Machine Learning Systems With Formal Mathematics
• Differential restriction categories
• Pycobra: A Python Toolbox for Ensemble Learning and Visualisation
• Tangent: Automatic differentiation using source-code transformation for dynamically typed array programming
• Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
• Tricks from Deep Learning

Cited by in corpus (18)

• Automatic Differentiation in PCF
• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
• Smoothing Methods for Automatic Differentiation Across Conditional Branches
• On the Principles of Differentiable Quantum Programming Languages
• Differentiable Physics: A Position Piece
• A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation
• Higher Order Automatic Differentiation of Higher Order Functions
• CHAD for Expressive Total Languages
• Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
• Learning Stable Galerkin Models of Turbulence with Differentiable Programming
• Smart Choices and the Selection Monad
• Opening the Blackbox: Accelerating Neural Differential Equations by Regularizing Internal Solver Heuristics
• Categorical semantics of a simple differential programming language
• Automatic Differentiation for ML-family languages: correctness via logical relations
• Cartesian Differential Kleisli Categories
• A Language for Evaluating Derivatives of Functionals Using Automatic Differentiation
• Type-driven Neural Programming by Example
• Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages