论文标题
通过差异和分类粘合的自动分化的正确性
Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing
论文作者
论文摘要
我们提供自动分化（AD）的语义正确性证明。我们在具有代数数据类型的高阶语言上考虑一种前向模式AD方法，我们将其表征为保留宏观的独特结构，可以选择基本操作的衍生物。我们根据差异空间来描述用于可区分编程的丰富语义。我们证明它可以解释我们的语言，并且我们表达了广告方法对此语义的正确意义的含义。我们表明，我们对AD的特征产生了基于差异空间的粘合结构的优雅语义证明其正确性。从本质上讲，我们解释了这是一种逻辑关系论点。最后，我们通过考虑一种基于持续的方法来概述分析如何扩展到其他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. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.
