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.

翻译：我们运用程序验证技术来解决自动微分（AD）算法的规约与验证问题。聚焦于"定义即运行"（define-by-run）这一AD风格——即需要被微分的程序由自动微分算法执行并监控。我们首先提出两个问题："什么是AD的实现？"以及"AD实现正确的含义是什么？"通过精确的英文散文描述和形式化方法（运用类型与逻辑断言），我们在非正式与正式两个层面回答了这些问题。在解决这些宽泛问题后，我们聚焦于一个特定的AD实现，该实现涉及多项精妙的编程语言特性，包括动态分配的可变状态、一阶函数及效应处理器。我们采用现代分离逻辑变体，给出了经机器检验的正确性证明。我们视此成果为程序验证领域的高级实践范例，其未来可应用于更真实的自动微分系统验证，以及利用受限控制效应的其他软件组件的验证。