一句话：提出高阶反向模式自动微分的简单高效实现，并证明其正确性与渐近复杂度。
本文研究反向模式自动微分（AD）的高阶扩展与正确性保证。现有实现难以同时兼顾高阶函数与渐近效率，且缺乏形式化正确性证明。作者给出一种反向模式 AD 的翻译方案及实现，使其可自然扩展到高阶函数，并保持运行时间与内存消耗与原程序运行时间呈线性。论文不仅形式化描述了该翻译，还实现了算法，并通过逻辑关系论证证明其正确性。结果表明，该算法在可证明正确的同时具备渐近高效的特性，为高阶 AD 提供了坚实的语义与实现基础。
In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument.
@article{paperbot1581,
title = {Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation},
author = {Faustyna Krawiec and Simon Peyton Jones and Neel Krishnaswami and Tom Ellis and Richard A. Eisenberg and Andrew Fitzgibbon},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498710}
}