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实现，包括动态分配可变状态、一等函数和效应处理器。我们采用分离逻辑的现代变体，给出了一个机器校验的正确性证明。我们将此结果视为程序验证领域的高级练习，其潜在应用包括验证更真实的自动微分系统，以及利用定界控制效应的其他软件组件。