Research On The Property Verification Framework Of Neural Network Model Based On MSVL

Along with the widespread use of neural network models in various industries,their safety and robustness are receiving more and more attention from the academic and industrial communities,especially in safety-critical areas,such as autonomous driving,malware detection.Every wrong judgment of neural networks will bring irreparable consequences.Neural network is an optimization model based on mathematical statistics.The purpose is to use some approximate function to efficiently handle the indescribable input-output relationships in the physical world.This means that neural networks are inherently uncertain about unknown inputs.Formal method is a modeling and verification method based on rigorous mathematical logic suitable for describing software and hardware systems.The purpose is to improve the reliability of software and hardware design.It is a typical deterministic result-oriented method.Applying formal methods to the modeling and verification process of neural networks will help to improve the uncertainty relationship of neural networks and increase the credibility of neural network output results.The existing researches are mainly based on satisfiability modulo theories,abstract interpretation,interval calculation,etc.This thesis focuses on the verification of the temporal logic properties.Through the verification results,an accurate judgment of the key properties of the neural network is given,and the purpose of improving the neural network model system is achieved.This thesis proposes a research scheme based on temporal logic programming language to study the correctness and robustness of neural networks.This scheme works under the framework of UMC(Unified Model Checking)and the specific workflow is as follows:Firstly,the DNN(Deep Neural Network)model and the CNN(Convolutional Neural Network)model are selected,and the suitable text dataset and image dataset are given respectively.Secondly,the formal definitions of three common properties,which are model correctness,sample correctness and model robustness in neural network systems,are elaborated.These properties are refined in the DNN-based arithmetic expression system and the CNN-based handwritten image recognition system and they respectively describe the accuracy of the model systems,the rationality of the input data and the coping ability to the external attacks.Thirdly,a neural network model system M based on MSVL(Modeling,Simulation and Verification Language)is constructed and the execution results are obtained in the MC(MSVL Compiler).At the same time,the common property P based on PPTL(Propositional Projection Temporal Logic)is expressed and the verification results are obtained in the UMC4M validator.Finally,for the CNN model systems which include different dataset sizes and various network structures,the running time and the verification time are compared and analyzed.As a result,the feasibility and effectiveness of the property-driven neural network verification scheme is demonstrated.