Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification

AI summary

Overview

Research area: Formal verification of neural networks — specifically, accelerating branch-and-bound (BaB)–based verifiers using linear-programming duality and GPU-parallel computation.

Technical level: Advanced. The paper assumes familiarity with bound propagation (CROWN), convex relaxations, Lagrangian duality, and branch-and-bound search. The high-level ideas are accessible, but the algorithms rest on nontrivial optimization theory (piecewise-linear concave duality, coordinate ascent, knapsack equivalence).

One-sentence scope: The paper introduces a "clipping" framework that uses linear constraints produced essentially free by bound propagation to tighten intermediate neuron bounds and shrink input domains, dramatically reducing the number of branch-and-bound subproblems a verifier must explore.

What This Paper Is About

Neural network verifiers prove that a network behaves safely (e.g., no misclassification under small input perturbations) by relaxing the non-convex verification problem into tractable convex bounds, then splitting the problem into many subproblems via branch-and-bound when a single relaxation is too loose. The bottleneck is that intermediate-layer bounds are computed once at the start and never refreshed, so loose bounds force deep branching and explosive runtime. This paper asks: can we cheaply tighten those intermediate bounds and prune input regions at every branch-and-bound node, using only the linear constraints the verifier already computes?

Key Contributions

1. A general linear constraint-driven clipping framework that reformulates bound tightening at any layer as either direct optimization over neurons (Complete Clipping) or indirect optimization over the input box (Relaxed Clipping), without external solvers.

2. Complete Clipping: a coordinate-ascent algorithm built on a theorem showing that tightening one affine bound under one linear constraint reduces to a 1D concave, piecewise-linear maximization over a single Lagrange multiplier — solvable exactly via breakpoints in O(n log n), and shown equivalent to a continuous knapsack problem. With multiple constraints, coordinate ascent over the dual variables yields near-LP-quality bounds on a GPU.

3. Relaxed Clipping: a closed-form, O(n)-per-constraint procedure that computes the tightest axis-aligned box containing the feasible region induced by each linear constraint, then re-concretizes cached intermediate bounds over the shrunk box. It is component-wise tight and requires no iteration.

4. Integration into both Input BaB and Activation BaB within α,β-CROWN, with a clever reordering (clip after splitting so children inherit parent constraints), a top-k neuron selection heuristic based on BaBSR intercept scores, and a priori infeasibility detection that can mark subproblems verified without further work.

Main Findings

• Up to 96% fewer BaB subproblems. On the lsnc benchmark, Complete Clipping reduced subproblems from 142.3M to 5.3M (96.3% reduction) and cut total verification time from 115.3s to 84.3s. On acasxu, the reduction was 78.6%; on cartpole, 95.5% (1602s → 142s).

• Complete Clipping turns unsolvable problems into solved ones. On Quadrotor-2D, the baseline α,β-CROWN timed out, relaxed clipping also timed out, but complete clipping verified the benchmark in ~79,000s with 1.1B subproblems. On Quad-2D-Large, only complete clipping finished at all.

• Relaxed Clipping is often the fastest practical option. Because it is O(n) per constraint and parallelizable, it delivers large subproblem reductions (39–70%) at low overhead, and in some benchmarks (e.g., nn4sys, cartpole) it gives the best wall-clock time rather than the best subproblem count.

• Reorder-then-clip is consistently beneficial. Applying relaxed clipping after splitting so child domains inherit parent constraints reduced both runtime and subproblems in every tested case.

• GPU coordinate ascent beats commercial LP solvers by ~880×. Against Gurobi's dual simplex with a 10-iteration cap, the authors' GPU-parallelized solver ran in 0.0028s vs. 2.47s per round, with comparable bound accuracy (0.00085 vs. 0.0007 mean error).

• The approach generalizes beyond ReLU. Activation-space linear constraints are derived generically, enabling application to Vision Transformer benchmarks (oval22, cifar10-resnet, cifar100-2024, tinyimagenet-2024).

• Infeasibility is detected cheaply. Contradictory constraint combinations (e.g., conflicting ReLU assignments) are identified a priori and treated as verified, avoiding wasted branching.

Methodology in Plain English

The starting observation: When a verifier computes bounds on a neuron, it produces an affine expression — something like "this neuron's value is at least a·x + c for any input x in the current box." These linear pieces are usually thrown away after computing a number. The authors noticed that each such piece is itself a constraint that can be reused to eliminate parts of the input domain or to re-derive tighter bounds elsewhere in the network.

Complete Clipping (direct). To tighten a neuron's bound using a constraint, you'd normally solve a linear program. The authors instead take the Lagrangian dual: for a box domain, the inner minimization over the input can be done in closed form for any fixed Lagrange multiplier, leaving a one-dimensional concave function to maximize. Because that function is piecewise linear, its maximum lies exactly at a "breakpoint" where some coefficient flips sign — findable by sorting. With many constraints, they optimize one multiplier at a time (coordinate ascent), each step reusing the same breakpoint machinery. The whole thing is a sequence of sorts and cumulative sums, which maps naturally onto GPU parallelism.

