PCF 中的自动微分
计算机科学中的逻辑
2021-01-13 v3
摘要
我们在高阶、图灵完备语言（带实数的 PCF）的语境下研究自动微分（AD）的正确性，包括前向模式与反向模式。我们的主要结果是，在语言所包含的原始函数满足温和假设的条件下，AD 几乎处处正确，即它计算出所考虑程序的导数或梯度，除了一组勒贝格测度为零的集合之外。换言之，存在 AD 不正确的输入，但随机选取到这样一个输入的概率为零。我们的结果事实上更为精确，因为失败点集容许更明确的描述：例如，在原始函数仅为常数、加法和乘法的情况下，AD 失败的点集包含于非零多项式零集的可数并之中。
引用
@article{arxiv.2011.03335,
title = {Automatic Differentiation in PCF},
author = {Damiano Mazza and Michele Pagani},
journal= {arXiv preprint arXiv:2011.03335},
year = {2021}
}