mlsanityData to 7 Oct 2026

Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers

arXiv 2011.13824 ↗First posted 27 Nov 2020cs.AI cs.LGcited by 183

Not on the map. Why?

Abstract (arXiv)

Formal verification of neural networks (NNs) is a challenging and important problem. Existing efficient complete solvers typically require the branch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such as Linear Programming (LP) on linearly relaxed sub-domains. In this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typical machine learning accelerators such as GPUs and TPUs. However, unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire procedure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On a single GPU, we demonstrate an order of magnitude speedup compared to existing LP-based approaches.

Key facts. Cited by 183 papers in the map (data through 7 Oct 2026). First posted on arXiv 27 Nov 2020.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 11; 2022: 25; 2023: 20; 2024: 43; 2025: 39; 2026: 45.

183 papers.

Sort:

By area:

  1. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  2. 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
  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. 2021The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Resultscited by 71
  6. 2021Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Boundscited by 64
  7. 2023First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)cited by 58
  8. 2024Neural Network Verification with Branch-and-Bound for General Nonlinearitiescited by 47
  9. 2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
  10. 2021Reachability Analysis of Neural Feedback Loopscited by 41
  11. 2022The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Resultscited by 39
  12. 2024Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planescited by 33
38 more
  1. 2023Provably Bounding Neural Network Preimagescited by 28
  2. 2022Efficient Neural Network Analysis with Sum-of-Infeasibilitiescited by 24
  3. 2022Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopescited by 24
  4. 2023Expressive Losses for Verified Robustness via Convex Combinationscited by 23
  5. 2023A DPLL(T) Framework for Verifying Deep Neural Networkscited by 23
  6. 2024Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulationcited by 23
  7. 2022Safety Certification for Stochastic Systems via Neural Barrier Functionscited by 22
  8. 2023Convex Bounds on the Softmax Function with Applications to Robustness Verificationcited by 19
  9. 2022Scalable Verification of GNN-based Job Schedulerscited by 18
  10. 2022CertiFair: A Framework for Certified Global Fairness of Neural Networkscited by 17
  11. 2022Toward Certified Robustness Against Real-World Distribution Shiftscited by 16
  12. 2023The Best Defense is a Good Offense: Adversarial Augmentation against Adversarial Attackscited by 15
  13. 2021Learning Security Classifiers with Verified Global Robustness Propertiescited by 14
  14. 2022Can pruning improve certified robustness of neural networks?cited by 14
  15. 2023Provable Preimage Under-Approximation for Neural Networks (Full Version)cited by 13
  16. 2024Harnessing Neuron Stability to Improve DNN Verificationcited by 13
  17. 2024CTBENCH: A Library and Benchmark for Certified Trainingcited by 13
  18. 2022Toward Robust Spiking Neural Network Against Adversarial Perturbationcited by 12
  19. 2022Certifiable 3D Object Pose Estimation: Foundations, Learning Models, and Self-Trainingcited by 12
  20. 2022On Neural Network Equivalence Checking using SMT Solverscited by 10
  21. 2022Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustnesscited by 10
  22. 2023Efficient Error Certification for Physics-Informed Neural Networkscited by 10
  23. 2024Verifiably Robust Conformal Predictioncited by 10
  24. 2024Detecting Brittle Decisions for Free: Leveraging Margin Consistency in Deep Robust Classifierscited by 10
  25. 2025SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programmingcited by 10
  26. 2022CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustnesscited by 9
  27. 2023Safe Deep Reinforcement Learning by Verifying Task-Level Propertiescited by 9
  28. 2023Architecture-Preserving Provable Repair of Deep Neural Networkscited by 9
  29. 2024Neural Network Verification with PyRATcited by 9
  30. 2025Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verificationcited by 9
  31. 2021DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splittingcited by 8
  32. 2023Expressivity of ReLU-Networks under Convex Relaxationscited by 8
  33. 2024PREMAP: A Unifying PREiMage APproximation Framework for Neural Networkscited by 8
  34. 2021Provable Lipschitz Certification for Generative Modelscited by 7
  35. 2022P-split formulations: A class of intermediate formulations between big-M and convex hull for disjunctive constraintscited by 7
  36. 2024Provably Safe Neural Network Controllers via Differential Dynamic Logiccited by 7
  37. 2024Verified Safe Reinforcement Learning for Neural Network Dynamic Modelscited by 7
  38. 2024ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networkscited by 7

50 most cited of 183 All 183 (JSON)