Research map / Reinforcement learning / MDPs and planning

Formally Verified Approximate Policy Iteration

AAAI 2025 · Reinforcement learning › MDPs and planning · approach: Average-reward and regularized MDPs · 1 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Formally verifies approximate policy iteration for factored MDPs in Isabelle/HOL, refines it to executable Scala code, and certifies LP solutions with exact dual certificates.

Problem

Verifying correctness of algorithms for factored Markov Decision Processes, which are hard to formalize because of scoped functions, decision lists, linear programming and dynamic programming combined.

Approach

Uses interactive theorem proving with locales to decouple the approximate policy iteration algorithm into specified components, refines them to executable verified code, and certifies unverified exact LP solutions via dual/Farkas certificates rather than verifying an LP solver.

Key results

• The verified implementation solves ring-domain instances up to 19 computers (about half a million states, 20 actions in the abstract) in 92.19 s, with 30.25 s spent in the LP solver.
• Weights converged after 5 iterations in all runs (discount factor 0.9).
• The development comprises roughly 20,000 lines of Isabelle code, about two thirds for code generation.

Measured effects reported in the paper

Surprising findings

• The original algorithm omitted the default action's scope from the bonus function scope, which the authors found to be an oversight.
• The original algorithm can create equality constraints forcing variables to -infinity, which LP solvers do not support; the authors proved a modification that omits them.

Limitations

• SoPlex in exact mode fails to find rational solutions for larger LPs (beyond 19 computers).
• LP solver is unverified; certification only checks returned solutions, and assumes determinism.
• Evaluation limited to a single ring topology domain.

Experimental setup

Datasets: ring network factored MDP benchmark

Benchmarks: ring topology domain

Metrics: running time (s) time in LP solver (s) number of LP constraints and variables

Builds on: approximate policy iteration (Guestrin et al.) Isabelle/HOL Isabelle Collections Framework

Closest papers by meaning

• Process-Verified Reinforcement Learning for Theorem Proving via Lean (ICLR 2026 · similarity 0.84)
• Protocols for Verifying Smooth Strategies in Bandits and Games (NeurIPS 2025 · similarity 0.84)
• Polynomial-Time Approximability of Constrained Reinforcement Learning (ICML 2025 · similarity 0.83)
• Scalable Policy-Based RL Algorithms for POMDPs (NeurIPS 2025 · similarity 0.83)
• Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives (AAAI 2025 · similarity 0.83)
• Finding Simple Proofs for First-Order Optimization (NeurIPS 2026 · similarity 0.83)