Formally Verified Solution Methods for Markov Decision Processes
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.
Cite
Text
Schäffeler and Abdulaziz. "Formally Verified Solution Methods for Markov Decision Processes." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I12.26759Markdown
[Schäffeler and Abdulaziz. "Formally Verified Solution Methods for Markov Decision Processes." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/schaffeler2023aaai-formally/) doi:10.1609/AAAI.V37I12.26759BibTeX
@inproceedings{schaffeler2023aaai-formally,
title = {{Formally Verified Solution Methods for Markov Decision Processes}},
author = {Schäffeler, Maximilian and Abdulaziz, Mohammad},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {15073-15081},
doi = {10.1609/AAAI.V37I12.26759},
url = {https://mlanthology.org/aaai/2023/schaffeler2023aaai-formally/}
}