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.

翻译：我们在交互式定理证明器Isabelle/HOL中形式化验证了用于求解马尔可夫决策过程（MDP）的可执行算法。基于已有的概率论形式化成果，我们分析了无限时域问题上的期望总回报准则。我们的研究工作形式化了贝尔曼方程，并给出了最优策略存在的条件。基于此分析，我们验证了用于求解表格型MDP的动态规划算法。我们在标准问题上对形式化验证的实现进行了实验评估，证明其实用性。此外，研究表明，结合高效的非验证实现，我们的系统能够与最先进的系统竞争甚至超越它们。