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

1 Introduction

Recurrent neural networks (RNNs) are widely used in reinforcement learning (RL) to handle partial observability and multiple agents [Aydeniz et al., 2024; Marchesini et al., 2025a]. Such RNN-based policies learn hidden-state dynamics that encode past observations and actions, making decision-making depend on the interaction history rather than only the current input. Verifying such policies is challenging, as most existing verification tools are designed for feedforward neural networks [Liu et al., 2021; Wei et al., 2025].

When applied to RNNs, verification is typically restricted to robustness analysis, where networks are checked over a single transition by bounding the effect of perturbations to a fixed input on the corresponding output. While effective for local robustness, this abstraction fails to capture the sequential and history-dependent nature of recurrent RL agents. In particular, assessing whether an RNN-based policy performs unsafe or undesired actions (or behaviors, interchangeably) requires reasoning about which hidden states can arise from feasible, policy-induced histories, that is, interactions the agent can actually encounter during execution (Fig. 1). Existing approaches addressing this challenge typically rely on explicit transition models to reason about recurrent policies, and verification remains computationally challenging even under these assumptions [Akintunde et al., 2019; Carr et al., 2021; Everett et al., 2021]. Moreover, these methods are limited in both scalability and expressivity: they fail to scale to multiple agents or high-dimensional spaces [Marchesini et al., 2025b; Marchesini et al., 2026], and often yield only binary certificates (e.g., safe or unsafe). Such binary outcomes are frequently uninformative in practice, as policies may differ substantially in how often violations occur across different feasible histories. In principle, sound verification of RNN-based policies would require enumerating all reachable hidden-state configurations during execution and checking whether any of them lead to undesired behavior. However, this requirement is equivalent to computing neural network preimage measures for which a desired behavior holds [Kotha et al., 2024; Zhang et al., 2024], a problem that is #P-hard due to the nonlinearity and nonconvexity of neural networks [Marzari et al., 2023a]. Hence, under standard complexity assumptions, obtaining an exact characterization of the feasible-history space is computationally infeasible. This observation suggests that, for recurrent policies in RL, exact worst-case verification is not only computationally prohibitive but also misaligned with the structure of history-dependent decision making.

These limitations motivate a probabilistic and quantitative perspective on verification for RNN-based policies. Rather than enumerating all feasible hidden states exactly, we aim to estimate the likelihood of undesired behavior by quantifying how much of the feasible-history space leads to behavioral violations under a trained policy. To this end, we introduce RNN Probabilistic Verification (RNN-ProVe), a probabilistic framework that approximates the policy-induced feasible hidden state space using policy-driven sampling with explicit statistical error bounds, and produces bounded-error, highconfidence verification certificates. At its core, RNN-ProVe learns a feasibility oracle that distinguishes feasible from infeasible hidden state representations with respect to the distribution of histories induced by the policy during training. The oracle is implemented as a classifier trained on feasible representations encoded by the policy. RNN-ProVe then performs quantitative verification over probabilistically feasible histories identified by the classifier. Additionally, we derive statistical confidence bounds to determine the required sample sizes for verification, ensuring that the resulting certificates have provable error bounds and high statistical confidence.

We evaluate RNN-ProVe on single-agent and cooperative multi-agent partially observable tasks, demonstrating that the framework scales to settings in which existing verification tools become overly conservative or inapplicable, while providing informative probabilistic assessments of behavioral risk. Our results suggest that probabilistic verification over feasible histories is not merely a heuristic relaxation, but a principled response to fundamental computational barriers.

These outcomes motivate the following contributions: (i) We formulate the problem of probabilistic verification of recurrent RL policies under partial observability, explicitly accounting for the set of hidden states that are feasible under a trained policy. (ii) We propose RNN-ProVe, a policy-driven probabilistic verification framework that combines feasibility learning with Monte Carlo estimation to quantitatively assess behavioral violations in RNN-based policies. (iii) We extend the problem to fully cooperative multi-agent RL (MARL) and derive bounded-error, high-confidence guarantees for feasible-history identification and violation estimation, yielding a tractable approximation to an otherwise #Phard verification problem.

