Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.17153 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911691701223424 |
|---|---|
| author | Troxell, David Alexandr, Yulia Hunt, Sofia Lei, Stephanie Montúfar, Guido |
| author_facet | Troxell, David Alexandr, Yulia Hunt, Sofia Lei, Stephanie Montúfar, Guido |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_17153 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Stress-Testing Neural Network Verifiers with Provably Robust Instances Troxell, David Alexandr, Yulia Hunt, Sofia Lei, Stephanie Montúfar, Guido Machine Learning Logic in Computer Science Optimization and Control Primary 68Q60, Secondary 68T07, 65G20, 90C11, 90C25, 90C57 D.2.4; F.3.1; I.2.6 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. |
| title | Stress-Testing Neural Network Verifiers with Provably Robust Instances |
| topic | Machine Learning Logic in Computer Science Optimization and Control Primary 68Q60, Secondary 68T07, 65G20, 90C11, 90C25, 90C57 D.2.4; F.3.1; I.2.6 |
| url | https://arxiv.org/abs/2605.17153 |