# Verifying Recurrent Neural Networks using Invariant Inference

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Apr 2020.

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

- [Causality-based Neural Network Repair](https://mlsanity.com/paper/2204.09274/) (2022)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Certified Robustness to Programmable Transformations in LSTMs](https://mlsanity.com/paper/2102.07818/) (2021)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [Probabilistic Verification of Neural Networks Against Group Fairness](https://mlsanity.com/paper/2107.08362/) (2021)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [On Recurrent Neural Networks for learning-based control: recent results and ideas for future developments](https://mlsanity.com/paper/2111.13557/) (2021)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [RoMA: a Method for Neural Network Robustness Measurement and Assessment](https://mlsanity.com/paper/2110.11088/) (2021)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [Toward the Analysis of Graph Neural Networks](https://mlsanity.com/paper/2201.00115/) (2022)
- [Model-Agnostic Reachability Analysis on Deep Neural Networks](https://mlsanity.com/paper/2304.00813/) (2023)
- [Permutation Invariance of Deep Neural Networks with ReLUs](https://mlsanity.com/paper/2110.09578/) (2021)
- [Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach](https://mlsanity.com/paper/2311.12130/) (2023)
- [LTL Verification of Memoryful Neural Agents](https://mlsanity.com/paper/2503.02512/) (2025)
- [Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2605.14758/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [Bounded Reachability & Jailbreak Detection via Contraction-Constrained State Space Models](https://mlsanity.com/paper/2610.02853/) (2026)

## Abstract (arXiv)

Deep neural networks are revolutionizing the way complex systems are developed. However, these automatically-generated networks are opaque to humans, making it difficult to reason about them and guarantee their correctness. Here, we propose a novel approach for verifying properties of a widespread variant of neural networks, called recurrent neural networks. Recurrent neural networks play a key role in, e.g., natural language processing, and their verification is crucial for guaranteeing the reliability of many critical systems. Our approach is based on the inference of invariants, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems. Experiments with a proof-of-concept implementation of our approach demonstrate that it performs orders-of-magnitude better than the state of the art.