An Efficient Abstraction Method For Neural Network Verification

In recent years,with the rapid development of deep learning theory,artificial intelligence has been increasingly applied in various fields.When people gradually use deep learning in safety critical fields,such as unmanned driving and aircraft collision avoidance systems,the verification of system safety related properties becomes a very important task.Therefore,many neural network verification methods have been proposed,however,most of them suffer from poor scalability and thus are difficult to apply them to larger scale neural networks.New research has shown that abstraction methods can solve the problem of poor scalability of neural network verification methods.Using this method,an abstract deep neural network of smaller size can be generated.However,current abstraction methods suffer from one or more of the following problems: excessive output errors,lack of reasonable abstraction strategies,and lack of corresponding refinement strategies.To address the above shortcomings,this paper proposes an efficient abstraction method including the following contribution points.1.We have proposed the definition of the merge operator for abstraction,including the definition of the forward merge operation and the backward merge operation.The use of this merge operator can effectively reduce the output error of the abstraction neural network while ensuring the reliability.2.A heuristic dynamic selection merging strategy for abstraction is proposed,which is based on the calculated values of the edge weights in the merging operator to preferentially select the merge.The dynamic strategy ensures a wider range of neural network abstraction and further reduces the output error of the abstract neural network using this strategy.In this paper,we show that the neural network obtained by using our abstraction method satisfies the over-approximation property,which guarantees the reliability of the abstraction method.3.The proposed abstraction method corresponds to a refinement operation,which may introduce behaviors that do not exist in the neural network,i.e.,when the verification returns a counterexample,this counterexample may be a pseudo-counterexample,so a certain refinement operation is needed.The refinement operation in this paper is based on the merge operator and the heuristic strategy mentioned above,and the refinement operation can effectively deal with more cases.Combining the above three points,this paper proposes a more systematic and complete neural network abstraction method,and designs experiments to evaluate the effectiveness from several perspectives.