Abstract: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: this https URL.
| Subjects: | Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Optimization and Control (math.OC) |
| MSC classes: | Primary 68Q60, Secondary 68T07, 65G20, 90C11, 90C25, 90C57 |
| ACM classes: | D.2.4; F.3.1; I.2.6 |
| Cite as: | arXiv:2605.17153 [cs.LG] |
| (or arXiv:2605.17153v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2605.17153 arXiv-issued DOI via DataCite (pending registration) |
From: David Troxell [view email]
[v1]
Sat, 16 May 2026 20:56:52 UTC (2,875 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。