CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

TL;DR

This paper develops a Coq formalization of value and policy iteration algorithms for Markov decision processes, ensuring their convergence and correctness, which is crucial for safety-critical reinforcement learning applications.

Contribution

It introduces a formal Coq framework for proving convergence of reinforcement learning algorithms, specifically formalizing Bellman's optimality principle and its proof.

Findings

Formalization of Bellman's optimality principle in Coq

Proof of convergence of value and policy iteration algorithms

A reusable Coq library for reinforcement learning algorithms

Abstract

Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires a recent line of work on formally constrained reinforcement learning; however, these methods place the implementation of the learning algorithm in their Trusted Computing Base. The crucial correctness property of these implementations is a guarantee that the learning algorithm converges to an optimal policy. This paper begins the work of closing this gap by developing a Coq formalization of two canonical reinforcement learning algorithms: value and policy iteration for finite state Markov decision processes. The central results are a formalization of Bellman's optimality principle and its proof, which uses a contraction property of Bellman optimality operator to establish that a sequence converges in the infinite horizon limit. The CertRL development exemplifies how the Giry monad and mechanized metric coinduction streamline optimality proofs for reinforcement learning algorithms. The CertRL library provides a general framework for proving properties about Markov decision processes and reinforcement learning algorithms, paving the way for further work on formalization of reinforcement learning algorithms.