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.

我们使用交互式定理证明器Isabelle/HOL对一种近似策略迭代算法在因子化马尔可夫决策过程上进行了形式验证。接着，我们展示了如何将形式化的算法细化为可执行的验证实现。所开发的实现方案经过了基准问题的评估，表明其实用性。作为细化的一部分，我们开发了经过验证的软件以认证线性规划解法。该算法基于丰富的形式化数学库，并推动了交互式定理证明器的现有方法的极限。我们讨论了验证项目的过程以及为形式验证所需的算法修改。

正式验证的近似策略迭代