An Improved Interval Neural Network Abstraction Method

In recent years,deep learning has been developing vigorously and has achieved outstanding performance in many complex tasks.Therefore,researchers have begun to try to apply deep learning to safety-critical systems,such as autonomous driving and aircraft collision avoidance.However,there is no mature method for the verification of the safety properties of deep learning.And many existing methods have the problem of low scalability.Abstracting neural networks is an effective way to improve the scalability of the verification method.Abstracting deep neural networks into interval neural networks is a new abstraction technique proposed in recent years.Interval neural network is a type of neural network whose parameters are all intervals instead of values.It can be constructed by merging neurons in a deep neural network.The constructed interval neural network can be regarded as an abstraction of the original deep neural network,which has fewer parameters than the original network.So this technique can improve the efficiency and scalability of the verification method.However,the existing interval neural network abstraction technology still faces the problem of inaccuracy.This thesis proposes an abstraction method based on interval neural network.This method includes a new set of neuron merging rules.According to the weights of neurons,the merging is divided into four categories with different rules,so that the accuracy of the constructed interval neural network is greatly improved.This thesis also proposes a heuristic neuron selection strategy,estimating the similarity between each pair of neurons to decide which pairs of neurons to merge.The strategy further improve the accuracy of abstraction.For the obtained interval neural network,mixed integer linear programming is used to construct constraints to compute the output reachable set.This thesis modifies the existing two mixed-integer linear programming methods used in deep neural network verification so that they can be used to calculate the output reachable set of interval neural networks.Then we compare the performance of the two methods.To evaluate the effectiveness of the methods involved in this thesis,we designed multi-level comparative experiments.Experimental results show that both the new merging rules and the heuristic neuron selection strategies can effectively improve the accuracy of the abstraction.