Research map / Learning theory and algorithms / Combinatorial and search optimization
Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification
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.
Proposes Clip-and-Verify, a linear-constraint-driven domain clipping framework (complete and relaxed clipping, GPU-based) that tightens intermediate bounds and prunes BaB subproblems in NN verifiers such as α,β-CROWN.
Problem
Neural network verification with branch-and-bound is costly because loose intermediate bounds cause exponential subproblem growth, and existing verifiers do not efficiently tighten intermediate-layer bounds.
Approach
Reuse linear constraints produced by bound propagation (split constraints and output constraints) to (1) shrink the input box in closed form (relaxed clipping) and (2) directly optimize per-neuron intermediate bounds via a 1D dual/coordinate-ascent solver (complete clipping), avoiding external LP solvers.
Key results
- On lsnc, complete clipping reduces BaB subproblems by 96.3% (142M to 5.3M) with the same 40 verified instances.
- On acasxu, relaxed clipping with reorder reduces subproblems by 64.2% and time to 150.25s versus 280.51s for alpha,beta-CROWN.
- On cartpole, complete clipping cuts subproblems by 95.5% and time to 142s from 1602s; Quadrotor-2D becomes verifiable (78,818s) where baseline times out.
- Clip-and-Verify with BICCOS reaches 131 and 144 verified on cifar100-2024 and tinyimagenet-2024 style benchmarks, according to the paper's summary.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add relaxed clipping to α,β-CROWN | α,β-CROWN · lsnc | subproblems: 142,293,985 -> 92,402,227 | Helped |
| add complete clipping to α,β-CROWN | α,β-CROWN · lsnc | subproblems: 142,293,985 -> 5,334,421 | Helped |
| add reordering to relaxed clipping (ablation) | Clip-and-Verify · lsnc | subproblems: 92,402,227 -> 66,412,652 | Helped |
| add reordering to relaxed clipping (ablation) | Clip-and-Verify · acasxu | subproblems: 3,124,100 -> 2,557,715 | Helped |
| add reordering to relaxed clipping (ablation) | Clip-and-Verify · nn4sys | subproblems: 2,691,750 -> 2,300,894 | Helped |
| use complete clipping instead of relaxed clipping (ablation) | Clip-and-Verify · nn4sys | time(s): 1193.89 -> 2846.06 | Hurt |
| use complete clipping instead of relaxed clipping (ablation) | Clip-and-Verify · cartpole | subproblems: 16,453,971 -> 2,438,359 | Helped |
| add Clip-and-Verify to β-CROWN | β-CROWN · oval22 | verified properties: 20 -> 22 | Helped |
| add Clip-and-Verify to BICCOS | BICCOS · cifar10-resnet | verified properties: 63 -> 64 | Helped |
| add Clip-and-Verify to β-CROWN | β-CROWN · cifar100-2024 | verified properties: 119 -> 126 | Helped |
| add Clip-and-Verify to BICCOS | BICCOS · tinyimagenet-2024 | verified properties: 138 -> 144 | Helped |
| add Clip-and-Verify to β-CROWN | β-CROWN · vision-transformer 2024 | verified accuracy: 59.0 -> 61.0 | Helped |
Surprising findings
- Complete clipping was slower than relaxed clipping on nn4sys (2846s vs 1193s) despite fewer or similar subproblems.
- An LP solver (Gurobi) with a 10-iteration limit was reported to be over 880x slower than the GPU coordinate ascent per round.
Limitations
- Complete clipping can be slower in wall-clock time than relaxed clipping on some benchmarks (nn4sys).
- Relaxed clipping is looser since it relaxes the feasible region to an axis-aligned box.
- Critical-neuron selection for complete clipping is a heuristic (top-k by BaBSR score) and not guaranteed optimal.
Experimental setup
Datasets: VNN-COMP benchmarks (acasxu, lsnc, nn4sys, oval22, cifar10-resnet, cifar100-2024, tinyimagenet-2024, vit-2024) MNIST CIFAR-10 control system benchmarks (cartpole, Quadrotor-2D)
Benchmarks: acasxu lsnc nn4sys oval22 cifar10-resnet cifar100-2024 tinyimagenet-2024 vit-2024 cartpole Quadrotor-2D MNIST CIFAR-10 CNN
Metrics: number of BaB subproblems time (s) verified accuracy number of verified properties
Baselines: alpha,beta-CROWN BICCOS GCP-CROWN Marabou PyRAT nnenum NNV Cora NeuralSAT ERAN OVAL VeriNet
Builds on: CROWN alpha-CROWN beta-CROWN BaBSR
Closest papers by meaning
- Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (NeurIPS 2024 · similarity 0.91)
- SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming (ICML 2025 · similarity 0.90)
- Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification (NeurIPS 2021 · similarity 0.90)
- Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification (AAAI 2025 · similarity 0.89)
- DeepBern-Nets: Taming the Complexity of Certifying Neural Networks Using Bernstein Polynomial Activations and Precise Bound Propagation (AAAI 2024 · similarity 0.87)
- Dynamic Algorithm Termination for Branch-and-Bound-based Neural Network Verification (AAAI 2025 · similarity 0.86)
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.