# Scalable Polyhedral Verification of Recurrent Neural Networks

arXiv: https://arxiv.org/abs/2005.13300 · HTML: https://mlsanity.com/paper/2005.13300/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 May 2020.

## Built on by (most cited first, 20 of 20)

- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [A Survey of Adversarial Defences and Robustness in NLP](https://mlsanity.com/paper/2203.06414/) (2022)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Robust Natural Language Processing: Recent Advances, Challenges, and Future Directions](https://mlsanity.com/paper/2201.00768/) (2022)
- [LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions](https://mlsanity.com/paper/2201.13351/) (2022)
- [Localized Randomized Smoothing for Collective Robustness Certification](https://mlsanity.com/paper/2210.16140/) (2022)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [Boosting Robustness Verification of Semantic Feature Neighborhoods](https://mlsanity.com/paper/2209.05446/) (2022)
- [Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone](https://mlsanity.com/paper/2211.09810/) (2022)
- [Verification of Neural Networks Local Differential Classification Privacy](https://mlsanity.com/paper/2310.20299/) (2023)
- [STR-Cert: Robustness Certification for Deep Text Recognition on Deep Learning Pipelines and Vision Transformers](https://mlsanity.com/paper/2401.05338/) (2023)
- [Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification](https://mlsanity.com/paper/2511.11699/) (2025)
- [Distribution and Clusters Approximations as Abstract Domains in Probabilistic Abstract Interpretation to Neural Network Analysis](https://mlsanity.com/paper/2603.25273/) (2026)
- [Robustness Verification of Recurrent Neural Networks with Abstraction Refinement](https://mlsanity.com/paper/2606.12490/) (2026)
- [Shifting-based Optimizable Linear Relaxations for General Activation Functions](https://mlsanity.com/paper/2606.20292/) (2026)

## Abstract (arXiv)

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.