提出可生成带真实鲁棒性标签的测试用例，用于精准评估神经网络验证器。
Stress-Testing Neural Network Verifiers with Provably Robust Instances
- 通过解析构造法生成已知鲁棒性标签的验证实例。
- 发现多个验证器存在数值容差问题和实现缺陷。
- 提供可量化难度的验证难题分析框架，助力改进验证器设计。
神经网络验证器旨在为模型行为提供形式化保证，但现有验证基准因缺乏真实标签而受到根本限制。因此，验证器评估依赖间接启发式方法，无法实现精确评分和系统性故障模式分析。本文提出一种可复用的框架，能够通过解析构造生成具有先验已知鲁棒性标签的验证实例。该框架揭示了多个主流验证器中的数值容差问题及实现错误，凸显了真实标签的重要性。此外，我们引入验证难度轮廓（Verification Difficulty Profile），一组可估算的量，用于捕捉不同实例难度来源。基于此框架与轮廓，我们评估了五种先进验证器，发现不同实例会分别对验证流程的不同环节构成压力。这些结果有助于未来验证器开发，为提升数值可靠性、松弛质量与搜索行为提供了可操作目标。代码已公开：https://github.com/dtroxell19/VeriStressGT.git。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。