Formally Verified Approximate Policy Iteration

要約

対話型定理証明器 Isabelle/HOL を使用して、因数分解マルコフ決定プロセスの近似ポリシー反復アルゴリズムを正式に検証します。
次に、形式化されたアルゴリズムを実行可能で検証済みの実装に洗練する方法を示します。
実装はベンチマーク問題で評価され、その実用性が示されます。
改良の一環として、線形計画法ソリューションを認定するための検証済みソフトウェアを開発します。
このアルゴリズムは、形式化された数学の多様なライブラリに基づいて構築されており、対話型定理証明者の既存の方法論を限界まで押し上げます。
検証プロジェクトのプロセスと、正式な検証に必要なアルゴリズムの変更について説明します。

要約(オリジナル)

We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions. The algorithm builds on a diverse library of formalized mathematics and pushes existing methodologies for interactive theorem provers to the limits. We discuss the process of the verification project and the modifications to the algorithm needed for formal verification.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google