Specification-Guided Safety Verification for Feedforward Neural Networks
This addresses safety verification for neural networks, which is crucial for deploying them in safety-critical applications, though it appears incremental as it builds on existing interval analysis approaches.
The paper tackles the problem of safety verification for feedforward neural networks by developing a specification-guided method that reduces computational cost through interval analysis and bisection processes. Experiments show the method achieves significantly more efficiency with much less computational cost.
This paper presents a specification-guided safety verification method for feedforward neural networks with general activation functions. As such feedforward networks are memoryless, they can be abstractly represented as mathematical functions, and the reachability analysis of the neural network amounts to interval analysis problems. In the framework of interval analysis, a computationally efficient formula which can quickly compute the output interval sets of a neural network is developed. Then, a specification-guided reachability algorithm is developed. Specifically, the bisection process in the verification algorithm is completely guided by a given safety specification. Due to the employment of the safety specification, unnecessary computations are avoided and thus the computational cost can be reduced significantly. Experiments show that the proposed method enjoys much more efficiency in safety verification with significantly less computational cost.