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.