# Lagrangian Decomposition for Neural Network Verification

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

## Key facts

- Cited by 35 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Feb 2020.

## Built on by (most cited first, 30 of 35)

- [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)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound](https://mlsanity.com/paper/2206.14772/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [From Robustness to Explainability and Back Again](https://mlsanity.com/paper/2306.03048/) (2023)
- [Generating Adversarial Examples with Graph Neural Networks](https://mlsanity.com/paper/2105.14644/) (2021)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [Optimizing Objective Functions from Trained ReLU Neural Networks via Sampling](https://mlsanity.com/paper/2205.14189/) (2022)
- [Scaling the Convex Barrier with Sparse Dual Algorithms](https://mlsanity.com/paper/2101.05844/) (2021)
- [Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness](https://mlsanity.com/paper/2206.07839/) (2022)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [BNN-DP: Robustness Certification of Bayesian Neural Networks via Dynamic Programming](https://mlsanity.com/paper/2306.10742/) (2023)
- [Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation](https://mlsanity.com/paper/2408.13140/) (2024)
- [Neural Network Branch-and-Bound for Neural Network Verification](https://mlsanity.com/paper/2107.12855/) (2021)
- [Zonotope Domains for Lagrangian Neural Network Verification](https://mlsanity.com/paper/2210.08069/) (2022)
- [Sound and Complete Verification of Polynomial Networks](https://mlsanity.com/paper/2209.07235/) (2022)
- [Faster Verified Explanations for Neural Networks](https://mlsanity.com/paper/2512.00164/) (2025)
- [Taking the human out of decomposition-based optimization via artificial intelligence: Part I. Learning when to decompose](https://mlsanity.com/paper/2310.07068/) (2023)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [On Using Certified Training towards Empirical Robustness](https://mlsanity.com/paper/2410.01617/) (2024)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)

## Abstract (arXiv)

A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. Previous methods have either used off-the-shelf solvers, discarding the problem structure, or relaxed the problem even further, making the bounds unnecessarily loose. We propose a novel approach based on Lagrangian Decomposition. Our formulation admits an efficient supergradient ascent algorithm, as well as an improved proximal algorithm. Both the algorithms offer three advantages: (i) they yield bounds that are provably at least as tight as previous dual algorithms relying on Lagrangian relaxations; (ii) they are based on operations analogous to forward/backward pass of neural networks layers and are therefore easily parallelizable, amenable to GPU implementation and able to take advantage of the convolutional structure of problems; and (iii) they allow for anytime stopping while still providing valid bounds. Empirically, we show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time, and obtain tighter bounds in the same time as previous dual algorithms. This results in an overall speed-up when employing the bounds for formal verification. Code for our algorithms is available at https://github.com/oval-group/decomposition-plnn-bounds.