Recent work has shown that forward- and reverse- mode automatic differentiation (AD) over the reals is almost always correct in a mathematically precise sense. However, actual programs work with machine-representable numbers (e.g., floating-point numbers), not reals. In this paper, we study the correctness of AD when the parameter space of a neural network consists solely of machine-representable numbers. In particular, we analyze two sets of parameters on which AD can be incorrect: the incorrect set on which the network is differentiable but AD does not compute its derivative, and the non-differentiable set on which the network is non-differentiable. For a neural network with bias parameters, we first prove that the incorrect set is always empty. We then prove a tight bound on the size of the non-differentiable set, which is linear in the number of non-differentiabilities in activation functions, and give a simple necessary and sufficient condition for a parameter to be in this set. We further prove that AD always computes a Clarke subderivative even on the non-differentiable set. We also extend these results to neural networks possibly without bias parameters.

翻译：近期研究表明，在实数域上，前向与反向模式自动微分在数学精确定义下几乎总是正确的。然而，实际程序处理的是机器可表示数（如浮点数）而非实数。本文研究了参数空间仅由机器可表示数构成的神经网络中自动微分的正确性。具体而言，我们分析了自动微分可能出错的两类参数集：网络可微但自动微分未计算其导数的错误集，以及网络不可微的非可微集。对于含偏置参数的神经网络，我们首先证明错误集始终为空，随后给出非可微集大小的紧界（该界与激活函数中不可微点数量呈线性关系），并给出参数属于该集的简洁充要条件。我们进一步证明，即使在非可微集上，自动微分仍能计算Clarke次导数。最后，我们将这些结论推广至可能不含偏置参数的神经网络。