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.

翻译：我们应用程序验证技术来解决自动微分算法的规约与验证问题。聚焦于定义时运行这一自动微分风格——即待微分程序在执行过程中由自动微分算法进行监控。首先提出两个核心问题："自动微分实现是什么？"以及"自动微分实现正确性的含义是什么？"我们分别以精确的英文散文体在非形式化层面，以及利用类型与逻辑断言在形式化层面作答。在解答这些一般性问题后，我们聚焦于一个涉及多项精妙编程语言特性的自动微分实现，包括动态分配的可变状态、一等函数及效应处理器。我们给出了基于分离逻辑现代变体的机器检查正确性证明。将此结果视为程序验证领域的高级实践，其潜在应用前景包括验证更具现实性的自动微分系统，以及利用限定控制效应的其他软件组件。