Understanding and Enhancing Neural Network Verification Performance

With the rapid progression of machine learning, large-scale neural network models are being extensively implemented in safety-critical domains. Researchers have devised various techniques to evaluate the behaviors of these systems. One widely recognized approach involves using formal methods to validate or invalidate specifications that express desirable properties of system behaviors. Over the past six years, the neural network verification (NNV) community has developed more than 50 methods. Nevertheless, the community faces a challenge in generating benchmarks to effectively assess these approaches. Furthermore, the complexity of neural network models is growing at a much faster pace than the scalability of neural network verifiers. Therefore, there is a need for research on scaling NNV to apply them to real-world neural networks.
Understanding the performance characteristics of various NNV tools is crucial for their effective applications in practical scenarios and for the advancement of current methodologies. This dissertation focuses on two primary phases: understanding and enhancing the performance of NNV. In the initial phase, we introduce innovative automated approaches to systematically create diverse benchmarks for assessing existing verifiers, exploring their performance boundaries, and identifying bottlenecks. In the second phase, we effectively enhance the scalability of state-of-the-art neural network verifiers by addressing the recognized bottleneck known as “neuron stability.” This is achieved by guiding the training process to produce neural networks with fewer unstable neurons; and by improving an existing verifier to stabilize neurons during the verification process, thereby significantly reducing the search space. The research conducted in this dissertation has led to the development of six open-source software artifacts for future research and development in the field.