Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning
For researchers and practitioners in reinforcement learning, this work addresses the challenge of verifying recurrent neural network policies in partially observable environments, offering a more practical and scalable verification approach.
RNN-ProVe estimates the likelihood of undesired behaviors in RNN-based policies for partially observable RL, providing bounded-error, high-confidence probabilistic guarantees that outperform existing tools in both single and multi-agent settings.
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 $\textbf{RNN}$ $\textbf{Pro}$babilistic $\textbf{Ve}$rification ($\texttt{RNN-ProVe}$), a probabilistic framework that $\textit{estimates the likelihood}$ of undesired behaviors in RNN-based policies. $\texttt{RNN-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 $\texttt{RNN-ProVe}$ yields more quantitative, feasibility-aware probabilistic guarantees than existing tools, while scaling to recurrent and multi-agent settings.