一句话：揭示反向传播与 Gödel Dialectica 解释的意外联系，并连接到微分 λ 演算与微分线性逻辑。
自动微分研究如何高效计算微分；其中反向传播算法因神经网络而广受关注。本文揭示反向传播与 Gödel 的 Dialectica 解释之间存在出人意料的联系：Dialectica 是一种实现半经典公理的逻辑翻译。作者在不同逻辑框架中利用这一对应，证明 Dialectica 的计算解释可以翻译到微分 λ 演算，并说明微分线性逻辑（Differential Linear Logic）包含了 Dialectica 的逻辑解释。该工作为反向传播与自动微分提供了新的逻辑与演算基础，连接了证明论、线性逻辑与微分演算。摘要未报告实现或实验评估。
Automatic Differentiation is the study of the efficient computation of differentials. While the first automatic differentiation algorithms are concomitant with the birth of computer science, the specific backpropagation algorithm has been brought to a modern light by its application to neural networks. This work unveils a surprising connection between backpropagation and Gödel's Dialectica interpretation, a logical translation that realizes semi-classical axioms. This unexpected correspondence is exploited through different logical settings. In particular, we show that the computational interpretation of Dialectica translates to the differential λ-calculus and that Differential Linear Logic subsumes the logical interpretation of Dialectica.