mlsanityData to 7 Oct 2026

General Cutting Planes for Bound-Propagation-Based Neural Network Verification

arXiv 2208.05740 ↗First posted 11 Aug 2022cs.LG cs.CR cs.CVcited by 102

Not on the map. Why?

Abstract (arXiv)

Bound propagation methods, when combined with branch and bound, are among the most effective methods to formally verify properties of deep neural networks such as correctness, robustness, and safety. However, existing works cannot handle the general form of cutting plane constraints widely accepted in traditional solvers, which are crucial for strengthening verifiers with tightened convex relaxations. In this paper, we generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints, including those involving relaxed integer variables that do not appear in existing bound propagation formulations. Our generalized bound propagation method, GCP-CROWN, opens up the opportunity to apply general cutting plane methods for neural network verification while benefiting from the efficiency and GPU acceleration of bound propagation methods. As a case study, we investigate the use of cutting planes generated by off-the-shelf mixed integer programming (MIP) solver. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers using our new formulation. Since the branching-focused bound propagation procedure and the cutting-plane-focused MIP solver can run in parallel utilizing different types of hardware (GPUs and CPUs), their combination can quickly explore a large number of branches with strong cutting planes, leading to strong verification performance. Experiments demonstrate that our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark compared to the best tool in VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a wide range of benchmarks. GCP-CROWN is part of the α,!β-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN

Key facts. Cited by 102 papers in the map (data through 7 Oct 2026). Builds on 25 of its 67 references that are in the map. First posted on arXiv 11 Aug 2022.

Builds on

25 of 67 references.

References · 25

  1. 2014Adam: A Method for Stochastic Optimizationcited by 36,960
  2. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  3. 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
  4. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  5. 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
  6. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
  7. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  8. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  9. 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
  10. 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 178
  11. 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
  12. 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
13 more
  1. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  2. 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
  3. 2019A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networkscited by 124
  4. 2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
  5. 2021The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Resultscited by 71
  6. 2020Enabling certification of verification-agnostic networks via memory-efficient semidefinite programmingcited by 65
  7. 2020The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verificationcited by 50
  8. 2019Neural Network Branching for Neural Network Verificationcited by 45
  9. 2021Improved Branch and Bound for Neural Network Verification via Lagrangian Decompositioncited by 44
  10. 2020Scaling Polyhedral Neural Network Verification on GPUscited by 43
  11. 2020Lagrangian Decomposition for Neural Network Verificationcited by 35
  12. 2019Verification of Non-Linear Specifications for Neural Networkscited by 14
  13. 2021DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splittingcited by 8

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 6; 2023: 23; 2024: 33; 2025: 20; 2026: 20.

102 papers.

Sort:

By area:

  1. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  2. 2023First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)cited by 58
  3. 2022Certified Training: Small Boxes are All You Needcited by 51
  4. 2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
  5. 2022The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Resultscited by 39
  6. 2023When Deep Learning Meets Polyhedral Theory: A Surveycited by 39
  7. 2024Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planescited by 33
  8. 2023Provably Bounding Neural Network Preimagescited by 28
  9. 2023Understanding Certified Training with Interval Bound Propagationcited by 26
  10. 2023Expressive Losses for Verified Robustness via Convex Combinationscited 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
38 more
  1. 2023Neural Lyapunov Control for Discrete-Time Systemscited by 21
  2. 2023Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guaranteescited by 19
  3. 2023Incremental Verification of Neural Networkscited by 14
  4. 2023Exact Verification of ReLU Neural Control Barrier Functionscited by 14
  5. 2024Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programscited by 14
  6. 2024NLP Verification: Towards a General Methodology for Certifying Robustnesscited by 14
  7. 2024Harnessing Neuron Stability to Improve DNN Verificationcited by 13
  8. 2024CTBENCH: A Library and Benchmark for Certified Trainingcited by 13
  9. 2023TAPS: Connecting Certified and Adversarial Trainingcited by 11
  10. 2023Efficient Error Certification for Physics-Informed Neural Networkscited by 10
  11. 2025SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programmingcited by 10
  12. 2023Multi-scale Diffusion Denoised Smoothingcited by 9
  13. 2025Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verificationcited by 9
  14. 2023Expressivity of ReLU-Networks under Convex Relaxationscited by 8
  15. 2024Generative AI and Process Systems Engineering: The Next Frontiercited by 8
  16. 2024Efficient local linearity regularization to overcome catastrophic overfittingcited by 7
  17. 2024Verification-Aided Learning of Neural Network Barrier Functions with Termination Guaranteescited by 7
  18. 2024Verified Safe Reinforcement Learning for Neural Network Dynamic Modelscited by 7
  19. 2024ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networkscited by 7
  20. 2024Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisationcited by 7
  21. 2024Set-Based Training for Neural Network Verificationcited by 6
  22. 2024DeepCDCL: An CDCL-based Neural Network Verification Frameworkcited by 6
  23. 2025Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansioncited by 6
  24. 2023PECAN: A Deterministic Certified Defense Against Backdoor Attackscited by 5
  25. 2024Relational DNN Verification With Cross Executional Bound Refinementcited by 5
  26. 2024Certified Continual Learning for Neural Network Regressioncited by 5
  27. 2024SoundnessBench: A Soundness Benchmark for Neural Network Verifierscited by 5
  28. 2025Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systemscited by 5
  29. 2025Enhancing Certified Robustness via Block Reflector Orthogonal Layers and Logit Annealing Losscited by 5
  30. 2025No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networkscited by 5
  31. 2022Tight Certification of Adversarially Trained Neural Networks via Nonconvex Low-Rank Semidefinite Relaxationscited by 4
  32. 2024Gaussian Loss Smoothing Enables Certified Training with Tight Convex Relaxationscited by 4
  33. 2024Revisiting Differential Verification: Equivalence Verification with Confidencecited by 4
  34. 2025Parameterized Hardness of Zonotope Containment and Neural Network Verificationcited by 4
  35. 2025Faster Verified Explanations for Neural Networkscited by 4
  36. 2023A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networkscited by 3
  37. 2023Interpreting Robustness Proofs of Deep Neural Networkscited by 3
  38. 2024On Using Certified Training towards Empirical Robustnesscited by 3

50 most cited of 102 All 102 (JSON)