Formal verification of deep neural networks

This paper introduces a method for the formal verification of neural networks using a Satisfiability Modulo Theories (SMT) solver. This approach enables the mathematical validation of specific neural network properties, enhancing their predictability. We propose a method for simplifying a neural network’s computational graph within certain input space regions. This is achieved by replacing neurons’ piecewise-linear activation functions with a subset of their linear segments. This optimization hypothesizes a simpler interpretation of a neural network over limited input data ranges. The simplified interpretation is derived from the incremental simplification of the neural network graph, achieved by solving local SMT tasks on a neuron-by-neuron basis. This optimization significantly speeds up the verification algorithm compared to solving a single SMT task over the entire unoptimized network graph. The method is applicable to any deep neural networks with piecewise-linear activation functions. The approach’s effectiveness was demonstrated by automatically verifying a network traffic classifier specializing in botnet activity detection. The classification model was tested for robustness against adversarial attacks, where attackers attempt to evade detection by introducing specially crafted disturbances into the network data. The verification procedure was conducted over regions in the feature-space near the classifier’s decision boundary. The results contribute to the prospects for more active application of artificial intelligence models in cybersecurity, where result predictability and interpretability are crucial. Additionally, the neuron - wise simplification technique proposed is a promising direction for further development in neural network verification.