SMT-based Formal Verification Methods of Deep Neural Networks using Structural Properties

Moonhyeon Chung, Kyungmin Bae

http://doi.org/10.5626/JOK.2021.48.9.998

Deep neural networks (DNN) are widely used for software in various fields, such as speech recognition and image classification. However, unexpected errors, such as adversarial examples, may exist in DNNs. DNN formal verification techniques to verify the requirements of DNNs are being widely studied in order to prevent these errors. This paper proposes a methodology that utilizes the structural properties of DNNs to increase the performance of DNN verification. This paper mathematically defines the structural property of DNN, suggests two structural properties of DNN with ReLU as an activation function, and shows that the verification speed of SMT-based DNN verification can be increased using the structural properties.