Modeling And Verification Of DeepID Based On MSVL

In recent years,neural network systems,especially convolutional neural network systems,have been widely used in various fields of society.However,because its internal model is opaque and difficult to explain,there are major security risks in some application fields,especially in the medical and financial fields,which are related to the safety of patients' lives and personal properties.At present,most of the interpretability research on deep learning starts from the perspective of visualization or automatic feature extraction,and lacks the exploration of the internal properties of the model.Formal verification uses mathematical methods to express system models and properties,and strictly analyzes the relationship between models and properties.As a deep learning model based on convolutional neural network,DeepID has a good performance in the field of face verification.This thesis takes DeepID as the research object and analyzes the relationship between model intermediate data and prediction results from the perspective of formal verification,so as to explore the interpretability of the convolutional neural network system.Aiming at the DeepID convolutional neural network model,this thesis proposes a modeling and verification scheme based on Modeling,Simulation and Verification Language(MSVL),which analyzes the relationship between the model's intermediate data and decision results,property extraction and verification.Specifically,at first,we expand and tailor the face data set You Tube Faces,and divide it into training set,verification set,No.1 and No.2 test sets.Next,we use MSVL to construct the DeepID forward propagation network model,including defining the structure,initializing the network,and realizing the forward propagation algorithm,among which the model parameters are determined by Python training on the training set and the validation set.Then,we analyze the relationship between the location distribution of neurons activated after Re LU operation and the decision result,and extract two types of distribution rules of neurons: activation consistency and activation inclusion.Finally,we use the Propositional Projection Temporal Logic(PPTL)formula to characterize the two types of properties,input the MSVL program and PPTL formula into the verification tool PPTLCheck,and verify the properties on the test set.The experimental results show that75.13% of the samples in No.1 test set meet the activation consistency,and 99.96% of the samples in No.2 test set meet the activation inclusion,which reveals the relationship between the neuron activation location and the model decision-making results.