# Lipschitz-Based Robustness Certification Under Floating-Point Execution

arXiv: https://arxiv.org/abs/2603.13334 · HTML: https://mlsanity.com/paper/2603.13334/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 32 of its 62 references that are in the map.
- First posted on arXiv 6 Mar 2026.

## Builds on (most cited first, 30 of 32)

- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [DeepFool: a simple and accurate method to fool deep neural networks](https://mlsanity.com/paper/1511.04599/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Regularisation of Neural Networks by Enforcing Lipschitz Continuity](https://mlsanity.com/paper/1804.04368/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Adversarial Robustness Toolbox v1.0.0](https://mlsanity.com/paper/1807.01069/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Efficient Bound of Lipschitz Constant for Convolutional Layers by Gram Iteration](https://mlsanity.com/paper/2305.16173/) (2023)
- [Harnessing Neuron Stability to Improve DNN Verification](https://mlsanity.com/paper/2401.14412/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [Tight and Efficient Upper Bound on Spectral Norm of Convolutional Layers](https://mlsanity.com/paper/2409.11859/) (2024)
- [Set-Based Training for Neural Network Verification](https://mlsanity.com/paper/2401.14961/) (2024)
- [Mixed precision accumulation for neural network inference guided by componentwise forward error analysis](https://mlsanity.com/paper/2503.15568/) (2025)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks](https://mlsanity.com/paper/2506.01054/) (2025)
- [Getting a-Round Guarantees: Floating-Point Attacks on Certified Robustness](https://mlsanity.com/paper/2205.10159/) (2022)
- [QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2111.13110/) (2021)
- [Spectral Norm of Convolutional Layers with Circular and Zero Paddings](https://mlsanity.com/paper/2402.00240/) (2024)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)

## Abstract (arXiv)

Lipschitz-based robustness certification bounds a network's sensitivity through concrete numerical computation rather than symbolic reasoning, and so scales efficiently. It is increasingly used even where verifiable guarantees matter. Yet, as with most prior work on robustness certification and verification, soundness is typically proved against a semantic model assuming exact real arithmetic. Deployed networks instead execute in floating-point, creating a gap between certified properties and executed behaviour. As motivating evidence, we give counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to floating-point execution under standard rounding-error models for feed-forward ReLU networks. We derive sound conditions for floating-point robustness, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We also give an efficient floating-point Gram iteration algorithm for Lipschitz bounds and prove that it never under-estimates the true norm. Separately, when a model is certified pre-deployment, we show how measuring its actual deviation against a high-precision execution can substantially reduce certificate degradation. We formalise the theory and its soundness, and implement an executable certifier, evaluated across dense networks spanning image, tabular, and many-class classification. To our knowledge, ours is the first method for soundly accounting for floating-point effects in Lipschitz-based robustness certification, and, done efficiently, the first floating-point-sound robustness checking procedure of any kind to certify models' entire test set -- seven those with 500,000 examples -- while retaining enough precision to be practical.