# CLAD: Constrained Abstract Domain for Neural Network Verification

arXiv: https://arxiv.org/abs/2609.34628 · HTML: https://mlsanity.com/paper/2609.34628/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 26 of its 48 references that are in the map.
- First posted on arXiv 28 Sep 2026.

## Builds on (most cited first, 26 of 26)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Safety-Enhanced Autonomous Driving Using Interpretable Sensor Fusion Transformer](https://mlsanity.com/paper/2207.14024/) (2022)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Harnessing Neuron Stability to Improve DNN Verification](https://mlsanity.com/paper/2401.14412/) (2024)
- [SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming](https://mlsanity.com/paper/2506.06665/) (2025)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [FGGM: Formal Grey-box Gradient Method for Attacking DRL-based MU-MIMO Scheduler](https://mlsanity.com/paper/2510.26075/) (2025)
- [Verifying DNN-based Semantic Communication Against Generative Adversarial Noise](https://mlsanity.com/paper/2602.08801/) (2026)
- [LEVIS: Large Exact Verifiable Input Spaces for Neural Networks](https://mlsanity.com/paper/2408.08824/) (2024)

## Abstract (arXiv)

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.