ERAN User Manual

Neural networks are becoming more and more important. They are applied in many real-world applications, such as speech recognition [Hinton et al. 2012], medical diagnostic [Al-Shayea 2011], and autonomous driving [Bojarski et al. 2016] among other fields. Thus it is critical that neural networks behave reliably. This has led to the need to verify the safety of these networks. A number of efforts have been made in this direction, from less scalable but complete verifiers based on SMT solving [Katz et al. 2017, Ehlers 2017, Bunel et al. 2017], mixed-integer linear programming [Tjeng and Tedrake 2017], or Lipschitz optimization [Ruan et al. 2018] to more scalable but incomplete verifiers based on abstract interpretation [Gehr et al. 2018, Singh et al. 2018, Singh et al. 2019a], duality [Dvijotham et al. 2018, Kolter and Wong 2017], semidefinite programming [Raghunathan et al. 2018, Dvijotham et al. 2019] or linear relaxations [Weng et al. 2018, Zhang et al. 2018, Boopathy et al. 2019]. All of the above works require specific network formats, which limits usability. The Secure, Reliable, and Intelligent Systems Lab (SRI) at ETH aims to provide all of its state-of-the-art research on neural network verification in one tool with the ETH Robustness Analyzer for Neural Networks (ERAN). The goal of this work is to extend ERAN for handling more diverse network formats and architectures and add testing support to increase the trust in the verification process. This thesis describes the newest version of the ERAN, which offers complete and incomplete verification methods for feedforward, convolutional and residual neural networks. ERAN can analyze ONNX and TensorFlow models directly, making it accessible and easy to use.