Fully Automatic Neural Network Reduction for Formal Verification
This addresses the problem of slow formal verification for neural networks in safety-critical domains, representing a novel method for a known bottleneck.
The paper tackles the scalability challenge in formally verifying neural networks for safety-critical applications by introducing a fully automatic and sound reduction method using reachability analysis, which reduces large networks to a fraction of their original neuron count and similarly shortens verification time.
Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems under strict time constraints. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. Our sound reduction approach is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specification. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach reduces large neural networks to a fraction of the original number of neurons and thus shortens the verification time to a similar degree.