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, with discrepancies becoming pronounced at lower-precision formats such as float16. 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）下变得显著。随后，我们建立了一个形式化的组合理论，将基于实数运算Lipschitz的敏感性边界与标准舍入误差模型下的浮点执行敏感性联系起来，并专门针对具有ReLU激活函数的前馈神经网络。我们推导出浮点执行下鲁棒性的可靠条件，包括认证退化边界和避免溢出的充分条件。我们对该理论及其主要可靠性结论进行了形式化，并基于这些原则实现了一个可执行的认证器，通过实证评估验证了其实用性。