Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL
This provides a rigorous mathematical foundation for discrete reinforcement learning, though it is incremental as it formalizes existing theory rather than developing new algorithms.
The authors formalized finite Markov decision processes with rewards in Isabelle/HOL, deriving foundational results like the Bellman equation and proving the existence of optimal policies and convergence of value and policy iteration algorithms.
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.