一句话：为高阶语言中的前向模式自动微分建立基于 diffeological spaces 的语义正确性证明，并扩展到高阶导数。
本文研究高阶语言中自动微分（AD）的语义正确性。作者考虑带代数数据类型的高阶语言上的前向模式 AD，将其刻画为在给定基本运算导数后唯一保持结构的宏。为可微编程，他们基于 diffeological spaces 给出丰富语义，证明该语义可解释此语言，并明确 AD 相对该语义正确的含义。核心结果是通过 diffeological spaces 上的粘合构造给出优雅的语义正确性证明，本质上是一种逻辑关系论证。作者还说明该分析如何扩展到使用 Taylor 近似计算高阶导数的 AD 方法。
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Throughout, we show how the analysis extends to AD methods for computing higher order derivatives using a Taylor approximation.
@article{paperbot1713,
title = {Higher Order Automatic Differentiation of Higher Order Functions},
author = {Mathieu Huot and Sam Staton and Matthijs Vákár},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:41)2022}
}