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

Koundinya Vajjha, Avraham Shinnar, Vasily Pestun +2

Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learni…