# Verified Probabilistic Policies for Deep Reinforcement Learning

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 50 references that are in the map.
- First posted on arXiv 10 Jan 2022.

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

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Asynchronous Methods for Deep Reinforcement Learning](https://mlsanity.com/paper/1602.01783/) (2016)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Deep Reinforcement Learning for Robotic Manipulation with Asynchronous Off-Policy Updates](https://mlsanity.com/paper/1610.00633/) (2016)
- [Reinforcement Learning in Healthcare: A Survey](https://mlsanity.com/paper/1908.08796/) (2019)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [Learning to Drive in a Day](https://mlsanity.com/paper/1807.00412/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Learning to be Safe: Deep RL with a Safety Critic](https://mlsanity.com/paper/2010.14603/) (2020)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Agent Modelling under Partial Observability for Deep Reinforcement Learning](https://mlsanity.com/paper/2006.09447/) (2020)
- [Cautious Reinforcement Learning with Logical Constraints](https://mlsanity.com/paper/2002.12156/) (2020)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Verifiably Safe Exploration for End-to-End Reinforcement Learning](https://mlsanity.com/paper/2007.01223/) (2020)
- [Feasible Actor-Critic: Constrained Reinforcement Learning for Ensuring Statewise Safety](https://mlsanity.com/paper/2105.10682/) (2021)
- [Logically-Constrained Neural Fitted Q-Iteration](https://mlsanity.com/paper/1809.07823/) (2018)
- [Probabilistic Guarantees for Safe Deep Reinforcement Learning](https://mlsanity.com/paper/2005.07073/) (2020)
- [Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems](https://mlsanity.com/paper/1901.01576/) (2019)
- [Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report)](https://mlsanity.com/paper/2112.09655/) (2021)
- [Approximate Abstractions of Markov Chains with Interval Decision Processes (Extended Version)](https://mlsanity.com/paper/1804.08554/) (2018)
- [Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning](https://mlsanity.com/paper/2106.06931/) (2021)

## Built on by (most cited first, 6 of 6)

- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [A Dynamical Systems Framework for Reinforcement Learning Safety and Robustness Verification](https://mlsanity.com/paper/2508.15588/) (2025)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance](https://mlsanity.com/paper/2603.07546/) (2026)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

Deep reinforcement learning is an increasingly popular technique for synthesising policies to control an agent's interaction with its environment. There is also growing interest in formally verifying that such policies are correct and execute safely. Progress has been made in this area by building on existing work for verification of deep neural networks and of continuous-state dynamical systems. In this paper, we tackle the problem of verifying probabilistic policies for deep reinforcement learning, which are used to, for example, tackle adversarial environments, break symmetries and manage trade-offs. We propose an abstraction approach, based on interval Markov decision processes, that yields probabilistic guarantees on a policy's execution, and present techniques to build and solve these models using abstract interpretation, mixed-integer linear programming, entropy-based refinement and probabilistic model checking. We implement our approach and illustrate its effectiveness on a selection of reinforcement learning benchmarks.