# Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 41 references that are in the map.
- First posted on arXiv 14 May 2026.

## Builds on (most cited first, 27 of 27)

- [On the Properties of Neural Machine Translation: Encoder-Decoder Approaches](https://mlsanity.com/paper/1409.1259/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Deep Recurrent Q-Learning for Partially Observable MDPs](https://mlsanity.com/paper/1507.06527/) (2015)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Benchmarking Multi-Agent Deep Reinforcement Learning Algorithms in Cooperative Tasks](https://mlsanity.com/paper/2006.07869/) (2020)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An Introduction to Centralized Training for Decentralized Execution in Cooperative Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2409.03052/) (2024)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [POPQORN: Quantifying Robustness of Recurrent Neural Networks](https://mlsanity.com/paper/1905.07387/) (2019)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Verifying Recurrent Neural Networks using Invariant Inference](https://mlsanity.com/paper/2004.02462/) (2020)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Macro-Action-Based Deep Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2004.08646/) (2020)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [DiffRNN: Differential Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2007.10135/) (2020)
- [Safe Deep Reinforcement Learning by Verifying Task-Level Properties](https://mlsanity.com/paper/2302.10030/) (2023)
- [RL2Grid: Benchmarking Reinforcement Learning in Power Grid Operations](https://mlsanity.com/paper/2503.23101/) (2025)
- [Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation](https://mlsanity.com/paper/2302.06695/) (2023)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Improving Policy Optimization via varepsilon-Retrain](https://mlsanity.com/paper/2406.08315/) (2024)
- [On Stateful Value Factorization in Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2408.15381/) (2024)
- [Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation](https://mlsanity.com/paper/2505.05235/) (2025)
- [Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation](https://mlsanity.com/paper/2504.21643/) (2025)
- [On the Probabilistic Learnability of Compact Neural Network Preimage Bounds](https://mlsanity.com/paper/2511.11656/) (2025)

## Abstract (arXiv)

History-dependent policies induced by recurrent neural networks (RNNs) rely on latent hidden state dynamics, making verification in partially observable reinforcement learning (RL) challenging. Existing RNN verification tools typically rely on restrictive modeling assumptions or coarse over-approximations of the hidden state space, which can lead to overly conservative or inconclusive results. We propose RNN Probabilistic Verification (textttRNN-ProVe), a probabilistic framework that textitestimates the likelihood of undesired behaviors in RNN-based policies. textttRNN-ProVe uses policy-driven sampling to approximate the set of hidden states that are feasible under a trained policy, and derives statistical error bounds to produce bounded-error, high-confidence estimates of behavioral violations. Experiments on partially observable single-agent and cooperative multi-agent tasks show that textttRNN-ProVe yields more quantitative, feasibility-aware probabilistic guarantees than existing tools, while scaling to recurrent and multi-agent settings.