Sensitivity-based robustness certification has emerged as a practical approach for certifying neural network robustness, including in settings that require verifiable guarantees. A key advantage of these methods is that certification is performed by concrete numerical computation (rather than symbolic reasoning) and scales efficiently with network size. However, as with the vast majority of prior work on robustness certification and verification, the soundness of these methods is typically proved with respect to a semantic model that assumes exact real arithmetic. In reality deployed neural network implementations execute using floating-point arithmetic. This mismatch creates a semantic gap between certified robustness properties and the behaviour of the executed system. As motivating evidence, we exhibit concrete counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers. Discrepancies become pronounced at lower-precision formats such as float16, and under adversarially constructed models reach semantically meaningful perturbation radii at float32. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to the sensitivity of floating-point execution under standard rounding-error models, specialised to feed-forward neural networks with ReLU activations. We derive sound conditions for robustness under floating-point execution, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We formalize the theory and its main soundness results, and implement an executable certifier based on these principles, which we empirically evaluate to demonstrate its practicality.

翻译：基于灵敏度的鲁棒性认证已成为认证神经网络鲁棒性的一种实用方法，尤其是在需要可验证保证的场景中。这类方法的关键优势在于，认证通过具体数值计算（而非符号推理）完成，且随网络规模高效扩展。然而，与先前绝大多数鲁棒性认证和验证工作类似，这些方法的完备性通常是在假设精确实数运算的语义模型下证明的。现实中部署的神经网络实现使用浮点算术运行。这种不匹配造成了认证鲁棒性属性与执行系统行为之间的语义鸿沟。作为动机性证据，我们展示了具体反例，证明实数算术鲁棒性保证在浮点执行下可能失效——即使对于先前已验证的认证器也是如此。差异性在低精度格式（如float16）下变得显著，且在对抗性构造的模型中，对float32格式的语义有效扰动半径也会产生偏离。随后，我们发展了一套形式化的组合理论，将基于Lipschitz的实数算术灵敏度界与标准舍入误差模型下浮点执行的灵敏度相关联，专门针对具有ReLU激活函数的前馈神经网络。我们推导了浮点执行下鲁棒性的充分条件，包括证书退化边界以及无溢出的充分条件。我们形式化了该理论及其主要完备性结果，并基于这些原理实现了一个可执行的认证器，通过实验评估证明了其实用性。