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.

翻译：神经网络验证器旨在为模型行为提供形式化保证，但现有验证基准因缺乏真值标签而存在根本局限性。因此，验证器评估依赖于间接启发式方法，这阻碍了精确评分和验证器失效模式的系统性研究。我们通过引入可复用框架来弥补这一空白，该框架通过解析构造生成已知真值稳健性标签的验证实例。该框架使我们发现多个主流验证器存在数值容差问题及实现缺陷，凸显了真值标签的必要性。此外，为系统性研究验证器失效模式，我们提出验证难度剖面——一组可估计的量化指标，用于捕捉实例难度的不同来源。基于该框架与剖面，我们评估了五种最先进的验证器，表明不同实例会对验证管线的不同方面施加压力。研究结果表明，这些成果通过提供数值可靠性、松弛质量及搜索行为优化的可行目标，可助力验证器的未来发展。我们的代码已公开：https://github.com/dtroxell19/VeriStressGT.git。