Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
Paulo Emílio de Vilhena, François Pottier
TL;DR
The paper develops a formal verification framework for define-by-run automatic differentiation by treating a minimal AD library as a pure interface diff : exp -> exp operating on a tagless-final representation of expressions. It provides a precise informal and formal specification within a Separation Logic setting and demonstrates that multiple implementations (forward-mode, stack-based reverse-mode, and an effect-handler-based reverse-mode) satisfy the specification. The main contribution is a machine-checked proof of correctness for the effect-based reverse-mode AD, using a core calculus HH with the Hazel logic to manage first-class functions, mutable state, and delimited control. The work showcases how compositional, logic-based verification can certify sophisticated AD components and suggests a path toward verifying realistic AD systems and other delimited-control-based software. It also connects to broader literature on effect handlers, program verification, and AD semantics, illustrating how a concise specification can guide correctness proofs across diverse implementation strategies.
Abstract
We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored by the automatic differentiation algorithm. We begin by asking, "what is an implementation of AD?" and "what does it mean for an implementation of AD to be correct?" We answer these questions both at an informal level, in precise English prose, and at a formal level, using types and logical assertions. After answering these broad questions, we focus on a specific implementation of AD, which involves a number of subtle programming-language features, including dynamically allocated mutable state, first-class functions, and effect handlers. We present a machine-checked proof, expressed in a modern variant of Separation Logic, of its correctness. We view this result as an advanced exercise in program verification, with potential future applications to the verification of more realistic automatic differentiation systems and of other software components that exploit delimited-control effects.