在 Isabelle/HOL 中形式化离散强化学习的基础
计算机科学中的逻辑
2021-12-14 v1 人工智能
最优化与控制
摘要
我们在 Isabelle 定理证明器中提出了带奖励的有限马尔可夫决策过程的形式化。我们关注动态规划以及在此类过程上使用强化学习智能体所需的基础。特别地，我们从第一性原理推导了贝尔曼方程（标量与向量形式），推导了产生任意策略 p 期望值的向量计算，并进一步证明了在折扣因子小于 1 时存在普遍最优策略。最后，我们证明了值迭代与策略迭代算法能在有限时间内工作，分别产生 epsilon-最优与完全最优策略。
引用
@article{arxiv.2112.05996,
title = {Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL},
author = {Mark Chevallier and Jacques Fleuriot},
journal= {arXiv preprint arXiv:2112.05996},
year = {2021}
}