Attack-Guided Efficient Robustness Verification of ReLU Neural Networks

Nowadays the robustness of Deep Neural Networks (DNN) is gaining much more attention than ever. That is because DNNs are intensively adopted in safety-critical AI-enabled applications such as autonomous driving and authentication control. Formal methods have been proved to be effective to provide provable guarantee to the robustness of DNNs. However, they are suffering from bad scalability due to intrinsic high computational complexity of the verification problem. In this paper, we propose a novel attack-guided approach for efficiently verifying the robustness of neural networks. The novelty of our approach is that we use existing attack approaches to generate coarse adversarial examples, by which we can significantly simply final verification problem. In particular, we are focused on the neural networks that take ReLU activation functions, which are widely adopted for solving classification problems. The experimental results show that our approach outperforms those verification tools based on constraint solving by up to 69 times speedup, while it can compute minimum adversarial examples. The improvement is particularly significant on those adversarially trained networks.