Research map / Label-efficient and robust learning / Noisy labels
Stress-Testing Neural Network Verifiers with Provably Robust Instances
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces VeriStress-GT, a framework of analytically constructed neural network verification instances with known robustness labels and a Difficulty Profile of hardness estimators, and uses it to stress-test five verifiers, uncovering numerical tolerance issues and an implementation bug.
Problem
Neural network verifier benchmarks lack ground-truth robustness labels and offer little diagnostic characterization of instance difficulty, so verifier evaluation relies on heuristics (majority voting, assuming soundness) and cannot systematically stress-test failure modes.
Approach
Generate verification instances via analytic constructors (MILP exact radius, constant-on-box embedding, MEAP, input-corner, paired-bias CNN, contractive CNN, attention, polynomial networks) whose robustness is provably known, with difficulty knobs, and profile each instance with five estimable quantities (sampled minimum margin, IBP relative gap, unstable fraction, local-region complexity, effect
Key results
- Five state-of-the-art verifiers evaluated on 225 VeriStress-GT instances plus MNIST_fc and oval21; multiple verifiers return false SAT claims on provably robust instances at 0.999 times the exact radius, largely attributed to numerical tolerance.
- A bug in a popular verifier's handling of disjunctive output constraints led to false UNSAT claims on provably non-robust MILP instances; reported to and fixed by developers.
- In MNIST_fc, final 16 instances have G_IBP >= 2x10^5, several orders of magnitude above other instances, suggesting interval relaxation looseness as the dominant obstruction.
Surprising findings
- Several verifiers return false SAT claims on analytically robust instances, largely due to numerical tolerance issues.
- A verifier implementation bug caused false UNSAT claims on provably non-robust instances.
Limitations
- Verifiers tested with a limited number of repeated seeds due to computational cost.
- Difficulty profiles are not the sole predictors of verifier runtime.
- Constructors currently cover only fully connected, CNN, attention, and polynomial architectures (no residual or GNN).
Experimental setup
Datasets: MNIST CIFAR
Benchmarks: VeriStress-GT MNIST_fc oval21
Metrics: correct results over total instances runtime timeouts difficulty profile correlations
Baselines: alpha-beta-CROWN
Builds on: alpha-beta-CROWN Interval Bound Propagation VNN-COMP benchmarks
Closest papers by meaning
- VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.87)
- Dynamic Algorithm Termination for Branch-and-Bound-based Neural Network Verification (AAAI 2025 · similarity 0.85)
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.85)
- No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks (ICML 2025 · similarity 0.85)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.85)
- SURE: SUrvey REcipes for building reliable and robust deep networks (CVPR 2024 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.