A Survey on the Verification of Reinforcement Learning Policies
06:00 · July 21, 2026 · arXiv cs.AI RSS
Reinforcement learning (RL) is increasingly applied in complex, safety-critical domains, yet the lack of rigorous behavioral guarantees for neural network-based policies remains a major barrier to deployment. Recent advances in policy expressiveness and scale have intensified this challenge, leading to a rapidly growing but conceptually fragmented body of work on RL policy verification. This survey provides a unifying perspective on RL verification methods. We introduce a taxonomy that clarifies relationships among existing approaches along three axes: verification paradigm (formal versus probabilistic), temporal scope (step-wise versus multi-step), and guarantees strength. Beyond taxonomy, we unify underlying theoretical foundations, make implicit assumptions and limitations explicit, and identify emerging directions.
Summary
Reinforcement learning policies, typically implemented as deep neural networks, are increasingly considered for safety-critical applications such as autonomous driving and energy management. Their closed-loop interaction with environments introduces risks of error accumulation, distribution shift, and failures that appear only over extended horizons, which standard empirical testing cannot fully exclude. This survey addresses the resulting need for post-training verification by organizing a fragmented literature into a single taxonomy.
The taxonomy classifies methods along three dimensions: verification paradigm, distinguishing formal techniques based on satisfiability or reachability from probabilistic approaches that quantify risk; temporal scope, separating step-wise checks from multi-step analyses that capture longer trajectories; and guarantee strength, ranging from sound and complete certificates to weaker probabilistic or partial assurances. The authors apply this structure to existing solvers and abstractions, including bound propagation, abstract interpretation, SMT-based reasoning, neural Lyapunov functions, and control-barrier methods, while clarifying the assumptions each approach makes about policy architecture and environment dynamics.
Beyond classification, the survey traces the shift from purely local, step-wise robustness checks toward enumeration of unsafe state regions and multi-step verification that accounts for policy-environment coupling. It also examines hybrid neuro-symbolic techniques that combine learned policies with formal control constructs. Persistent limitations are noted for recurrent policies, whose internal state complicates reachability analysis, and for multi-agent settings, where interaction effects further increase verification complexity. The work concludes by outlining open directions for scaling guarantees to larger, more expressive models in deployment-critical domains.
Why it matters
The survey is highly relevant for Dutch AI researchers and practitioners focusing on trustworthy and transparent AI, aligning perfectly with EU regulatory demands for verifiable AI systems. It provides a structured foundation for teams developing safety-critical RL applications in sectors like energy and autonomous systems.
