Recent work has shown that automatic differentiation 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 automatic differentiation when the parameter space of a neural network consists solely of machine-representable numbers. For a neural network with bias parameters, we prove that automatic differentiation is correct at all parameters where the network is differentiable. In contrast, it is incorrect at all parameters where the network is non-differentiable, since it never informs non-differentiability. To better understand this non-differentiable set of parameters, we prove a tight bound on its size, which is linear in the number of non-differentiabilities in activation functions, and provide a simple necessary and sufficient condition for a parameter to be in this set. We further prove that automatic differentiation always computes a Clarke subderivative, even on the non-differentiable set. We also extend these results to neural networks possibly without bias parameters.

翻译：近期研究表明，实数域上的自动微分在精确数学意义上几乎总是正确的。然而实际程序处理的是机器可表示数（如浮点数）而非实数。本文研究了当神经网络参数空间仅包含机器可表示数时自动微分的正确性。对于带偏置参数的神经网络，我们证明了在所有网络可微的参数点上自动微分均正确；相反，在所有网络不可微的参数点上自动微分均不正确——因其从未报告不可微性。为深入理解该不可微参数集，我们证明了其规模的紧界（与激活函数中不可微点数量呈线性关系），并给出了参数属于该集合的简洁充要条件。进一步证明，即使在不可微集上，自动微分始终能计算Clarke次导数。我们还将这些结论推广至可能不含偏置参数的神经网络。