Relaxed Clipping (indirect). Rather than optimizing each neuron separately, shrink the shared input box so that it hugs the feasible region defined by the constraints. For a single linear constraint, the tightest enclosing axis-aligned box has a closed form: move each face in as far as the constraint allows. Applying this to many constraints in parallel and taking the intersection gives a smaller box; all cached affine bounds are then re-evaluated over the smaller box, tightening the entire network at once.

Wiring it into the verifier. In input BaB, every unverified subdomain leaves behind a final-layer bound that splits the input into "verified" and "needs work" regions; the latter becomes a constraint passed to the children after the split. In activation BaB, choosing a ReLU to be active or inactive implies a linear constraint on the input (via the neuron's affine over-approximation), and these constraints accumulate along the search path. In both cases, relaxed clipping is applied broadly and cheaply, while complete clipping targets a heuristically chosen top-k set of high-impact unstable neurons.

Why This Matters

Research impact. The paper challenges a long-standing design tradeoff in neural network verification — that updating intermediate bounds is too expensive to be worthwhile. By decoupling the tighten-then-branch ordering and exploiting duality tailored to box domains, it shows that bound refinement at every node can be both sound and cheap. The equivalence to continuous knapsack gives a clean theoretical handle, and the framework's activation-agnostic formulation opens the door to verifiers for architectures beyond piecewise-linear networks.

Real-world applications:

• Autonomous vehicles and drones: Verifying that a learned controller never issues a dangerous command inside a specified operating envelope (the quadrotor, cartpole, and nn4sys benchmarks are exactly this).
• Aircraft collision avoidance: Certified safety of neural advisory systems (the acasxu benchmark from the ACAS Xu program).
• Medical and industrial control: Formally guaranteeing safety properties of learned controllers before deployment in settings where certification is mandated.
• Robustness auditing of classifiers: Proving that image classifiers cannot be fooled by bounded pixel perturbations, relevant to security-sensitive deployments and regulatory review of ML systems.

Industry relevance. Verifiers are used by certification bodies and safety-critical ML teams, but their runtime has been a practical barrier to adoption. Reducing subproblem counts by an order of magnitude — and solving benchmarks that previously timed out — meaningfully changes the size of networks that can be certified within a reasonable compute budget. The implementation is already part of α,β-CROWN, the winner of the 2025 Verification of Neural Networks Competition, and the code is publicly released.

Future Directions

1. Beyond boxes. Both algorithms assume hyper-rectangular input domains. Extending the clipping framework to general polytopes or to layered (non-box) relaxations could capture tighter feasible regions at the cost of polyhedral operations.

2. Better neuron selection heuristics. Complete Clipping is applied only to a top-k subset chosen by BaBSR intercept scores. Whether learning-based or cost-aware selection could further improve the quality-versus-runtime tradeoff is open.

3. Scaling to larger architectures. Experiments cover Vision Transformers and moderate CNNs; whether the approach remains effective for very deep networks or large language-model-scale verification is untested.

4. Tighter LP-quality solutions. The coordinate ascent is only near-optimal for multiple constraints, and there is an order dependency in which constraint is updated first. Characterizing that dependency and closing the gap to exact LP solutions without losing GPU efficiency is a natural next step.

Target Audience

This paper is aimed at researchers and engineers working on formal verification of neural networks, adversarial robustness certification, or the intersection of convex optimization and deep learning. It will be most valuable to practitioners who build or extend branch-and-bound verifiers (or use α,β-CROWN and want to understand its internals), to optimization researchers interested in dual decomposition applied at GPU scale, and to graduate students entering the neural network verification field who want a concrete example of how duality, bound propagation, and search interact. Readers without a background in convex relaxation and branch-and-bound will find the motivation and results accessible, but the algorithmic sections require comfort with Lagrangian duality and piecewise-linear analysis.

Authors’ abstract

State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties. In this work, we introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers. Under this framework, we develop two novel algorithms that efficiently utilize linear constraints to 1) reduce portions of the input space that are either verified or irrelevant to a subproblem in the context of branch-and-bound, and 2) directly improve intermediate bounds throughout the network. The process novelly leverages linear constraints that often arise from bound propagation methods and is general enough to also incorporate constraints from other sources. It efficiently handles linear constraints using a specialized GPU procedure that can scale to large neural networks without the use of expensive external solvers. Our verification procedure, Clip-and-Verify, consistently tightens bounds across multiple benchmarks and can significantly reduce the number of subproblems handled during BaB. We show that our clipping algorithms can be integrated with BaB-based verifiers such as $α,β$-CROWN, utilizing either the split constraints in activation-space BaB or the output constraints that denote the unverified input space. We demonstrate the effectiveness of our procedure on a broad range of benchmarks where, in some instances, we witness a 96% reduction in the number of subproblems during branch-and-bound, and also achieve state-of-the-art verified accuracy across multiple benchmarks. Clip-and-Verify is part of the $α,β$-CROWN verifier (http://abcrown.org), the VNN-COMP 2025 winner. Code available at https://github.com/Verified-Intelligence/Clip_and_Verify.