Stress-Testing Neural Network Verifiers with Provably Robust Instances

TL;DR

This paper introduces a framework for generating neural network verification instances with known ground-truth labels, enabling systematic stress-testing and analysis of verifier failure modes.

Contribution

It provides a reusable method for creating verification benchmarks with ground-truth labels and a new difficulty profile to analyze verifier robustness.

Findings

Discovered numeric tolerance issues in popular verifiers.

Identified an implementation bug affecting verifier accuracy.

Different instances stress different aspects of verification pipelines.

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: https://github.com/dtroxell19/VeriStressGT.git.