In the robustness verification of neural networks, formal methods have been used to give deterministic guarantees for neural networks. However, recent studies have found that the verification method of single-neuron relaxation in this field has an inherent convex barrier that affects its verification capability. To address this problem, we propose a new verification method by combining dual-neuron relaxation and linear programming. This method captures the dependencies between different neurons in the same hidden layer by adding a two-neuron joint constraint to the linear programming model, thus overcoming the convex barrier problem caused by relaxation for only a single neuron. Our method avoids the combination of exponential inequality constraints and can be computed in polynomial time. Experimental results show that we can obtain tighter bounds and achieve more accurate verification than single-neuron relaxation methods.

The verification techniques based on formal methods can provide deterministic guarantees for the robustness of Deep Neural Networks(DNNS). However, the enormous scale of DNNS makes the application of such methods in this field a huge challenge. To address this problem, this study proposes a single-sample sub-network pruning method, which can identify redundant nodes by combining neuron coverage and the symbolic interval propagation method to reduce the network verification scale. In addition, to solve the problem of too many sub-networks to be pruned, according to the similarity of neuron coverage between samples, we propose a corresponding clustering algorithm to establish sub-networks for different categories of samples to improve the verification efficiency. We combine the MIPverify verification tool to validate the above method. Experiments show that the sub-networks can give the same robust validation results and similar robustness bounds as the original network, while greatly reducing the validation time and network size.