无限时域马尔可夫决策过程的正式验证求解方法
人工智能
2023-03-09 v2 计算机科学中的逻辑
摘要
我们在交互式定理证明器 Isabelle/HOL 中正式验证了用于求解马尔可夫决策过程（MDPs）的可执行算法。我们基于已有的概率论形式化成果，分析无限时域问题上的期望总回报准则。我们的研究形式化了贝尔曼方程，并给出了最优策略存在的条件。基于此分析，我们验证了用于求解表格 MDP 的动态规划算法。我们在标准问题上对正式验证的实现进行了实验评估，表明它们是实用的。此外，我们表明，结合高效的未验证实现，我们的系统可以与最先进的系统竞争甚至超越它们。
引用
@article{arxiv.2206.02169,
title = {Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes},
author = {Maximilian Schäfeller and Mohammad Abdulaziz},
journal= {arXiv preprint arXiv:2206.02169},
year = {2023}
}