More broadly, this work advocates probabilistic verification over feasible histories as a principled foundation for reasoning about safety and reliability in history-dependent decision-making systems.

2 Preliminaries and RelatedWork

At time t, an RNN produces an output yt by using a hidden state representation ht of an input sequence x = (x1↪ ▷ ▷ ▷ ↪ xt). Following the illustration of Fig. 2, the transition function for a vanilla RNN is ht = ω(Wxxt + Whht→1 + bh), where Wx↪Wh are the input and recurrent weight matrices, bh is a bias vector, and ω is typically a non-linear activation function. The output is derived via a linear transformation as yt = Wyht + by, where Wy is the output weight matrix and by is another bias vector. This recursive structure enables RNNs, as well as gated variants such as LSTMs [Hochreiter and Schmidhuber, 1997] and GRUs [Cho et al., 2014], to model temporal dependencies over input sequences.

RNNs in RL. In partially observable RL, an agent typically learns a policy ε : H → !(A); where H denotes the agent's action-observation history (o0↪ a0↪ ▷ ▷ ▷ ↪ ot→1), A is the set of actions modeling the RNN's output y, and o ↑ O are observations (i.e., RNN's input x) distributed following a stochastic transition function TO : S ↓A → !(O) (where O↪ S are the finite sets of observations and states, respectively) [ ˚Astr¨om, 1965]. In practice, at time t, ε uses the RNN's hidden state ht as a compressed history representation that depends on: (i) the previous hidden state ht→1; and (ii) the current observation ot, to output an action. 1 When tackling problems with N agents, we consider the setting where each agent i ↑ N has a local observation space Oi and conditions its policy on the local action-observation history [Oliehoek and Amato, 2016]. To achieve this decentralization, centralized training with decentralized execution (CTDE) is the de facto standard paradigm [Amato, 2024; Aydeniz et al., 2025]. In CTDE, agents leverage privileged information during training (including the state s ↑ S) while learning local history-based policies for execution [Papoudakis et al., 2021]. Similarly, RNN-ProVe accesses the state while keeping decentralized execution. Thus, our framework is consistent with established practice in partially observable RL.

RNN Verification. Although RNNs are commonly used in partially observable RL tasks, existing RNN verification methods are developed primarily for robustness analysis. Robustness verification certifies the stability of network outputs under bounded input perturbations over a fixed time horizon.

Without loss of generality, consider verifying an RNN with a single scalar output, where the robustness requirement is to ensure that the output satisfies a given input-output property [Liu et al., 2021]. Let f denote the RNN transition dynamics such that ht = f(ht→1↪ xt) for t ↑ ¶1↪ ▷ ▷ ▷ ↪ T♦, where T is the verification horizon. The property is encoded by appending a linear layer that outputs a margin value [Wang et al., 2021]. Specifically, the final output is defined as yT = c↑hT + by, where yT > 0 indicates that the property is satisfied. In more detail, let H0 = ¶h0♦ be the initial hidden state set and let X1:T = ¶X1↪ ▷ ▷ ▷ ↪XT♦ denote the admissible input sets, where each Xt = [xt ↪ xt] represents an ϑ↓-ball of radius ϖ around a nominal input. The over-approximated reachable hidden state sets are computed recursively as Ht = ¶f(h↪ x) ♣ h ↑ Ht→1↪ x ↑ Xt♦↪ and the corresponding output set is YT = ¶yT ♣ h ↑ HT♦. 2 Robustness verification then amounts to checking whether min(YT ) > 0. 3

Definition 1 (Robustness RNN-VERIFICATION).

Input: A tuple T = ↔f↪ H0↪ X1:T ↪ ε↗.

1 For simplicity, we use h↪ H for both histories and hidden states.

2 Reachability-based methods do not consider which hidden states can arise from feasible histories.

3 We provide a numerical example in Appendix 6.

Related Work. Several methods have been proposed for RNNs robustness verification. [Akintunde et al., 2019] unrolls the network over a finite time horizon, reducing it to a feedforward architecture. While effective, this strategy incurs exponential complexity in the horizon length. [Jacoby et al., 2020] infers inductive invariants over hidden states to remove explicit horizon dependence. However, synthesizing precise invariants for nonlinear networks is computationally difficult and often yields conservative results. To improve scalability, interval- and relaxation-based reachability analyses are used within branch-and-bound frameworks [Ko et al., 2019; Bunel et al., 2020; Xu et al., 2021; Mohammadinejad et al., 2021; Du et al., 2021; Tran et al., 2023; Marzari et al., 2025c]. These methods over-approximate reachable hidden states by assuming step-wise bounded input perturbations and targeting local robustness properties. Unlike robustness-based approaches that estimate output stability under bounded or stochastic input perturbations, our work quantifies how often undesired behaviors arise over the set of policy-induced feasible histories, addressing a fundamentally different source of uncertainty. This gap increases over long horizons, as over-approximation errors accumulate.

Beyond robustness, some works aim to verify recurrent policies. [Carr et al., 2021] propose extracting finite-state automata or abstract MDPs from trained RNN policies. While conceptually powerful, these approaches rely on discretization heuristics that scale exponentially with the dimensionality of the hidden state, restricting their applicability to smallscale RNNs. [Everett et al., 2021] perform backward reachability analysis directly in the state-action space. This method assumes full knowledge of the environment dynamics and deterministic transitions, assumptions that are rarely satisfied in complex, partially observable RL settings. Moreover, maintaining exact or even over-approximated reachable sets becomes intractable as the trajectory length increases.

Hence, existing approaches rely on strong modeling assumptions or suffer from severe scalability issues due to the combinatorial explosion inherent in abstracting continuous hidden state spaces. These problems highlight that current methods cannot effectively verify recurrent policies in RL.

3 RNN-Verification for RL

To verify RNN-based RL policies, we must move beyond input-perturbation-based RNN-VERIFICATION (Def. 1) and reason about uncertainty in the RNN's internal memory, namely the hidden state that encodes the agent's history. Specifically, instead of checking robustness against noisy inputs, we must verify actions over the set of feasible hidden states that could have arisen from past interactions. Hence, given an RNN-based policy f and the current observation o, our goal is to determine whether there exists any hidden state h, within the set of feasible ones H↔ ⇒ H up to o, such that f(h↪ o) leads to a violation of a desired behavior (e.g, an action that leads to an unsafe situation, such as colliding into an obstacle). We formally define this verification problem as:

Definition 2 (RNN-VERIFICATION for RL).

As in robustness verification, we assume that the behavior of interest can be expressed using a single scalar output whose sign indicates whether a violation occurs (i.e., the output is strictly positive if and only if the undesired action is not selected). This assumption can be enforced by appending a post-processing layer that encodes the action selection mechanism together with the desired behavioral constraint. In summary, Fig. 3 illustrates our verification problem, which checks whether there exists a feasible hidden state h ↑ H↔ such that, when combined with the current observation o, the RNN selects an action that violates a desired behavior.

In contrast to robustness, RNN-VERIFICATION for RL requires characterizing the set of feasible hidden states H↔ that reach a certain configuration (state). To this end, formal verification methods typically use coarse geometric overapproximations, such as independent intervals or hyperrectangles. However, as previously stated, these relaxations may admit spurious hidden states (i.e., combinations of hidden neuron values that cannot arise from any valid interaction history of an RL agent). As a result, propagating such inflated sets through the transition function f can yield spurious counterexamples, or false positives, that do not correspond to situations the agent can actually encounter. Sec. 3.1 discusses how RNN-ProVe addresses this issue.

Quantifying violations. Existing RNN verification tools typically return only a binary outcome and do not quantify the extent to which a trained RNN violates a desired requirement. In the context of RNN-based RL policies, this means that it is not possible to measure how much of the feasible hidden state space leads to violations of a desired behavior.

This limitation motivates our novel quantitative formulation, #RNN-VERIFICATION. In analogy with the feedforward network case [Kotha et al., 2024; Marchesini et al., 2023; Marzari et al., 2025a], we invert the analysis perspective. Rather than characterizing all the inputs of the RNN that lead to violating the desired behavior, we characterize the set of feasible hidden states (histories) that violate the behavior for a certain situation at time t (i.e., for a fixed input observation). This formulation enables explicit reasoning about uncertainty over feasible histories and yields a characterization of the region of hidden states that induce undesired behavior.

Definition 3 (#RNN-VERIFICATION for RL).

Input: A tuple T = ↔f↪H↪ o↗.

Output: V ol("(T )).

With "(T ) := ¶h ↑ H↔ ♣ f(h↪ o) ⇓ 0♦ ⇒ H the set of feasible histories for a fixed o that result in undesired behaviors.

Broadly speaking, the objective of this quantitative formulation is to compute the volume of "(T ) relative to Vol(H), which corresponds to the probability that the current policy exhibits an undesired behavior. We also note that exactly characterizing the feasible-history space H↔ is at least as hard as computing the volume of inputs that violate a behavior for a neural network, a problem known as #DNNVERIFICATION [Marzari et al., 2023a].

Theorem1. The #RNN-VERIFICATION problem is #P-hard.

In Appendix 7 we report a complete argument of this theoretical result. Under standard complexity assumptions, it implies that for any non-trivial RNN-based RL policy, obtaining an exact characterization of Vol("(T )) is computationally infeasible. This observation motivates our shift to a probabilistic perspective on verification, which we develop in Sec. 3.1.

Verifying Cooperative MARL. To the best of our knowledge, we now extend the previous problem formulations for the first time to fully cooperative MARL. We consider a setting in which a decentralized set of N agents must coordinate to achieve a shared objective. In this setting, each agent i ↑ N acts according to its own RNN-based policy fi, relying on its local observation oi and hidden state representation hi ↑ Hi. Considering the agents' common goal, we define verification of a cooperative MARL problem as the conjunction of individual desired-behavior constraints, meaning the system does not exhibit violations if every agent satisfies its individual desired behavior. Conversely, the system has violations if at least one agent violates its behavior. We formally define the verification problem for this setting as follows:

Definition 4 (RNN-VERIFICATION for MARL).

We thus extend the quantitative formulation of Def. 3 to the multi-agent domain. Due to our interest in fully cooperative MARL, we are interested in quantifying the agent with the highest probability of violations given its current local history. Therefore, the #RNN-VERIFICATION problem for MARL aims to compute the maximum volume of undesired feasible histories across all agents.

Since we adopt the standard decentralized setting in which each agent i acts based solely on its local information, the evaluation of V ol("(Ti)) for each agent is independent. The verification certificate is therefore determined by the worstperforming agent. This cooperative MARL formulation preserves tractability by decomposing into independent verification tasks, enabling parallel analysis without introducing additional conservatism. Accordingly, in the remainder of the paper, we present the proposed probabilistic framework and its theoretical guarantees for the single-agent case.

3.1 RNN-ProVe: a Novel Probabilistic Approach

Following the result in Theorem 1, RNN-ProVe solves a relaxed probabilistic version of the #RNN-VERIFICATION problem for RL. Intuitively, the following formalization asks for a scalar volume estimate that accurately approximates the volume measure of the true undesired set "(T ).

Definition 6 (Approximate #RNN-VERIFICATION for RL). Input: A tuple T = ↔f↪ H↪ o↗, an error tolerance ϱ ↑ (0↪ 1), and a confidence parameter ς ↑ (0↪ 1).

Output: ˜ V ↑ [0↪ V ol(H)] estimate of V ol("(T )), s.t.

This probabilistic problem definition requires that, with high confidence 1 ⇔ ς, the deviation between the estimated ˜ V and true volumes V ol("(T )), normalized by the total volume of the hidden space V ol(H), remains within the specified error bound ϱ. Since computing V ol("(T )) exactly is computationally prohibitive, an alternative strategy is to perform a Monte Carlo estimation as V ol("(T )) ↙ V ol(H) · 1k ∑ki=1 1f(hi↪o)↘0↪ where h1↪ ▷ ▷ ▷ ↪ hk are independent samples drawn from the hidden state domain H, and 1f(hi↪o)↘0 is the indicator function for undesired behaviors. However, this naive sampling strategy implicitly assumes that all histories within the domain H are feasible, while the set of feasible histories H↔ is a complex, lower-dimensional manifold within H. Consequently, a uniform sample from H inevitably includes unfeasible histories, leading to inaccurate verification results (as we will show in our experiments).

To address this issue, one would require an oracle that determines whether, for a given configuration (i.e., a state s ↑ S), a history h is feasible, meaning that it can be realized as an internal hidden state by ε. Since no exact analytical form of this oracle exists, RNN-ProVe leverages the universal approximation theorem [Hornik et al., 1989] to learn an approximation of this oracle, as illustrated in Fig. 4. In more detail, during RL training, the agent's policy explores a wide range of environment states s and generates corresponding internal hidden state representations of the actual histories leading to s. RNN-ProVe records these state-hidden state pairs to construct a dataset used to train a feasibility history classifier C : S ↓H → ¶0↪ 1♦. Specifically, given a state s and a hidden state h, the classifier predicts whether h corresponds to a feasible hidden state for the trained policy (phases 1 and 2 in the upper part of Fig. 4). This data collection process leverages maximum entropy-based RL exploration mechanisms, which, in our experiments, lead to a sufficient coverage of the hidden state space for our dataset [Kaelbling et al., 1996]. As a result, the dataset captures a wide variety of the feasible hidden state space, including both optimal and suboptimal but realizable interactions, which is essential for training a reliable feasibility classifier. Once the classifier C is trained, RNN-ProVe enters the quantitative verification phase (phase 3 in Fig. 4). For a given state of interest s where we want to verify a certain behavior, the method samples n candidate history vectors from the hidden state domain H and evaluates them using C. The classifier acts as a feasibility oracle, retaining only those representations h↔ that are predicted to be feasible hidden states of the RNN-based policy leading to state s. These validated histories are then used to evaluate the policy under the observation o associated with s. Hence, for each h ↑ h↔ , the method checks whether the action selected by the trained policy satisfies the desired behavior (i.e., selects a certain action), that is, whether f(h↪ o) > 0. If violations are observed, RNN-ProVe estimates the undesired volume ˜ V as the ratio of violating hidden states to the total number of validated hidden states tested.

The reliability of the resulting certificate depends on two sources of uncertainty: (i) the accuracy of the feasibility classifier, which determines whether the identified set faithfully represents the true feasible hidden state manifold without admitting spurious histories; and (ii) sampling variance, which depends on the number of validated hidden states used to estimate the undesired volume. RNN-ProVe addresses both sources of uncertainty through rigorous statistical analysis, providing high-confidence and bounded-error certificates.

3.2 Theoretical Guarantees

RNN-ProVe guarantees rely on decomposing the estimation error ϱ into two components: (i) the approximation error of the histories classifier; and (ii) the statistical variance of the safety evaluation (i.e., the sampling error). We bound both terms using Hoeffding's inequality [Hoeffding, 1963] to derive a global probabilistic certificate.

Lemma 1 (Hoeffding's inequality [Hoeffding, 1963]). Let X1↪ ▷ ▷ ▷ ↪ Xn be independent random variables such that Xi ↑ [0↪ 1], and let θ = E[Xi] and its estimate ˆθ = 1n ∑ni=1 Xi▷ Then, for any ϱ > 0, Pr(♣ˆθ ⇔ θ♣ ↖ ϱ) ⇓ 2 exp(⇔2nϱ2 ).

In our setting, let, without loss of generality, H ⇒ [0↪ 1]n be the hidden state domain and ϱ↪ ς ↑ (0↪ 1) be the total error tolerance and confidence parameters required by Def. 6. We distribute these budgets into classifier validation components (ˆ e↪ ϱclf ↪ ςclf) and verification components (ϱver↪ ςver), such that ϱ = ˆ e + ϱclf + ϱver and ς = ςclf + ςver.

Theorem 2 (RNN-ProVe Probabilistic Guarantees). Let ˆ p be the empirical probability of undesired behavior computed over N histories validated via the classifier C. Let ˆ e be the empirical error rate of C measured on a heldout validation set of size M. If the sample sizes satisfy N ↖ ln(2◁ωver) 2ε2ver and M ↖ ln(2◁ωclf) 2ε2clf , then the volume estimate ˜ V = V ol(H) · ˆ p computed by RNN-ProVe satisfies Pr (∣∣∣ ˜ V →V ol(!(T )) V ol(H) ∣∣∣ ⇓ ϱ) ↖ 1⇔ ς.

Proof. Let p↔ denote the true probability of undesired behavior (i.e., the V ol("(T ))◁V ol(H)) and pC denote the probability induced by the classifier C. We bound the total deviation ♣ˆ p ⇔ p↔ ♣ by applying the triangle inequality ♣ˆ p ⇔ p↔ ♣ ⇓ ♣ˆ p⇔pC♣+♣pC⇔p↔ ♣, representing the verification sampling and classifier error. To bound the classification error, we note that by applying Lemma 1, and enforcing that 2e→2Mε2clf ⇓ ςclf , we obtain a validation set of size M ↖ ln(2◁ωclf) 2ε2clf . By using this M we guarantee, with probability at least 1 ⇔ ςclf , that ♣pC ⇔p↔ ♣ ⇓ ϱclf ⇓ ϱclf + ˆ e. Analogously, ˆ p is a Monte Carlo estimate of pC obtained fromN independent samples. By applying once again Lemma 1, if N ↖ ln(2◁ωver) 2ε2ver we have that ♣ˆ p ⇔ pC♣ ⇓ ϱver, with probability at least 1 ⇔ ςver. By union bound, these inequalities hold simultaneously with probability at least 1 ⇔ (ςclf + ςver) = 1 ⇔ ς, giving ♣ˆ p ⇔ p↔ ♣ ⇓ ϱver + ˆ e+ϱclf = ϱ. Finally, substituting ˆ p = ˜ V Vol(H) and p↔ = V ol(!(T )) V ol(H) , we obtain Pr (∣∣∣ ˜ V Vol(H) ⇔ Vol(!(T )) Vol(H) ∣∣∣ ⇓ ϱ) ↖ 1⇔ς, concluding the argument.

This result shows that RNN-ProVe provides a boundederror, high-confidence certificate for the volume of hidden states violating the desired behavior, providing a solution to the approximate #RNN-VERIFICATION for RL problem.

For example, consider a target confidence of 1⇔ς = 99▷9% and an ϱ = 5% error in the certified violation volume. Suppose the classifier C achieves an empirical error rate of ˆ e = 0▷01 (i.e., 99% accuracy). We allocate the remaining error budget evenly between classifier validation and Monte Carlo estimation by setting ϱclf = 0▷02 and ϱver = ϱ⇔(ˆ e+ϱclf ) = 0▷02, with confidence parameters ςclf = ςver = ς◁2 = 5 · 10→4 . By Theorem 2, the required validation set size for the classifier and the sample histories for the verification are M↪N ↖ ln(2◁ω) 2ε2 = ln(2000) 2·0▷022 ↙ 10362. Hence, RNN-ProVe certifies the violation volume with 99▷9% confidence and a maximum error margin of 5% using ↙ 2 · 10362 total queries. Crucially, parallel execution on a GPU makes this computation take negligible time as shown in our experiments.

Limitations. While these guarantees are not restricted to discrete domains, extending RNN-ProVe to continuous settings requires identifying feasible hidden states when state and observation spaces are continuous. A natural extension, following standard practice in verification, is to discretize or quantize these spaces to obtain a finite abstraction over which feasibility can be learned and verified [Liu et al., 2021; Marzari et al., 2024; Marzari et al., 2026a]. An alternative is to approximate feasibility via conservative reachable-set approximations of the hidden-state dynamics. Exploring such extensions is left for future work. RNN-ProVe may also be less effective for very small problem instances or when the rate of undesired behavior is extremely low. In these cases, the number of samples required to achieve high statistical confidence may approach or exceed the number of feasible histories, making direct enumeration more appropriate. More generally, since the sample complexity scales as O(ϱ→2 ), estimating extremely rare violations (where p↔ → 0) requires very small error tolerances, leading to large sample requirements. This behavior reflects the complexity of the underlying counting problem rather than a limitation of our method.

4 Experiments

Our experiments address the following points: (i) Can RNN-ProVe verify recurrent policies in partially observable single- and cooperative multi-agent tasks? (ii) Does RNN-ProVe scale with problem complexity, in regimes where existing RNN verification methods become computationally intractable? (iii) How does RNN-ProVe compare to naive sampling baselines, and how does incorporating RNN-ProVe dataset affect the linearization-based baseline?

We evaluate RNN-ProVe on two classes of discrete environments: (i) single-agent navigation tasks of increasing size, with policies trained using the widely adopted DRQN algorithm [Hausknecht and Stone, 2017]; (ii) cooperative multiagent policies trained on the BoxPushing (BP) domain [Xiao et al., 2020], with increasing environment sizes, using the CTDE DRQN-based approach of [Xiao et al., 2020]. 4 Both environments are described in Fig. 5 and Appendix 8.

Since existing RNN verification tools are not designed to identify the feasible history space H↔ and would therefore require an external oracle for this purpose, we adapt the linearization-based RNN verification approach of [Ko et al., 2019] as a baseline for comparisonwithRNN-ProVe. In particular, we use the same feasibility oracle as in RNN-ProVe and perform an exact quantitative volume estimation. Employing the same feasibility oracle ensures a fair and controlled comparison. Our experiments thus aim to highlight the scalability limitations of exact solvers and the practical advantages of RNN-ProVe in challenging settings. Notably, both RNN-ProVe and the baseline are agnostic to the specific learning algorithm used to train the policies, as is standard in verification. In all experiments, the recurrent component of the policy is implemented using a GRU layer, selected for its strong empirical performance. Experiments are conducted on Xeon E5-2650 CPU nodes with 64GB of RAM. We verify 10 independently trained policies per task, collected at convergence. The following curves show the average return over the independent runs, smoothed over 100 episodes, with shaded regions indicating 95% confidence intervals. We also trained three independent feasibility classifiers with different random initializations; as the resulting verification estimates exhibited negligible variation, we report only the averaged results in Tab. 1. The environmental impact of the experiments is discussed in Appendix 10.

Desired Behaviors. For single-agent navigation, we verify collision-avoidance behaviors (Def. 3), where the agent should not select an action that leads to a collision (as in [Marzari et al., 2023b; Marzari et al., 2025b; Marzari et al., 2025d]). In the cooperative BP, we verify a joint behavior

4 Complete hyperparameters are reported in Appendix 9.

(Def. 5), requiring that both agents pick the push action when positioned in front of the box. These are designed to assess both individual and cooperative violations. At a highlevel, the resulting violation percentages can be interpreted as the likelihood that an agent exhibits undesired behavior when reaching a given state from arbitrary feasible histories, providing an indicator of policy generalization and robustness to history-dependent uncertainty, such as that induced by noisy or non-deterministic interactions.

4.1 Empirical Evaluation

Verification of RNN-based policies. RNN-ProVe verifies recurrent policies in all single-agent navigation and cooperative multi-agent BP. In navigation tasks, RNN-ProVe identifies non-trivial violation rates in smaller environments, with a mean violation of approximately 1% in the 4 ↓ 4 grid and approximately 13% in the 8↓8 grid (Table 1). In contrast, for the 16 ↓ 16 environment, RNN-ProVe reports low violation rates below 1% under the specified (ϱ↪ ς) guarantees.

Fig. 6 also visualizes the spatial distribution of violations for the 8 ↓ 8 environment. Despite strong training performance, the learned policies do not generalize uniformly across feasible hidden states. Specifically, the reported violation values correspond to the fraction of feasible histories from which the agent selects an action that eventually leads to a collision, revealing sensitivity to particular configurations near obstacles. These failures are not captured by standard empirical evaluations based on average return [Marzari et al., 2026b]. In the cooperative BP task, RNN-ProVe certifies mean violation values of approximately 1▷18% in the 10↓10 environment and approximately 1▷7% in the 20↓20 environment, demonstrating that the framework naturally extends to cooperative settings with interacting recurrent agents while providing quantitative, probabilistic safety assessments.

20≃20

99.23 ♣ 99.99

Table 1: Quantitative verification results for RNN-based navigation (Nav) and BP tasks. Gray rows correspond to the baselines; RNN-ProVe reports probabilistic certificates with bounded error ω and confidence at least 1 ↑ ε.

Scalability Consideration. Results in Tab. 1 highlight the scalability limitations of exact linearization-based RNN verification when applied to recurrent RL policies. In navigation, the baseline requires several minutes of computation to verify the small 4 ↓ 4 environment, increases its runtime to over 18 minutes in the 8↓8 setting, and fails to complete the 16↓16 task within the imposed 45-minute timeout. This behavior reflects the rapid growth of exact over-approximationbased RNN verification methods as both the environment size and the GRU hidden state dimension increase. In contrast, RNN-ProVe scales efficiently across all tasks, returning quantitative verification results (comparable with the baseline) in milliseconds. This efficiency stems from reasoning probabilistically over feasible histories. Moreover, existing RNN verification methods are not designed to handle cooperative multi-agent formulations and therefore cannot be directly applied to the BP task. In these settings, RNN-ProVe enables probabilistically quantitative verification of recurrent policies under decentralized execution, demonstrating its applicability beyond single-agent scenarios.

Ablation Study. We report two additional experimental variants for the navigation tasks in Table 1. For the 4 ↓ 4 environment, we compare baseline results obtained with an exact feasibility oracle to those obtained with the approximate feasibility oracle learned by RNN-ProVe. In this environment, where an exact oracle is achievable, we notice that the verification results are nearly identical, indicating that the histories collected during training already cover a large portion of the feasible history space. When used within the RNN-ProVe pipeline, this data enables learning a feasibility classifier that closely approximates the true feasible-history distribution. We also compare our approach against a naive Monte-Carlo variant that removes the feasibility classifier and evaluates the policy on uniformly sampled hidden states. This leads to substantially higher violation rates, as most sampled hidden states do not correspond to realizable interaction histories and therefore induce spurious failures when fed into the policy. Overall, these experiments rule out two natural alternatives: naive linearization and bound-propagation-based hidden-state bound estimation, as well as naive Monte Carlo estimation without feasibility filtering. They further show that the proposed components are not only necessary to verify histories arising under policy execution, but also sufficient to produce accurate probabilistic estimates of behavioral violations. By operating over feasible combinations of hiddenstate features, RNN-ProVe computes violation values that reliably reflect the true behavior of the policy.

5 Discussion

We presented RNN-ProVe, a probabilistic verification framework for recurrent policies in single- and cooperative multi-agent RL. RNN-ProVe addresses the challenge of reasoning over feasible histories, which is not captured by existing RNN verification methods. By combining policydriven sampling with statistical analysis, we produce quantitative, high-confidence certificates that estimate how frequently undesired behaviors occur over feasible hidden states. RNN-ProVe enables scalable analysis in regimes where exact methods become intractable.

A key insight emerging from our analysis is that verification precision is governed not by tighter bounds, but by accurately capturing the combinatorial structure of feasible hidden state configurations induced by policy execution.

Acknowledgements

This work was supported in part by the "Fondo Italiano per la Scienza" project (FIS-2024-05614), and in part by the Austrian Science Fund (FWF) project 10.55776/ESP1944725, the Vienna Science and Technology Fund (WWTF) under Grant ICT22-023 (TAIGER) and the European Union, RobustifAI project, ID 101212818. The authors thank the reviewers for their insightful and constructive feedback, which has substantially improved the quality of this work.