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

TL;DR

RNN-ProVe is a probabilistic verification framework that estimates the likelihood of undesirable behaviors in RNN-based policies for partially observable reinforcement learning, providing scalable, high-confidence guarantees.

Contribution

It introduces a novel probabilistic approach that overcomes limitations of existing tools by using policy-driven sampling and statistical bounds for RNN verification in complex RL settings.

Findings

Provides more quantitative probabilistic guarantees than existing methods.

Scales effectively to recurrent and multi-agent reinforcement learning tasks.

Offers bounded-error, high-confidence estimates of behavioral violations.

Abstract

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.