# Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 35 references that are in the map.
- First posted on arXiv 5 Jun 2022.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Developing Bug-Free Machine Learning Systems With Formal Mathematics](https://mlsanity.com/paper/1706.08605/) (2017)
- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL](https://mlsanity.com/paper/2112.05996/) (2021)
- [A Verified Compiler for Probability Density Functions](https://mlsanity.com/paper/1707.06901/) (2017)

## Abstract (arXiv)

We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. Based on this analysis, we verify dynamic programming algorithms to solve tabular MDPs. We evaluate the formally verified implementations experimentally on standard problems and show they are practical. Furthermore, we show that, combined with efficient unverified implementations, our system can compete with and even outperform state-of-the-art systems.