# Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

arXiv: https://arxiv.org/abs/1702.01135 · HTML: https://mlsanity.com/paper/1702.01135/

## Key facts

- Cited by 744 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Feb 2017.

## Built on by (most cited first, 30 of 744)

- [Scalable agent alignment via reward modeling: a research direction](https://mlsanity.com/paper/1811.07871/) (2018)
- [Are aligned neural networks adversarially aligned?](https://mlsanity.com/paper/2306.15447/) (2023)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Survey of Vulnerabilities in Large Language Models Revealed by Adversarial Attacks](https://mlsanity.com/paper/2310.10844/) (2023)
- [Advances in adversarial attacks and defenses in computer vision: A survey](https://mlsanity.com/paper/2108.00401/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Explainability of deep vision-based autonomous driving systems: Review and challenges](https://mlsanity.com/paper/2101.05307/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [How Deep Learning Sees the World: A Survey on Adversarial Attacks & Defenses](https://mlsanity.com/paper/2305.10862/) (2023)
- [Risk Taxonomy, Mitigation, and Assessment Benchmarks of Large Language Model Systems](https://mlsanity.com/paper/2401.05778/) (2024)
- [Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Bounds](https://mlsanity.com/paper/2111.01395/) (2021)
- [Handcrafted Backdoors in Deep Neural Networks](https://mlsanity.com/paper/2106.04690/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Safe Reinforcement Learning via Shielding under Partial Observability](https://mlsanity.com/paper/2204.00755/) (2022)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Boosting Randomized Smoothing with Variance Reduced Classifiers](https://mlsanity.com/paper/2106.06946/) (2021)
- [Causality-based Neural Network Repair](https://mlsanity.com/paper/2204.09274/) (2022)
- [Evaluating Superhuman Models with Consistency Checks](https://mlsanity.com/paper/2306.09983/) (2023)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Fast Certified Robust Training with Short Warmup](https://mlsanity.com/paper/2103.17268/) (2021)
- [Certified Patch Robustness via Smoothed Vision Transformers](https://mlsanity.com/paper/2110.07719/) (2021)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [MultiplexNet: Towards Fully Satisfied Logical Constraints in Neural Networks](https://mlsanity.com/paper/2111.01564/) (2021)
- [Guidance on the Assurance of Machine Learning in Autonomous Systems (AMLAS)](https://mlsanity.com/paper/2102.01564/) (2021)

## 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.