# Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition

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

## Key facts

- Cited by 44 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 50 references that are in the map.
- First posted on arXiv 14 Apr 2021.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples](https://mlsanity.com/paper/1802.00420/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Adversarial Risk and the Dangers of Evaluating Against Weak Attacks](https://mlsanity.com/paper/1802.05666/) (2018)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (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)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Catalyst Acceleration for First-order Convex Optimization: from Theory to Practice](https://mlsanity.com/paper/1712.05654/) (2017)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [Fast Neural Network Verification via Shadow Prices](https://mlsanity.com/paper/1902.07247/) (2019)

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

- [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)
- [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)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [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)
- [Harnessing Neuron Stability to Improve DNN Verification](https://mlsanity.com/paper/2401.14412/) (2024)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)
- [Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness](https://mlsanity.com/paper/2206.07839/) (2022)
- [Efficient Error Certification for Physics-Informed Neural Networks](https://mlsanity.com/paper/2305.10157/) (2023)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [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)
- [Boosting Robustness Verification of Semantic Feature Neighborhoods](https://mlsanity.com/paper/2209.05446/) (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)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Verification of Neural Networks against Convolutional Perturbations via Parameterised Kernels](https://mlsanity.com/paper/2411.04594/) (2024)
- [Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification](https://mlsanity.com/paper/2505.00963/) (2025)
- [Efficient Preimage Approximation for Neural Network Certification](https://mlsanity.com/paper/2505.22798/) (2025)
- [Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification](https://mlsanity.com/paper/2507.23197/) (2025)
- [Learning Better Certified Models from Empirically-Robust Teachers](https://mlsanity.com/paper/2602.02626/) (2026)

## Abstract (arXiv)

We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. First, we propose novel bounding algorithms based on Lagrangian Decomposition. Previous works have used off-the-shelf solvers to solve relaxations at each node of the BaB tree, or constructed weaker relaxations that can be solved efficiently, but lead to unnecessarily weak bounds. Our formulation restricts the optimization to a subspace of the dual domain that is guaranteed to contain the optimum, resulting in accelerated convergence. Furthermore, it allows for a massively parallel implementation, which is amenable to GPU acceleration via modern deep learning frameworks. Second, we present a novel activation-based branching strategy. By coupling an inexpensive heuristic with fast dual bounding, our branching scheme greatly reduces the size of the BaB tree compared to previous heuristic methods. Moreover, it performs competitively with a recent strategy based on learning algorithms, without its large offline training cost. Finally, we design a BaB framework, named Branch and Dual Network Bound (BaDNB), based on our novel bounding and branching algorithms. We show that BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial robustness properties.