Research On Neural Network Verification Algorithm Based On Reachability Analysis And Optimization

With the continuous upgrading of mathematical and computer technologies,neural network has also been vigorously developed and been more widely used in various industries,especially in safety-critical areas such as aircraft collision avoidance,medical diagnosis,and autonomous driving.Every miscalculation of neural networks in these fields can lead to serious safety problems.However,neural networks are naturally uncertain and often give wrong judgments for inputs with minor adversarial or even accidental perturbations.Therefore there is an urgent need for a method that can rigorously check whether a neural network violates the given safety properties.In contrast,formal methods can effectively improve the reliability of the system by modeling and verifying the hardware and software system strictly according to mathematical logic with the help of mathematical notation.How to use formal methods to verify neural network in order to improve the security of neural network has become a hot research topic nowadays.Formal verification of neural networks is still a long way from practical application.The current methods for formal verification of neural networks can be divided into two categories: reachability analysis and optimization.The methods based on reachability analysis analyze the network layer by layer and finally calculate the reachable range.This approach generally approximate the entire network,reducing accuracy in exchange for verification speed,so reachability analysis is not a complete algorithm because it does not necessarily return a deterministic result.The methods based on optimization encode the entire network and use optimization to verify the network.This approach is complete and generally gives a safe or unsafe deterministic result.However,there is the problem that scalability is too poor and a simple problem may consume a lot of time.This paper improves the reachability analysis method and the optimization method based on mixed integer linear programming,and proposes a refined symbolic linear relaxation algorithm based on node errors and a branch and bound algorithm based on node dependence.The refined symbolic linear relaxation algorithm based on node error uses symbols to propagate during the layer-by-layer analysis,preserving the input relations between nodes.For nodes that cannot continue linear propagation,linear approximation is performed using an efficient approximation method.And the nodes with the most errors introduced in the propagation process are refined so that the range of nodes obtained is tighter.The branch and bound algorithm based on node-dependence uses the dependency relationship between nodes to find out the nodes with the highest dependency degree for branching,thus fixing more nodes and reducing the state space of the solver.Meanwhile,based on the two proposed algorithms,this paper implements a complete verification tool,FFNNV,which retains the completeness of the optimization method and utilizes the reachability analysis method to achieve better scalability.Finally,this paper designs multi-level and multi-angle comparison experiments to analyze the proposed method and the neural network verification tool.The experiment results show that both the refined symbolic linear relaxation algorithm based on node error and the branch delimitation algorithm based on node dependencies can effectively improve the efficiency and scalability of the tool.