Scalable Polyhedral Verification of Recurrent Neural Networks

Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Dan, Martin Vechev

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 non-linear 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.
Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
Subtitle of host publication33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
EditorsAlexandra Silva, K. Rustan Leino
Number of pages24
ISBN (Electronic)978-3-030-81685-8
ISBN (Print)978-3-030-81684-1
StatePublished - Jul 15 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12759 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Abstraction refinement
  • Long short-term memory
  • Polyhedral abstraction
  • Recurrent neural networks
  • Robustness verification
  • Speech classifier verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Scalable Polyhedral Verification of Recurrent Neural Networks'. Together they form a unique fingerprint.

Cite this