用数学证明工具验证强化学习算法收敛性，为理论严谨性奠基。
Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach
- 基于Robbins-Siegmund定理，统一证明Q-learning与线性TD的几乎必然收敛
- 在马尔可夫采样下，严格形式化了两类经典RL算法的收敛性
- 代码开源，适合对强化学习理论验证感兴趣的学者和工程师
本文利用Lean 4定理证明器和Mathlib库，基于Robbins-Siegmund定理，正式验证了在马尔可夫样本下Q-learning与线性时序差分（TD）学习的几乎必然收敛性。这两类算法是强化学习中最古老且最具影响力的算法之一。对其收敛性质的研究不仅在强化学习早期发展中占据核心地位，至今仍是重要课题。本文构建的统一框架可进一步拓展至收敛速率及其他收敛模式。该工作为全面形式化收敛型强化学习结果迈出了关键一步。代码已公开于https://github.com/ShangtongZhang/rl-theory-in-lean。
原文摘要 · Abstract (English)
In this paper, we formalize the almost sure convergence of $Q$-learning and linear temporal difference (TD) learning with Markovian samples using the Lean 4 theorem prover based on the Mathlib library. $Q$-learning and linear TD are among the earliest and most influential reinforcement learning (RL) algorithms. The investigation of their convergence properties is not only a major research topic during the early development of the RL field but also receives significant attention nowadays. This paper formally verifies their almost sure convergence in a unified framework based on the Robbins-Siegmund theorem. The framework developed in this work can potentially be extended to convergence rates and other modes of convergence. This work thus makes an important step towards fully formalizing convergent RL results. The code is available at https://github.com/ShangtongZhang/rl-theory-in-lean.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。