19 May 2017 | Guy Katz, Clark Barrett, David Dill, Kyle Julian and Mykel Kochenderfer
Reluplex is an efficient and scalable technique for verifying properties of deep neural networks (DNNs) with ReLU activation functions. The technique extends the simplex method to handle the non-convex nature of ReLUs, allowing for the verification of large DNNs without simplifying assumptions. The authors evaluated Reluplex on a prototype DNN implementation of the ACAS Xu system, demonstrating its ability to prove properties of networks that are an order of magnitude larger than those verifiable using existing methods. Key contributions include the extension of the simplex algorithm to support ReLU constraints, the encoding of DNNs and their properties as inputs to Reluplex, and the implementation details such as floating-point arithmetic, bound derivation, and conflict analysis. The evaluation shows that Reluplex can successfully verify various properties of the ACAS Xu networks, including functionality and robustness, with significant improvements over state-of-the-art solvers.Reluplex is an efficient and scalable technique for verifying properties of deep neural networks (DNNs) with ReLU activation functions. The technique extends the simplex method to handle the non-convex nature of ReLUs, allowing for the verification of large DNNs without simplifying assumptions. The authors evaluated Reluplex on a prototype DNN implementation of the ACAS Xu system, demonstrating its ability to prove properties of networks that are an order of magnitude larger than those verifiable using existing methods. Key contributions include the extension of the simplex algorithm to support ReLU constraints, the encoding of DNNs and their properties as inputs to Reluplex, and the implementation details such as floating-point arithmetic, bound derivation, and conflict analysis. The evaluation shows that Reluplex can successfully verify various properties of the ACAS Xu networks, including functionality and robustness, with significant improvements over state-of-the-art solvers.