AAAI 2023technical9 citations
Formally Verified Solution Methods for Markov Decision Processes
Maximilian Schäffeler, Mohammad Abdulaziz
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 finite and 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, compare them with state-of-the-art systems, and show that they are practical.
BibTeX
@article{Schäffeler_Abdulaziz_2023, title={Formally Verified Solution Methods for Markov Decision Processes}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/26759}, DOI={10.1609/aaai.v37i12.26759}, abstractNote={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 finite and 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, compare them with state-of-the-art systems, and show that they are practical.}, number={12}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Schäffeler, Maximilian and Abdulaziz, Mohammad}, year={2023}, month={Jun.}, pages={15073-15081} }