Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL

TL;DR

This paper formalises the mathematical foundations of discrete reinforcement learning within Isabelle/HOL, including Bellman equations, policy evaluation, and optimality proofs, ensuring rigorous correctness of key algorithms.

Contribution

It introduces a formal Isabelle/HOL framework for finite MDPs, deriving core equations and proving the correctness and optimality of value and policy iteration algorithms.

Findings

Formal derivation of Bellman equations in Isabelle/HOL

Proof of existence of a universally optimal policy

Finite-time convergence of value and policy iteration algorithms

Abstract

We present a formalisation of finite Markov decision processes with rewards in the Isabelle theorem prover. We focus on the foundations required for dynamic programming and the use of reinforcement learning agents over such processes. In particular, we derive the Bellman equation from first principles (in both scalar and vector form), derive a vector calculation that produces the expected value of any policy p, and go on to prove the existence of a universally optimal policy where there is a discounting factor less than one. Lastly, we prove that the value iteration and the policy iteration algorithms work in finite time, producing an epsilon-optimal and a fully optimal policy respectively.