Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes

TL;DR

This paper presents formally verified algorithms for solving infinite-horizon Markov decision processes using Isabelle/HOL, ensuring correctness and practical efficiency in comparison to existing systems.

Contribution

It introduces formally verified dynamic programming algorithms for infinite-horizon MDPs within a theorem prover, combining formal correctness with practical performance.

Findings

Verified algorithms solve standard MDP problems effectively

Formalization ensures correctness of the Bellman equation and policies

System can outperform some state-of-the-art solutions

Abstract

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.