# Stress-Testing Neural Network Verifiers with Provably Robust Instances

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 30 references that are in the map.
- First posted on arXiv 16 May 2026.

## Builds on (most cited first, 14 of 14)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [A Systematic Review of Robustness in Deep Learning for Computer Vision: Mind the gap?](https://mlsanity.com/paper/2112.00639/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [Robustness Verification of Polynomial Neural Networks](https://mlsanity.com/paper/2602.06105/) (2026)

## Abstract (arXiv)

Neural network verifiers aim to provide formal guarantees on model behavior, but existing verification benchmarks are fundamentally limited by their lack of ground-truth labels. As a result, verifier evaluation relies on indirect heuristics, which prevents exact scoring and systematic study of verifier failure modes. We address this gap by introducing a reusable framework for generating verification instances whose ground-truth robustness labels are known a priori through analytic construction. Our framework led to the discovery of multiple numeric tolerance concerns and an implementation bug in popular verifiers, highlighting the need for ground-truth labels. Additionally, to systematically study verifier failure modes, we introduce the verification Difficulty Profile, a collection of estimable quantities capturing distinct sources of instance hardness. Using our framework and these profiles, we evaluate five state-of-the-art verifiers and show that different instances stress distinct aspects of the verification pipeline. We show that these results can aid the future development of verifiers as they provide actionable targets for improving numerical reliability, relaxation quality, and search behavior. Our code is publicly available: https://github.com/dtroxell19/VeriStressGT.git.