Formally Verified Approximate Policy Iteration

TL;DR

This paper presents a formally verified approximate policy iteration algorithm for Factored Markov Decision Processes, including a verified implementation and software for certifying Linear Programming solutions, demonstrating practical applicability.

Contribution

It introduces a formally verified algorithm for approximate policy iteration and develops verified software for Linear Programming certification, advancing formal methods in decision process algorithms.

Findings

Verified algorithm successfully applied to benchmark problems

Implementation demonstrates practical viability

Enhanced formal methods for interactive theorem proving

Abstract

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.