论文标题
PCF的自动差异化
Automatic Differentiation in PCF
论文作者
论文摘要
我们在高阶，图灵完整语言（具有实数的PCF）的背景下研究自动分化（AD）的正确性，无论是在正向和反向模式下。我们的主要结果是，在语言中包含的原始功能的轻度假设下，AD几乎无处不在，即它计算所考虑的程序的派生或梯度，除了一组Lebesgue Measure Measure Zero。否则说，在某些输入中，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 non-identically-zero polynomials.
