Deep neural networks (DNNs) have become integral to numerous safety-critical applications, necessitating rigorous verification of their trustworthiness. However, the problem of verifying DNNs has high computational complexity, and existing techniques have limited efficiency, insufficient to deal with large-scale network models. To address this challenge, we propose a novel abstraction-refinement verification method that reduces network size while maintaining verification accuracy. Specifically, the method quantifies the similarity between neurons based on various factors such as their interval outputs, and then merges similar neurons to generate a smaller abstract network. In addition, a counterexample-guided refinement process is developed to mitigate the impact of potential spurious counterexamples, so that verification results from the abstract network are applicable to the original network. We have implemented this method as a tool named ARVerifier and integrated it with three state-of-the-art verification tools for evaluation on ACAS Xu and MNIST benchmarks. Experimental results demonstrate that ARVerifier significantly reduces network size and yields verification time reductions by 11.61%, 18.70%, and 12.20% compared to α,β-CROWN, Verinet, and Marabou, respectively. Moreover, ARVerifier exhibits efficiency improvements by 26.64% and 46.87% compared to existing abstraction-refinement methods NARv and CEGAR-NN, respectively.
Liu et al. (Mon,) studied this question.