# Formally Verified Approximate Policy Iteration

arXiv: https://arxiv.org/abs/2406.07340 · HTML: https://mlsanity.com/paper/2406.07340/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 47 references that are in the map.
- First posted on arXiv 11 Jun 2024.

## Builds on (most cited first, 11 of 11)

- [Near-optimal Reinforcement Learning in Factored MDPs](https://mlsanity.com/paper/1403.3741/) (2014)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Developing Bug-Free Machine Learning Systems With Formal Mathematics](https://mlsanity.com/paper/1706.08605/) (2017)
- [Enabling Research through the SCIP Optimization Suite 8.0](https://mlsanity.com/paper/2303.07101/) (2023)
- [A Practitioner's Guide to MDP Model Checking Algorithms](https://mlsanity.com/paper/2301.10197/) (2023)
- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [Polynomial Time Reinforcement Learning in Factored State MDPs with Linear Value Functions](https://mlsanity.com/paper/2107.05187/) (2021)
- [Formally Verified SAT-Based AI Planning](https://mlsanity.com/paper/2010.14648/) (2020)
- [Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL](https://mlsanity.com/paper/2112.05996/) (2021)
- [Formal Semantics and Formally Verified Validation for Temporal Planning](https://mlsanity.com/paper/2203.13604/) (2022)

## Built on by (most cited first, 1 of 1)

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)

## Abstract (arXiv)

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.