← All papers
First page of CLAD: Constrained Abstract Domain for Neural Network Verification

CLAD: Constrained Abstract Domain for Neural Network Verification

Hai Duong, Thanh Le, ThanhVu Nguyen

cs.SE Sep 28, 2026 · v2 cs.LG
Soundness (weak duality) and tightness (strong duality via Sion's minimax theorem) of the CLAD bounds are mechanized sorry-free in Lean 4 with Mathlib.
Neural network verification (NNV) formally verifies that a network satisfies a specified property for all inputs within a defined region. Modern NNV tools employ abstract domains to compute a sound over-approximation of the network's behavior from the given input region, thus the tightness of these abstractions essentially determines efficiency. A long line of increasingly precise domains has been developed, but they all describe the valid input region in the same restrictive way, e.g., an Lp-norm ball. A practical input region is rarely a simple Lp ball, but rather a combination Lp ball with additional constraints. Verifying a network over such a region with existing abstraction produces a loose over-approximation, which results in either failing to verify a property or spurious counterexamples. We introduce Constrained Lagrangian Abstract Domain (CLAD), a new abstract domain that computes a sound over-approximation of neural networks over input regions defined by a combination of convex constraints. CLAD propagates these constraints and tightens bounds over the true feasible region. However, bounding a neuron over the intersection of these constraints has no closed-form solution, so CLAD relaxes each constraint into the objective with a Lagrange multiplier and solves the resulting max-min problem with a projected primal-dual method, alternating a projected gradient step on the input with a multiplier update. CLAD supports any convex constraint with a subgradient, e.g., from automatic differentiation. We evaluate CLAD on 1,944 instances across four convolutional networks with motion-blur structured perturbations with halfspace or L2-ball constraints. On standard unconstrained Linf property, CLAD verifies as many instances as GCPCROWN at a similar runtime. On constrained properties, CLAD verifies 60% more instances than GCPCROWN on L2-ball properties, and 22% more in total.

Abstract domains for neural network verification describe the input region as an Lp-norm ball. Practical regions combine an Lp ball with extra convex constraints, and over-approximating these with existing domains gives loose bounds. The result is failed verifications or spurious counterexamples.

CLAD keeps symbolic polyhedral bounds and concrete bounds for each neuron. It computes the concrete bounds by optimizing over the full feasible region: each convex constraint is relaxed into the objective with a Lagrange multiplier. The resulting max-min problem is solved by a projected primal-dual method. Soundness (weak duality) and tightness under the Slater condition (strong duality via Sion's minimax theorem) are mechanized sorry-free in Lean 4 against Mathlib.

The evaluation covers 1,944 motion-blur instances on four convolutional networks. On unconstrained Linf properties, CLAD matches GCP-CROWN in verified instances at similar runtime. On constrained properties it verifies 60% more instances on L2-ball properties and 22% more in total.