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.

翻译：本文给出了自动微分（AD）的语义正确性证明。我们考虑了一种带代数数据类型的高阶语言上的前向模式AD方法，并将其刻画为在基本运算的导数选择下唯一保持结构的宏。我们基于微分几何空间建立了一种可微编程的丰富语义，证明了该语义可解释我们的语言，并阐述了AD方法相对于该语义正确的含义。通过微分几何空间上的胶合构造，我们证明了AD的刻画可自然导出其正确性的优雅语义证明，并阐明这本质上是逻辑关系论证。我们始终展示了该分析如何扩展到利用泰勒近似计算高阶导数的AD方法。