CertRL：在 Coq 中形式化价值迭代与策略迭代的收敛性证明
人工智能
2020-12-17 v2 计算机科学中的逻辑
编程语言
摘要
强化学习算法通过在概率环境中优化长期奖励来解决序贯决策问题。在安全关键场景中应用强化学习的诉求催生了近期一系列关于形式化约束强化学习的工作；然而，这些方法将学习算法的实现置于其可信计算基中。这些实现的关键正确性性质是保证学习算法收敛到最优策略。本文通过开展两种经典强化学习算法（有限状态马尔可夫决策过程的价值迭代与策略迭代）的 Coq 形式化，启动了弥合这一差距的工作。核心结果是对贝尔曼最优性原理及其证明的形式化，该证明利用贝尔曼最优算子的压缩性质来确立序列在无限时域极限下收敛。CertRL 开发例证了 Giry 单子与机械化度量余归纳如何简化强化学习算法的最优性证明。CertRL 库为证明关于马尔可夫决策过程与强化学习算法的性质提供了通用框架，为进一步的形式化强化学习算法工作铺平了道路。
引用
@article{arxiv.2009.11403,
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
author = {Koundinya Vajjha and Avraham Shinnar and Vasily Pestun and Barry Trager and Nathan Fulton},
journal= {arXiv preprint arXiv:2009.11403},
year = {2020}
}