一句话：证明 PCF（含实数的高阶图灵完备语言）中前向与反向自动微分在温和假设下几乎处处正确。
论文研究高阶、图灵完备且含实数的语言 PCF 中自动微分（AD）的正确性，涵盖前向与反向模式。作者不假设程序处处可微，而是在对基本函数施加温和假设后，通过语义分析证明 AD 几乎处处正确：AD 计算的导数或梯度仅可能在一组 Lebesgue 测度为零的输入上失败，因此随机取到错误输入的概率为零。结果还更精确地刻画失败点集；例如当基本函数仅为常数、加法和乘法时，AD 失败点包含在一列多项式零点集的并集之中。该工作表明 AD 虽非绝对正确，但在测度意义下对一大类高阶程序可靠。
We study the correctness of automatic differentiation (AD) in the context of a higher-order, Turing-complete language (PCF with real numbers), both in forward and reverse mode. Our main result is that, under mild hypotheses on the primitive functions included in the language, AD is almost everywhere correct, that is, it computes the derivative or gradient of the program under consideration except for a set of Lebesgue measure zero. Stated otherwise, there are inputs on which AD is incorrect, but the probability of randomly choosing one such input is zero. Our result is in fact more precise, in that the set of failure points admits a more explicit description: for example, in case the primitive functions are just constants, addition and multiplication, the set of points where AD fails is contained in a countable union of zero sets of polynomials.