Neuron importance based verification of neural networks via divide and conquer

Neural networks are widely used in various applications such as image classification, speech recognition and natural language processing. As intelligent systems often rely on neural networks to make critical decisions, it is crucial to ensure that the behavior of a neural network is trustworthy. Along with the increase in the scale and complexity of neural networks, it becomes a challenging problem to verify their safety, since the large-scale state space may make the verification of safety properties infeasible or unsolvable. In order to achieve efficient safety verification of neural networks, this paper proposes a divide-and-conquer verification method based on neuron importance analysis. The method converts the safety constraints to be verified into an optimization problem composed of output neurons, and recursively measures the influence of neurons in the network on the final objective function to calculate their importance. The neurons with the greatest importance are split to refine the constraints, so that the original verification problem is transformed into a set of sub-problems for solution. The method is implemented as a tool named NIAVerify, which is evaluated through experiments of property verification on ReLU-based fully-connected benchmark networks trained on two classic datasets. Experimental results show that NIAVerify can achieve significant state space reduction and the verification efficiency is 44.80% higher than the existing verification method.