Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Guy Katz, Clark Barrett, David Dill, Kyle Julian, Mykel Kochenderfer
TL;DR
This work introduces Reluplex, an SMT-based solver that extends the simplex algorithm to handle ReLU activations for formal verification of deep neural networks. By encoding ReLUs with a hybrid forward/backward variable scheme and augmenting simplex with ReLU-specific rules, Reluplex efficiently verifies safety and robustness properties on real-world ACAS Xu networks. The approach demonstrates scalability beyond previous methods and shows how bound tightening, conflict analysis, and floating-point safeguards contribute to practical performance, while also establishing the NP-completeness of DNN property verification. The results suggest that ReLU-aware SMT techniques can substantially advance certification of safety-critical DNNs and guide future extensions to other layer types and proofs.
Abstract
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.