Divide-and-Conquer Verification And Adversarial Testing Based Neural Network Safety Analysis

With the rapid development of artificial intelligence(AI)technology,deep learning has found widespread applications in safety-critical domains such as autonomous driving,intelligent manufacturing and medical diagnostics.However,in contrast to traditional algorithms,neural networks exhibit a lack of stability and interpretability.And in practical applications,failures of neural network models have caused many serious safety incidents.This issue has significantly hindered further development of deep learning,and consequently research on safety analysis of neural networks has great importance for reducing pre-deployment risks and establishing safe and reliable neural network systems.Existing techniques in this domain are designed to ensure the safety of neural networks.They employ verification methods based on formal specification and mathematical reasoning to analyze the properties of a systems or utilize adversarial testing methods from the perspective of system behavior to find potential errors,flaws,or violations.Research in this area is meaningful to discover vulnerabilities of neural networks,ensure the safety of model applications and develop safe and trustworthy artificial intelligence technology.However,research in the field of neural network safety analysis still faces several problems to be solved.Firstly,due to the large scale and non-convex nature of general neural networks,the verification of their properties has high complexity.Existing methods employ approximate approaches when constructing an abstract model of a neural network,which have low precision,and exhaustive exploration of the model leads to the problem of state space explosion.Secondly,the divide-and-conquer strategies in existing precise verification methods have not yet consider variations caused by model relevant factors,which leads to redundant exploration of sub-problems as it is difficult to reduce their solution spaces effectively.This limitation hampers the efficiency of safety analysis methods based on divide-and-conquer verification.Thirdly,safety analysis methods based on adversarial testing used in scenarios where model information and structure are not accessible have limited effectiveness of test cases and cannot achieve targeted local robustness analysis,making it difficult to realize sufficient assessment of the safety of neural networks.To address these critical issues,this thesis proposes a comprehensive framework for neural network safety analysis,which effectively addresses the state space explosion problem in neural network verification and enhances the effectiveness of test cases,and develop the corresponding safety analysis tools.The goal is to provide effective safety assurance for neural networks.The main contributions and innovations of this thesis are summarized as follows:(1)To address the issues that node boundaries are not tight enough caused by low precision of model abstraction methods and that divide-and-conquer strategies affect verification efficiency,this thesis proposes a neural network safety analysis method based on adaptive model abstraction and relaxed error partitioning.This method employs an adaptive symbolic linear relaxation algorithm to traverse neurons and obtain their upper and lower bounds,improving the boundary accuracy of nonlinear neurons in a neural network and consequently reducing the number of nonlinear neurons.This enhances the overall stability of neural networks while reducing the number of binary variables in Mixed-Integer Linear Programming(MILP)encoding.Furthermore,due to the hierarchical structure of a neural network which results in gradual accumulation and amplification of relaxation errors during network propagation,this method quantitatively analyzes relaxation errors and propagation effects,and proposes a heuristic divide-and-conquer strategy.By partitioning nodes with larger relaxation and propagation errors,the method decomposes a property verification problem into multiple sub-problems with more accurate relaxation boundaries.This further reduces the search space of sub-problems,thereby improving the efficiency of neural network verification.Experimental results show that compared to existing property verification methods,the proposed method improves verification efficiency by 37.18%.(2)To address the issue that the neglect of model factors of existing divide-and-conquer strategies leads to slow convergence of sub-problems,this thesis proposes a neural network safety analysis method based on neuron importance partitioning.This method initially adopts adversarial search and consistency check to rapidly determine whether the model satisfies the given property.It then recursively analyzes the impact of neurons on the optimization objective through backpropagation and uses it as a measure of their importance.Combined with the calculation of relaxation errors,it further optimizes the importance of nodes.The most critical neurons in the network are identified and partitioned,so that verification problem is divided into a set of sub-problems which are easier to solve.Through the neuron importance analysis,the resulting sub-problems have fewer nonlinear neurons,which leads to smaller search space,faster convergence and significantly reduced computational resource requirements.Additionally,the method introduces a solution space reduction technique based on consistency check,which further enhances verification efficiency.Experimental results show that compared to existing property verification methods,the proposed method can verify more safety properties,with an efficiency improvement of 44.8%.(3)Safety analysis methods based on adversarial testing can effectively complement verification methods in terms of scale and complexity.To address the issue that existing adversarial testing methods have limited effectiveness of test cases and cannot perform targeted local robustness testing in black-box scenarios,this thesis proposed a method based on saliency distribution and data augmentation to enhance the transferability of adversarial examples and improve the effectiveness of test cases.The main idea of the method is to guide the search direction of adversarial perturbations towards common vulnerable regions of the source model and the tested model,enhancing the ability of generated test cases to perform targeted local robustness testing on black-box models.To reduce the reliance on the source model,a model-agnostic feature extraction algorithm is used to compute the distribution of salient optimization perturbations on images.As the model’s decisions are sensitive to these features,changes in feature distribution can avoid falling into local extremum values of the source model,thereby the transferability of adversarial examples is enhanced.Furthermore,by performing ordered perspective transformations during the iterative process,the method effectively distorts the structure of input images to expand the image set within finite computations,mitigates the overfitting problem caused by perturbing individual images and thus achieves effective neural network safety analysis.Evaluation on a series of black-box defense models demonstrates that the proposed method increases the success rate in black-box model testing by 25.9%,further strengthening the safety analysis of black-box defense models.In summary,this thesis addresses three challenges in neural network safety analysis and provides corresponding theories and methods,formulating a new solution for trustworthy assurance of neural networks in safety-critical domains.