Stress-Testing Neural Network Verifiers with Provably Robust Instances
This work provides a principled evaluation methodology for neural network verifiers, addressing the lack of ground-truth benchmarks that has hindered systematic testing and improvement of verification tools.
The authors introduce a framework to generate neural network verification instances with known ground-truth robustness labels, enabling exact scoring of verifiers. Using this framework, they discovered numeric tolerance issues and a bug in popular verifiers, and evaluated five state-of-the-art verifiers to identify distinct failure modes.
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.