Research and development of a formal verification algorithm and quality assessment metrics based on ANN dimensionality reduction methods

Abstract

Checking the quality of operation of artificial neural networks (ANN) using formal verification algorithms is the most guaranteed method among others, but there is a problem of computational complexity and very high time costs. The priority direction of research is to reduce the operating time of algorithms, which can be done either by directly changing the formal verification algorithm itself, or by carrying out some actions on the artificial neural network architecture being verified. This paper presents a study of methods for formal verification of  artificial neural networks based on ANN reduction methods, describes  experiments conducted to test the properties of selected neural network  architectures, and analyzes these methods. The Planet algorithm was taken as a  formal verification algorithm, the operation of the architecture with the  ReLU activation function was checked, so LeNet was chosen, dimensionality reduction methods such as dropout, pruning and quantization were used, the reachability property was checked, and the quality was determined using the RNE metric. The experimental results showed that the use of pruning gives a time gain, but the dropout method turned out to be the most effective, while the use of quantization for the selected Planet algorithm turned out to be impossible.