Scalable Polyhedral Verification of Recurrent Neural Networks

TL;DR

This paper introduces Prover, a scalable and precise verification tool for recurrent neural networks that uses novel polyhedral abstractions and gradient descent refinement, enabling certification of complex models in speech, vision, and sensor data.

Contribution

Prover is the first scalable verifier for recurrent neural networks that combines sampling, optimization, and Fermat's theorem for polyhedral abstraction, and employs gradient descent for refinement.

Findings

Successfully verifies challenging recurrent models in vision, speech, and sensor data.

Outperforms prior work in verifying complex neural network models.

Develops custom abstractions for nonlinear speech preprocessing.

Abstract

We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and nonlinear recurrent update functions by combining sampling, optimization, and Fermat's theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.