# Exploiting Verified Neural Networks via Floating Point Numerical Error

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

## Key facts

- Cited by 35 papers in the map (data through 7 Oct 2026).
- First posted on arXiv 6 Mar 2020.

## Built on by (most cited first, 30 of 35)

- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)
- [Hardware and Software Platform Inference](https://mlsanity.com/paper/2411.05197/) (2024)
- [Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers](https://mlsanity.com/paper/2202.05207/) (2022)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks](https://mlsanity.com/paper/2506.01054/) (2025)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables](https://mlsanity.com/paper/2208.08609/) (2022)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [TorchLean: Formalizing Neural Networks in Lean](https://mlsanity.com/paper/2602.22631/) (2026)
- [A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks](https://mlsanity.com/paper/2203.07078/) (2022)
- [CheckINN: Wide Range Neural Network Verification in Imandra (Extended)](https://mlsanity.com/paper/2207.10562/) (2022)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Sound Randomized Smoothing in Floating-Point Arithmetics](https://mlsanity.com/paper/2207.07209/) (2022)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)
- [Hardware-Triggered Backdoors](https://mlsanity.com/paper/2601.21902/) (2026)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks](https://mlsanity.com/paper/2510.16028/) (2025)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [FloatDoor: Platform-Triggered Backdoors in LLMs](https://mlsanity.com/paper/2606.19535/) (2026)
- [A Domain-Theoretic Framework for Robustness Analysis of Neural Networks](https://mlsanity.com/paper/2203.00295/) (2022)
- [SysNoise: Exploring and Benchmarking Training-Deployment System Inconsistency](https://mlsanity.com/paper/2307.00280/) (2023)
- [On the Extreme Variance of Certified Local Robustness Across Model Seeds](https://mlsanity.com/paper/2601.13303/) (2026)

## Abstract (arXiv)

Researchers have developed neural network verification algorithms motivated by the need to characterize the robustness of deep neural networks. The verifiers aspire to answer whether a neural network guarantees certain properties with respect to all inputs in a space. However, many verifiers inaccurately model floating point arithmetic but do not thoroughly discuss the consequences. We show that the negligence of floating point error leads to unsound verification that can be systematically exploited in practice. For a pretrained neural network, we present a method that efficiently searches inputs as witnesses for the incorrectness of robustness claims made by a complete verifier. We also present a method to construct neural network architectures and weights that induce wrong results of an incomplete verifier. Our results highlight that, to achieve practically reliable verification of neural networks, any verification system must accurately (or conservatively) model the effects of any floating point computations in the network inference or verification system.