致力于形式化强化学习理论
机器学习
2025-11-06 v1 机器学习
摘要
本文基于 Lean 4 定理证明器（基于 Mathlib 库）对 Q 学习和线性时序差（TD）学习在马尔可夫采样条件下的几乎必然收敛性进行形式化。Q 学习和线性 TD 是最早且最具影响力的强化学习（RL）算法之一。其收敛性质的研究不仅是 RL 领域早期发展中的重要研究主题，也日益受到关注。本文在基于 Robbins-Siegmund 定理的统一框架中形式化验证了它们的几乎必然收敛性。本工作所发展的框架可以轻松扩展至收敛速率和其他收敛模式。因此，本工作标志着对收敛型 RL 结果进行完全形式化的重要一步。代码已公开于 https://github.com/ShangtongZhang/rl-theory-in-lean。
引用
@article{arxiv.2511.03618,
title = {Towards Formalizing Reinforcement Learning Theory},
author = {Shangtong Zhang},
journal= {arXiv preprint arXiv:2511.03618},
year = {2025}
}