Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

By Guy Katz, Clark W. Barrett, David L. Dill, Kyle D. Julian, Mykel J. Kochenderfer. 2017

2,155 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Vision and Pattern Recognition, Safety, Robustness & Interpretability

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Vision and Pattern Recognition

In Safety, Robustness & Interpretability

Citations in the corpus

Scalable agent alignment via reward modeling: a research direction (2018, background): “Recent progress on model checking for neural networks opens the door for formal verification of trained models (Katz et al., 2017).”
Risks from Learned Optimization in Advanced Machine Learning Systems (2019, methodology): “an SMT solver that in principle allows for verification of arbitrary propositions about activations in the network,[32] and black-box algorithms[33].”
Certified Robustness to Adversarial Examples with Differential Privacy (2018, background): “One line of work focuses on minimizing false positives by finding concrete counterexamples demonstrating robustness violations [24], [29].”
Attack of the Tails: Yes, You Really Can Backdoor Federated Learning (2020, methodology): “This idea is not novel and for example, has been used in [84] to prove another ReLU related NP-hardness result.”
Certified Adversarial Robustness via Randomized Smoothing (2019, methodology): “Exact methods are usually based on Satisfiability Modulo Theories (Katz et al., 2017; Carlini et al., 2017; Ehlers, 2017; Huang et al., 2017) or mixed integer linear programming (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2017; Fischetti & Jo, 2018; Bunel et al., 2018).”
Efficient Formal Safety Analysis of Neural Networks (2018, methodology): “Our experimental results show that on average Neurify is 5, 000× faster than Reluplex [13] and 20× than ReluVal [28].”
Training verified learners with learned verifiers (2018, background): “The verification problem (3) is NP-hard so computing the exact optimal value in general is difficult [14].”
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, methodology): “[21] extended the simplex algorithm to verify properties of FNNs with ReLU.”
Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, methodology): “Table 1 compares the time needed for ReluVal with that of Reluplex for verifying ten original properties described in their paper [20].”
Certified Defenses against Adversarial Examples (2018, methodology): “This includes verifying safety properties of air traffic control systems (Katz et al., 2017a;b) and self-driving cars (O’Kelly et al., 2016; 2017), as well as security applications such as robustness to training time attacks (Steinhardt et al., 2017).”
Verifying Neural Networks with Mixed Integer Programming (2017, neutral): “The algorithm relies on iteratively calling a Satisfiability Modulo Theories (SMT) solver [11] to determine whether there exists an adversarial example within a selected distance δ.”
Provable defenses against adversarial examples via the convex outer adversarial polytope (2017, methodology): “The ﬁrst (which is a topic that is broader than merely adversarial examples), is the work in the veriﬁcation of neural networks [Huang et al., 2017, Katz et al., 2017, Ehlers, 2017].”
NO Need to Worry about Adversarial Examples in Object Detection in Autonomous Vehicles (2017, background): “In the past few years, researchers tried to explain why neural nets are susceptible to such examples despite their impressive success on random test datasets [6, 5, 2], suggested new methods to generate adversarial examples and measure NN robustness against them [4, 21, 16, 9, 17, 19, 13], and propo”
DeepXplore: Automated Whitebox Testing of Deep Learning Systems (2017, background): “Another recent line of work has explored the possibility of formally verifying DNNs against different safety properties [32, 37, 57].”
Safety Verification of Deep Neural Networks (2016, methodology): “Since the first version of this paper appeared [20], another constraint-based method has been proposed in [21] which improves on [30].”
Toward Trustworthy AI Development: Mechanisms for Supporting Verifiable Claims (2020, background): “Without approximation, certificates are computationally prohibitive for all but the smallest real world tasks [69].”