# Floating-Point Neural Network Verification at the Software Level

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 95 references that are in the map.
- First posted on arXiv 27 Oct 2025.

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

- [Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift](https://mlsanity.com/paper/1502.03167/) (2015)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Generalized Out-of-Distribution Detection: A Survey](https://mlsanity.com/paper/2110.11334/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Evasion Attacks against Machine Learning at Test Time](https://mlsanity.com/paper/1708.06131/) (2017)
- [How Does Batch Normalization Help Optimization?](https://mlsanity.com/paper/1805.11604/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Activation Functions: Comparison of trends in Practice and Research for Deep Learning](https://mlsanity.com/paper/1811.03378/) (2018)
- [Fast Algorithms for Convolutional Neural Networks](https://mlsanity.com/paper/1509.09308/) (2015)
- [The Fallacy of AI Functionality](https://mlsanity.com/paper/2206.09511/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [International AI Safety Report](https://mlsanity.com/paper/2501.17805/) (2025)
- [A Unified Algebraic Perspective on Lipschitz Neural Networks](https://mlsanity.com/paper/2303.03169/) (2023)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [CAPE: Encoding Relative Positions with Continuous Augmented Positional Embeddings](https://mlsanity.com/paper/2106.03143/) (2021)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Machine Learning for Microcontroller-Class Hardware: A Review](https://mlsanity.com/paper/2205.14550/) (2022)
- [Impacts of floating-point non-associativity on reproducibility for HPC and deep learning applications](https://mlsanity.com/paper/2408.05148/) (2024)
- [Red Teaming Deep Neural Networks with Feature Synthesis Tools](https://mlsanity.com/paper/2302.10894/) (2023)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Towards Efficient Verification of Quantized Neural Networks](https://mlsanity.com/paper/2312.12679/) (2023)

## Built on by (most cited first, 2 of 2)

- [On the Extreme Variance of Certified Local Robustness Across Model Seeds](https://mlsanity.com/paper/2601.13303/) (2026)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)

## Abstract (arXiv)

The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques cannot certify the absence of faults at the software level. In this paper, we show how to specify and verify that neural networks are safe, by explicitly reasoning about their floating-point implementation. In doing so, we construct NeuroCodeBench 2.0, a benchmark comprising 912 neural network verification examples that cover activation functions, common layers, and full neural networks of up to 170K parameters. Our verification suite is written in plain C and is compatible with the format of the International Competition on Software Verification (SV-COMP). Thanks to it, we can conduct the first rigorous evaluation of eight state-of-the-art software verifiers on neural network code. The results show that existing automated verification tools can correctly solve an average of 11% of our benchmark, while producing around 3% incorrect verdicts. At the same time, a historical analysis reveals that the release of our benchmark has already had a significantly positive impact on the latter.