Technical Summary: Stress-Testing Neural Network Verifiers with Provably Robust Instances

Problem Statement

Neural network verifiers are designed to provide formal guarantees on model behavior, specifically certifying that a trained model behaves robustly under bounded input perturbations. However, the evaluation of these verifiers is fundamentally limited by the lack of ground-truth labels in existing benchmarks. Without knowing a priori whether a verification instance is truly robust or non-robust, evaluation relies on indirect heuristics, such as majority voting among verifiers or assuming soundness when no counterexample is found. This approach prevents exact scoring, obscures specific failure modes, and makes it difficult to systematically stress-test verifiers on increasingly difficult instances. Furthermore, current benchmarks offer limited diagnostic information regarding why a verifier fails (e.g., due to loose relaxations, complex local geometry, or numerical issues).

Methodology

The authors introduce VeriStress-GT (Verifier Stress-Testing via Ground Truth), a modular framework for generating neural network verification instances with analytically proven ground-truth robustness labels. Unlike traditional benchmarks that rely on training models on datasets, VeriStress-GT constructs instances where robustness is guaranteed by mathematical construction.

1. Robust Constructions

The framework defines a collection of "constructors," each targeting specific architectural classes or verifier bottlenecks. These constructors generate instances where the ground-truth label is known a priori:

• ReLU Network Constructors:
  • Exact-Radius via MILP: Computes the exact robustness radius using Mixed-Integer Linear Programming to create near-boundary robust instances.
  • Constant-on-Box Embedding: Constructs networks where an intermediate latent layer is constant over the perturbation set, ensuring robustness regardless of downstream complexity.
  • Mutually Exclusive Activation Patterns (MEAP): Creates pairs of neurons that are individually unstable (switching between active/inactive) but coupled such that at least one is always active, forcing verifiers to handle complex activation pattern dependencies.
  • Input-Corner Stress: Generates instances where robustness relies on the convexity of the margin function, requiring verification at the corners of the perturbation box rather than through local relaxations.
• CNN Constructors:
  • Deep Contractive CNN: Forces perturbations to contract through depth using Lipschitz-constrained convolutional blocks.
  • Paired-Bias CNN: A convolutional analogue to MEAP, where paired channels share filters but have ordered biases, ensuring a non-negative difference despite individual instability.
• Attention Module Constructors:
  • Fixed-Ordering Softmax Attention: Certifies robustness by ensuring the score ordering of attention heads remains stable under perturbation.
  • Dominant-Key Linear Attention: Enforces a dominant key in linear attention mechanisms, bounding the drift of the attention output.
• Polynomial Network Constructor: Generates instances by explicitly controlling the geometry of the decision boundary (a real algebraic hypersurface) and placing the input near this boundary with a known buffer.

2. Verification Instance Difficulty Profile

To systematically analyze verifier performance, the authors propose the Difficulty Profile, a tuple of five estimable quantities characterizing instance hardness independent of any specific verifier:

1. Minimum Margin ($\hat{M}_{min}$): An empirical estimate of the proximity to a counterexample via sampling.
2. IBP Relative Gap ($G_{IBP}$): Measures the looseness of Interval Bound Propagation (IBP) relative to the empirical margin.
3. Unstable Fraction ($U$): The fraction of nonlinear units whose activation state is ambiguous over the input set.
4. Local-Region Complexity ($A_\tau$): Estimates the number of distinct local affine behaviors (or Taylor approximations) required to cover the margin landscape over the perturbation set.
5. Effective Gradient Dimensionality ($d_{eff}$): Measures how distributed the margin sensitivity is across input coordinates (related to the Participation Ratio).

Key Contributions

1. VeriStress-GT Framework: The first reusable framework for generating neural network verification instances with verifier-independent ground-truth labels and controllable difficulty parameters.
2. Difficulty Profile: A unified framework for characterizing verification instance hardness, enabling the systematic evaluation of verifier scalability and failure modes beyond simple runtime metrics.
3. Empirical Evaluation: A comprehensive evaluation of five state-of-the-art verifiers (including $\alpha,\beta$-CROWN, Marabou, NeuralSAT, PyRAT, and nnenum) using the new framework.

Results

The evaluation of five state-of-the-art verifiers on 225 VeriStress-GT instances and external benchmarks (MNIST_fc, oval21) yielded three primary findings:

1. Revelation of Incorrect Claims: Ground-truth labels exposed that multiple verifiers returned false robustness claims (SAT) on instances that were analytically robust (UNSAT). These errors were largely attributed to numerical tolerance limitations. Furthermore, testing with provably non-robust instances revealed a specific implementation bug in a popular verifier regarding disjunctive output constraints, which was subsequently fixed.
2. Diagnosable Timeouts: The Difficulty Profile transformed opaque timeout outcomes into diagnosable failure modes. For example, high $G_{IBP}$ values correlated with failures due to extreme interval-relaxation looseness, while high $d_{eff}$ values correlated with timeouts in high-dimensional margin sensitivity scenarios.
3. Targeted Stress-Testing: Different constructors isolated distinct failure modes. MEAP instances stressed branching decisions and activation-pattern ambiguity, while Input-Corner instances isolated relaxation looseness from nonlinear-region complexity. This allows developers to target specific improvements (e.g., tighter relaxations vs. better branching heuristics).

Significance and Claims

The paper claims to reframe verification benchmarking from heuristic evaluation to controlled, ground-truth experimentation. By providing instances with known labels, the framework:

• Enables the detection of implementation bugs and numerical instabilities that are otherwise masked by consensus-based evaluation.
• Provides actionable targets for improving specific aspects of the verification pipeline, such as numerical reliability, relaxation quality, and search behavior.
• Offers a systematic way to study verifier failure modes by correlating specific difficulty profile components with verifier performance.

The authors emphasize that while the framework exposes limitations in current verifiers, it also serves as a tool for guiding future development toward more robust and reliable verification systems. The code and datasets are publicly available to facilitate this ongoing research.