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方法, 我们把它描述为一种独特的结构, 通过选择基本操作的衍生物来保护宏观。 我们描述一个丰富的基于 difflogist 空间的不同编程语义学。 我们用它来解释我们的语言, 我们用它来表达对于这个语义来说AD方法的正确性的含义。 我们用它来说明我们的AD方法对于这个语义学的正确性。 我们证明我们的AD的特性产生了一个优雅的语义学证明, 证明它是正确的, 其基于在 difflogicutical 空间上加插根的构造。 我们解释这在本质上是一个逻辑关系论证。 我们从总体上讲, 我们展示了分析是如何扩大到使用 Taylor 近似法计算更高顺序衍生物的AD方法。