Lipschitz-Based Robustness Certification Under Floating-Point Execution

TL;DR

This paper highlights the gap between real arithmetic robustness guarantees and actual floating-point execution in neural networks, proposing a Lipschitz-based theory to ensure sound robustness certification under floating-point arithmetic.

Contribution

It introduces a formal theory linking real arithmetic sensitivity bounds to floating-point execution, providing sound certification conditions and an executable certifier.

Findings

Counterexamples show robustness guarantees can fail under floating-point execution

Discrepancies are more severe at lower-precision formats like float16

The proposed certifier is practical and effective in real scenarios

Abstract

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.