BriefGPT.xyz
Jun, 2022
无限时间马尔可夫决策过程解决方案的形式验证方法
Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes
HTML
PDF
Maximilian Schäfeller, Mohammad Abdulaziz
TL;DR
本文利用交互式定理证明器Isabelle/HOL，对于解决马尔科夫决策过程（MDPs）的可执行算法进行正式验证，并基于此分析验证动态规划算法来解决表格MDPs，实验结果表明该系统可以与最先进的系统竞争甚至超过它们。
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 expec
→