Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL

Mark Chevallier, Jacques Fleuriot

Research output: Working paperPreprint

Abstract / Description of output

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.
Original languageUndefined/Unknown
Number of pages37
Publication statusPublished - 11 Dec 2021

Keywords / Materials (for Non-textual outputs)

  • Markov decision processes
  • Bellman equation
  • Isabelle/HOL
  • Policy optimisation

Cite this