一句话：对基于效应处理器的 define-by-run 反向模式自动微分库，给出机器检查的正确性证明。
本文把程序验证技术用于自动微分（AD）算法的规约与验证，聚焦 define-by-run 风格：待微分程序由 AD 算法执行并监控。作者先以精确英文散文和形式化方式回答“什么是 AD 实现”以及“AD 实现正确的含义”，用类型与逻辑断言给出规约。随后针对一个具体实现进行验证，该实现涉及动态分配的可变状态、一等函数和效应处理器等微妙语言特性。作者在现代分离逻辑变体中给出机器检查的正确性证明。该工作被视为程序验证的一次高级练习，并为验证更现实的自动微分系统及利用 delimited-control effects 的软件组件提供潜在基础。
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.
@article{paperbot2189,
title = {Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library},
author = {Paulo Emílio de Vilhena and François Pottier},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:5)2023}
}