Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

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