# Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification

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

## Key facts

- Cited by 228 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 56 references that are in the map.
- First posted on arXiv 11 Mar 2021.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [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)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations](https://mlsanity.com/paper/2003.08938/) (2020)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [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)
- [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)
- [Robust Deep Reinforcement Learning with Adversarial Attacks](https://mlsanity.com/paper/1712.03632/) (2017)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Robust Reinforcement Learning on State Observations with Learned Optimal Adversary](https://mlsanity.com/paper/2101.08452/) (2021)
- [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)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [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 228)

- [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)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [Improved deterministic l2 robustness on CIFAR-10 and CIFAR-100](https://mlsanity.com/paper/2108.04062/) (2021)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [Don't Lie to Me! Robust and Efficient Explainability with Verified Perturbation Analysis](https://mlsanity.com/paper/2202.07728/) (2022)
- [DensePure: Understanding Diffusion Models towards Adversarial Robustness](https://mlsanity.com/paper/2211.00322/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Boosting the Certified Robustness of L-infinity Distance Nets](https://mlsanity.com/paper/2110.06850/) (2021)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Local vs. Global Interpretability: A Computational Complexity Perspective](https://mlsanity.com/paper/2406.02981/) (2024)
- [Certified Robustness via Dynamic Margin Maximization and Improved Lipschitz Regularization](https://mlsanity.com/paper/2310.00116/) (2023)
- [DiffSmooth: Certifiably Robust Learning via Diffusion Models and Local Smoothing](https://mlsanity.com/paper/2308.14333/) (2023)
- [PRoA: A Probabilistic Robustness Assessment against Functional Perturbations](https://mlsanity.com/paper/2207.02036/) (2022)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [ScaleCert: Scalable Certified Defense against Adversarial Patches with Sparse Superficial Layers](https://mlsanity.com/paper/2110.14120/) (2021)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Double Bubble, Toil and Trouble: Enhancing Certified Robustness through Transitivity](https://mlsanity.com/paper/2210.06077/) (2022)
- [Logic of Differentiable Logics: Towards a Uniform Semantics of DL](https://mlsanity.com/paper/2303.10650/) (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)

## Abstract (arXiv)

Bound propagation based incomplete neural network verifiers such as CROWN are very efficient and can significantly accelerate branch-and-bound (BaB) based complete verification of neural networks. However, bound propagation cannot fully handle the neuron split constraints introduced by BaB commonly handled by expensive linear programming (LP) solvers, leading to loose bounds and hurting verification efficiency. In this work, we develop β-CROWN, a new bound propagation based method that can fully encode neuron splits via optimizable parameters β constructed from either primal or dual space. When jointly optimized in intermediate layers, β-CROWN generally produces better bounds than typical LP verifiers with neuron split constraints, while being as efficient and parallelizable as CROWN on GPUs. Applied to complete robustness verification benchmarks, β-CROWN with BaB is up to three orders of magnitude faster than LP-based BaB methods, and is notably faster than all existing approaches while producing lower timeout rates. By terminating BaB early, our method can also be used for efficient incomplete verification. We consistently achieve higher verified accuracy in many settings compared to powerful incomplete verifiers, including those based on convex barrier breaking techniques. Compared to the typically tightest but very costly semidefinite programming (SDP) based incomplete verifiers, we obtain higher verified accuracy with three orders of magnitudes less verification time. Our algorithm empowered the α,!β-CROWN (alpha-beta-CROWN) verifier, the winning tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN