Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes

要約

対話型定理証明器 Isabelle/HOL でマルコフ決定過程 (MDP) を解くための実行可能なアルゴリズムを正式に検証します。
確率論の既存の定式化に基づいて、無限の地平線の問題で期待される総報酬基準を分析します。
私たちの開発は、ベルマン方程式を形式化し、最適なポリシーが存在する条件を提供します。
この分析に基づいて、表形式の MDP を解くための動的計画法アルゴリズムを検証します。
標準問題で正式に検証された実装を実験的に評価し、それらが実用的であることを示します。
さらに、効率的な検証されていない実装と組み合わせることで、私たちのシステムは最先端のシステムと競合し、さらにはそれを凌駕することさえできることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google