Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing
Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing
复制标题
DOI：
10.1007/978-3-030-45231-5_17
复制
发表时间：
2020-04-17
期刊：
影响因子：
--
通讯作者：
Vákár M
中科院分区：
文献类型：
--
作者：
Huot M;Staton S;Vákár M
我们提出了自动微分（AD）的语义正确性证明。我们考虑一个高阶语言的代数数据类型的前向模式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.
登录
查看更多内容
影响因子：
1.8
作者：
Brunel, Alois;Mazza, Damiano;Pagani, Michele
通讯作者：
Pagani, Michele
影响因子：
2.7
作者：
LIU, DC;NOCEDAL, J
通讯作者：
NOCEDAL, J
DOI：
10.1007/978-3-030-45231-5_17
发表时间：
2020-04-17
期刊：
Foundations of Software Science and Computation Structures
影响因子：
--
作者：
Huot M;Staton S;Vákár M
通讯作者：
Vákár M
DOI：
10.1090/s0002-9947-2011-05107-x
发表时间：
2011-11-01
影响因子：
1.3
作者：
Baez, John C.;Hoffnung, Alexander E.
通讯作者：
Hoffnung, Alexander E.
影响因子：
1.1
作者：
Ehrhard, T;Regnier, L
通讯作者：
Regnier, L