mlsanityData to 7 Oct 2026

Neural Network Verification with Branch-and-Bound for General Nonlinearities

arXiv 2405.21063 ↗First posted 31 May 2024cs.LG cs.AIcited by 47

Not on the map. Why?

Abstract (arXiv)

Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs with piecewise linear activations, especially ReLU networks. In this paper, we develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures, based on linear bound propagation for NN verification. To decide which neuron to branch, we design a new branching heuristic which leverages linear bounds as shortcuts to efficiently estimate the potential improvement after branching. To decide nontrivial branching points for general nonlinear functions, we propose to pre-optimize branching points, which can be efficiently leveraged during verification with a lookup table. We demonstrate the effectiveness of our GenBaB on verifying a wide range of NNs, including NNs with activation functions such as Sigmoid, Tanh, Sine and GeLU, as well as NNs involving multi-dimensional nonlinear operations such as multiplications in LSTMs and Vision Transformers. Our framework also allows the verification of general nonlinear computation graphs and enables verification applications beyond simple NNs, particularly for AC Optimal Power Flow (ACOPF). GenBaB is part of the latest α,β-CROWN, the winner of the 4th and the 5th International Verification of Neural Networks Competition (VNN-COMP 2023 and 2024). Code for reproducing the experiments is available at https://github.com/shizhouxing/GenBaB.

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

Builds on

28 of 43 references.

References · 28

  1. 2017Attention Is All You Needcited by 59,932
  2. 2020An Image is Worth 16x16 Words: Transformers for Image Recognition at Scalecited by 29,915
  3. 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,326
  4. 2020Implicit Neural Representations with Periodic Activation Functionscited by 2,214
  5. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  6. 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
  7. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  8. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  9. 2019Towards Stable and Efficient Training of Verifiably Robust Neural Networkscited by 204
  10. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  11. 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
  12. 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
16 more
  1. 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
  2. 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
  3. 2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
  4. 2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
  5. 2020Robustness Verification for Transformerscited by 76
  6. 2019Neural Network Branching for Neural Network Verificationcited by 45
  7. 2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
  8. 2021Improved Branch and Bound for Neural Network Verification via Lagrangian Decompositioncited by 44
  9. 2019Fastened CROWN: Tightened Neural Network Robustness Certificatescited by 39
  10. 2023The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Resultscited by 38
  11. 2019Machine Learning for AC Optimal Power Flowcited by 24
  12. 2020Scalable Polyhedral Verification of Recurrent Neural Networkscited by 20
  13. 2023Convex Bounds on the Softmax Function with Applications to Robustness Verificationcited by 19
  14. 2022Toward Certified Robustness Against Real-World Distribution Shiftscited by 16
  15. 2022LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functionscited by 10
  16. 2023RNN-Guard: Certified Robustness Against Multi-frame Attacks for Recurrent Neural Networkscited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 8; 2025: 17; 2026: 22.

47 papers.

Sort:

  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. 2024SoundnessBench: A Soundness Benchmark for Neural Network Verifierscited by 5
  5. 2024Revisiting Differential Verification: Equivalence Verification with Confidencecited by 4
  6. 2024Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificatescited by 3
  7. 2024Certified Training with Branch-and-Bound for Lyapunov-stable Neural Controlcited by 3
  8. 2025Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimationcited by 3
  9. 2024Achieving the Tightest Relaxation of Sigmoids for Formal Verificationcited by 2
  10. 2024Expressiveness of Multi-Neuron Convex Relaxations in Neural Network Certificationcited by 2
  11. 2024Learning Ensembles of Vision-based Safety Control Filterscited by 2
  12. 2025Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputscited by 2
35 more
  1. 2025Adaptive Branch-and-Bound Tree Exploration for Neural Network Verificationcited by 2
  2. 2025Local Stability and Region of Attraction Analysis for Neural Network Feedback Systems under Positivity Constraintscited by 2
  3. 2025Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagationcited by 2
  4. 2026Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimizationcited by 2
  5. 2025A General Framework for Property-Driven Machine Learningcited by 1
  6. 2026Provably Explaining Neural Additive Modelscited by 1
  7. 2026Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorialcited by 1
  8. 2026Lookahead Branching for Neural Network Verificationcited by 1
  9. 2024Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Reportcited by 0
  10. 2025A Guide to Failure in Machine Learning: Reliability and Robustness from Foundations to Practicecited by 0
  11. 2025Evaluation and Verification of Physics-Informed Neural Models of the Grad-Shafranov Equationcited by 0
  12. 2025Language Models That Walk the Talk: A Framework for Formal Fairness Certificatescited by 0
  13. 2025Verification of Visual Controllers via Compositional Geometric Transformationscited by 0
  14. 2025Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Treescited by 0
  15. 2025Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precisioncited by 0
  16. 2025Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Casecited by 0
  17. 2025Lipschitz-aware Linearity Grafting for Certified Robustnesscited by 0
  18. 2025Dual Randomized Smoothing: Beyond Global Noise Variancecited by 0
  19. 2026Conformal Reachability for Safe Control in Unknown Environmentscited by 0
  20. 2026Optimized Piecewise Affine Abstractions of Neural Networks with Learnable Activation Functionscited by 0
  21. 2026Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solverscited by 0
  22. 2026Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimationcited by 0
  23. 2026Certified and accurate computation of function space norms of deep neural networkscited by 0
  24. 2026Lipschitz-Based Robustness Certification Under Floating-Point Executioncited by 0
  25. 2026Demystifying Lipschitz verification: positive matrices, negative resultscited by 0
  26. 2026Analyzing Symbolic Properties for DRL Agents in Systems and Networkingcited by 0
  27. 2026Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinementcited by 0
  28. 2026Encrypted Neural Networks without Overflowscited by 0
  29. 2026Lipschitz Optimization for Formal Verification of Homographiescited by 0
  30. 2026Neural Network Verification using Partial Multi-Neuron Relaxationcited by 0
  31. 2026Robustness Verification of Recurrent Neural Networks with Abstraction Refinementcited by 0
  32. 2026Shifting-based Optimizable Linear Relaxations for General Activation Functionscited by 0
  33. 2026Repurposing CLIP to Localize at Pixel Levelcited by 0
  34. 2026Learning Lookahead Lemmas for Neural Network Verificationcited by 0
  35. 2026Branch and Bound for Relational Verification of Neural Networkscited by 0