Data to 7 Oct 2026

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

arXiv 1702.01135 ↗First posted 3 Feb 2017cs.AI cs.LOcited by 739

Not on the map. Why?

Abstract (arXiv)

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.

Key facts. Cited by 739 papers in the map (data through 7 Oct 2026). First posted on arXiv 3 Feb 2017.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2018: 1; 2019: 0; 2020: 0; 2021: 137; 2022: 147; 2023: 128; 2024: 108; 2025: 98; 2026: 120.

739 papers.

Sort:

By area:

2018Scalable agent alignment via reward modeling: a research directioncited by 438
2023Are aligned neural networks adversarially aligned?cited by 305
2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
2023Survey of Vulnerabilities in Large Language Models Revealed by Adversarial Attackscited by 189
2021Advances in adversarial attacks and defenses in computer vision: A surveycited by 127
2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
2021Explainability of deep vision-based autonomous driving systems: Review and challengescited by 80
2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
2021The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Resultscited by 71
2023How Deep Learning Sees the World: A Survey on Adversarial Attacks & Defensescited by 65

38 more

2021Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Boundscited by 64
2024Risk Taxonomy, Mitigation, and Assessment Benchmarks of Large Language Model Systemscited by 63
2023First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)cited by 58
2021Handcrafted Backdoors in Deep Neural Networkscited by 57
2022Certified Training: Small Boxes are All You Needcited by 51
2022Safe Reinforcement Learning via Shielding under Partial Observabilitycited by 49
2022Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspectivecited by 48
2021Boosting Randomized Smoothing with Variance Reduced Classifierscited by 47
2022Logic-Based Explainability in Machine Learningcited by 47
2023Evaluating Superhuman Models with Consistency Checkscited by 47
2024Neural Network Verification with Branch-and-Bound for General Nonlinearitiescited by 47
2021Fast Certified Robust Training with Short Warmupcited by 45
2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
2021Improved Branch and Bound for Neural Network Verification via Lagrangian Decompositioncited by 44
2021Certified Patch Robustness via Smoothed Vision Transformerscited by 44
2021MultiplexNet: Towards Fully Satisfied Logical Constraints in Neural Networkscited by 44
2022Causality-based Neural Network Repaircited by 44
2022Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networkscited by 42
2021CROP: Certifying Robust Policies for Reinforcement Learning through Functional Smoothingcited by 41
2021Reachability Analysis of Neural Feedback Loopscited by 41
2022Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspectivecited by 41
2021Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Aheadcited by 40
2021Guidance on the Assurance of Machine Learning in Autonomous Systems (AMLAS)cited by 40
2021Boosting Fast Adversarial Training with Learnable Adversarial Initializationcited by 40
2021Provable Repair of Deep Neural Networkscited by 39
2022How to Robustify Black-Box ML Models? A Zeroth-Order Optimization Perspectivecited by 39
2022Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guaranteescited by 39
2022The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Resultscited by 39
2023When Deep Learning Meets Polyhedral Theory: A Surveycited by 39
2021POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systemscited by 38
2022Don't Lie to Me! Robust and Efficient Explainability with Verified Perturbation Analysiscited by 38
2021OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systemscited by 37
2021How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Reviewcited by 36
2021Neural Network Robustness as a Verification Property: A Principled Case Studycited by 35
2021Scalable Certified Segmentation via Randomized Smoothingcited by 35
2023A Survey on Knowledge Editing of Neural Networkscited by 34
2021A Review of Formal Methods applied to Machine Learningcited by 33
2021Towards Scalable Verification of Deep Reinforcement Learningcited by 33

50 most cited of 739 All 739 (JSON)