Formally Verified Approximate Policy Iteration
Not on the map. Why?
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.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 11 of its 47 references that are in the map. First posted on arXiv 11 Jun 2024.
Builds on
11 of 47 references.
References · 11
- 2014Near-optimal Reinforcement Learning in Factored MDPscited by 41
- 2017A storm is Coming: A Modern Probabilistic Model Checkercited by 34
- 2022Neural Network Verification with Proof Productioncited by 22
- 2017Developing Bug-Free Machine Learning Systems With Formal Mathematicscited by 13
- 2023Enabling Research through the SCIP Optimization Suite 8.0cited by 13
- 2020CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coqcited by 9
- 2023A Practitioner's Guide to MDP Model Checking Algorithmscited by 9
- 2021Polynomial Time Reinforcement Learning in Factored State MDPs with Linear Value Functionscited by 4
- 2020Formally Verified SAT-Based AI Planningcited by 3
- 2021Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOLcited by 3
- 2022Formal Semantics and Formally Verified Validation for Temporal Planningcited by 3
Built on by
Citing papers per year: 2025: 1.
1 paper.