Scalable Polyhedral Verification of Recurrent Neural Networks
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.
Code (1)
Similar Papers 제목 키워드 기반
Scaling Polyhedral Neural Network Verification on GPUs
Certifying the robustness of neural networks against adversarial attacks is essential to their reliable adoption in safety-critical systems such as autonomous driving and medical diagnosis. Unfortunately, state-of-the-ar…
Autonomous DrivingGPUMedical DiagnosisTIRAMISU: A Polyhedral Compiler for Dense and Sparse Deep Learning
In this paper, we demonstrate a compiler that can optimize sparse and recurrent neural networks, both of which are currently outside of the scope of existing neural network compilers (sparse neural networks here stand fo…
Deep Learningtensor algebraSTR-Cert: Robustness Certification for Deep Text Recognition on Deep Learning Pipelines and Vision Transformers
Robustness certification, which aims to formally certify the predictions of neural networks against adversarial inputs, has become an integral part of important tool for safety-critical applications. Despite considerable…
Scene Text RecognitionAbstraction-based Probabilistic Stability Analysis of Polyhedral Probabilistic Hybrid Systems
In this paper, we consider the problem of probabilistic stability analysis of a subclass of Stochastic Hybrid Systems, namely, Polyhedral Probabilistic Hybrid Systems (PPHS), where the flow dynamics is given by a polyhed…
Robustness Verification of Recurrent Neural Networks with Abstraction Refinement
Certified local robustness verification for recurrent neural networks (RNNs) is challenging because approximation errors introduced by nonlinear relaxations can propagate through recurrent connections and accumulate over…