mlsanityData to 7 Oct 2026

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

arXiv 2501.00200 ↗First posted 31 Dec 2024cs.LG cs.CR math.OCcited by 33

Not on the map. Why?

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 .

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

Builds on

31 of 63 references.

References · 31

  1. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  2. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
  3. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  4. 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
  5. 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
  6. 2018Strong mixed-integer programming formulations for trained neural networkscited by 115
  7. 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
  8. 2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
  9. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  10. 2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
  11. 2021The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Resultscited by 71
  12. 2020Enabling certification of verification-agnostic networks via memory-efficient semidefinite programmingcited by 65
19 more
  1. 2019Neural Network Branching for Neural Network Verificationcited by 45
  2. 2021Improved Branch and Bound for Neural Network Verification via Lagrangian Decompositioncited by 44
  3. 2020Scaling Polyhedral Neural Network Verification on GPUscited by 43
  4. 2024The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Resultscited by 42
  5. 2021Partition-based formulations for mixed-integer optimization of trained ReLU neural networkscited by 39
  6. 2022The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Resultscited by 39
  7. 2023When Deep Learning Meets Polyhedral Theory: A Surveycited by 39
  8. 2023The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Resultscited by 38
  9. 2019Verification of Neural Network Behaviour: Formal Guarantees for Power System Applicationscited by 26
  10. 2018Empirical Bounds on Linear Regions of Deep Rectifier Networkscited by 23
  11. 2023A DPLL(T) Framework for Verifying Deep Neural Networkscited by 23
  12. 2024Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulationcited by 23
  13. 2023Neural Lyapunov Control for Discrete-Time Systemscited by 21
  14. 2021ROMAX: Certifiably Robust Deep Multiagent Reinforcement Learning via Convex Relaxationcited by 17
  15. 2019Verification of Non-Linear Specifications for Neural Networkscited by 14
  16. 2022CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustnesscited by 9
  17. 2024Verification-Aided Learning of Neural Network Barrier Functions with Termination Guaranteescited by 7
  18. 2024DeepCDCL: An CDCL-based Neural Network Verification Frameworkcited by 6
  19. 2020Neural Network Virtual Sensors for Fuel Injection Quantities with Provable Performance Specificationscited by 4

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 11; 2026: 22.

33 papers.

Sort:

By area:

  1. 2025SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programmingcited by 10
  2. 2026Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guaranteescited by 10
  3. 2025Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verificationcited by 9
  4. 2025Proof Minimization in Neural Network Verificationcited by 4
  5. 2025Faster Verified Explanations for Neural Networkscited by 4
  6. 2025PICID: Proof-Driven Clause Learning in Neural Network Verificationcited by 3
  7. 2025Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimationcited by 3
  8. 2025Probabilistic Robustness Analysis in High Dimensional Space: Application to Semantic Segmentation Networkcited by 3
  9. 2026Incremental Neural Network Verification via Learned Conflictscited by 2
  10. 2025Mini-Batch Robustness Verification of Deep Neural Networkscited by 1
  11. 2025Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exitscited by 1
  12. 2026Learning Better Certified Models from Empirically-Robust Teacherscited by 1
21 more
  1. 2026Provably Explaining Neural Additive Modelscited by 1
  2. 2026IoUCert: Robustness Verification for Anchor-based Object Detectorscited by 1
  3. 2026Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorialcited by 1
  4. 2026Lookahead Branching for Neural Network Verificationcited by 1
  5. 2026TestifAI: Tomography-Based Testing for Deep Learning Systemscited by 1
  6. 2026ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Modelscited by 1
  7. 2025Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verificationcited by 0
  8. 2025Formal Reasoning About Confidence and Automated Verification of Neural Networkscited by 0
  9. 2026Talking with Verifiers: Automatic Specification Generation for Neural Network Verificationcited by 0
  10. 2026Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimationcited by 0
  11. 2026From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specificationscited by 0
  12. 2026Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networkscited by 0
  13. 2026Neural Network Verification using Partial Multi-Neuron Relaxationcited by 0
  14. 2026Rethinking Evaluation Paradigms in IBP-based Certified Trainingcited by 0
  15. 2026Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelismcited by 0
  16. 2026Robustness Verification of Recurrent Neural Networks with Abstraction Refinementcited by 0
  17. 2026Fast SDP certification of neural networks : towards large multi-class datasetscited by 0
  18. 2026Certified Training for Convolutional Perturbationscited by 0
  19. 2026Learning Lookahead Lemmas for Neural Network Verificationcited by 0
  20. 2026Verifying Neural Networks with Reinforcement Learningcited by 0
  21. 2026CLAD: Constrained Abstract Domain for Neural Network Verificationcited by 0