# Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 63 references that are in the map.
- First posted on arXiv 31 Dec 2024.

## Builds on (most cited first, 30 of 31)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [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)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (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)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [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)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Verification of Neural Network Behaviour: Formal Guarantees for Power System Applications](https://mlsanity.com/paper/1910.01624/) (2019)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Empirical Bounds on Linear Regions of Deep Rectifier Networks](https://mlsanity.com/paper/1810.03370/) (2018)
- [Neural Lyapunov Control for Discrete-Time Systems](https://mlsanity.com/paper/2305.06547/) (2023)
- [ROMAX: Certifiably Robust Deep Multiagent Reinforcement Learning via Convex Relaxation](https://mlsanity.com/paper/2109.06795/) (2021)
- [Verification of Non-Linear Specifications for Neural Networks](https://mlsanity.com/paper/1902.09592/) (2019)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees](https://mlsanity.com/paper/2403.07308/) (2024)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)

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

- [SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming](https://mlsanity.com/paper/2506.06665/) (2025)
- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [Faster Verified Explanations for Neural Networks](https://mlsanity.com/paper/2512.00164/) (2025)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation](https://mlsanity.com/paper/2506.13961/) (2025)
- [Probabilistic Robustness Analysis in High Dimensional Space: Application to Semantic Segmentation Network](https://mlsanity.com/paper/2509.11838/) (2025)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Learning Better Certified Models from Empirically-Robust Teachers](https://mlsanity.com/paper/2602.02626/) (2026)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [IoUCert: Robustness Verification for Anchor-based Object Detectors](https://mlsanity.com/paper/2603.03043/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Lookahead Branching for Neural Network Verification](https://mlsanity.com/paper/2607.17290/) (2026)
- [TestifAI: Tomography-Based Testing for Deep Learning Systems](https://mlsanity.com/paper/2608.18900/) (2026)
- [ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models](https://mlsanity.com/paper/2609.34457/) (2026)
- [Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification](https://mlsanity.com/paper/2506.10269/) (2025)
- [Formal Reasoning About Confidence and Automated Verification of Neural Networks](https://mlsanity.com/paper/2511.07293/) (2025)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimation](https://mlsanity.com/paper/2603.03082/) (2026)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)
- [Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks](https://mlsanity.com/paper/2605.24084/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [Rethinking Evaluation Paradigms in IBP-based Certified Training](https://mlsanity.com/paper/2606.02134/) (2026)
- [Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism](https://mlsanity.com/paper/2606.09377/) (2026)
- [Robustness Verification of Recurrent Neural Networks with Abstraction Refinement](https://mlsanity.com/paper/2606.12490/) (2026)
- [Fast SDP certification of neural networks : towards large multi-class datasets](https://mlsanity.com/paper/2607.03232/) (2026)
- [Certified Training for Convolutional Perturbations](https://mlsanity.com/paper/2607.18195/) (2026)

## Abstract (arXiv)

Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advances. However, GCP-CROWN currently relies on generic cutting planes (cuts) generated from external mixed integer programming (MIP) solvers. Due to the poor scalability of MIP solvers, large neural networks cannot benefit from these cutting planes. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes specific for this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), which leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts. Furthermore, we design a multi-tree search technique to identify more cuts, effectively narrowing the search space and accelerating the BaB algorithm. Our results demonstrate that BICCOS can generate hundreds of useful cuts during the branch-and-bound process and consistently increase the number of verifiable instances compared to other state-of-the-art neural network verifiers on a wide range of benchmarks, including large networks that previous cutting plane methods could not scale to. BICCOS is part of the α,β-CROWN verifier, the VNN-COMP 2024 winner. The code is available at http://github.com/Lemutisme/BICCOS .