反思型 AI 智能体反事实遗憾及其 Lean 验证保证

研究者提出了具备 Lean 形式化验证保证的反思型 AI 智能体反事实遗憾理论，推导出在保留原生控制器下实现次线性反事实遗憾的充分条件。该工作建立了资源敏感型转移机制，通过质量、覆盖度与硬预算权衡将策略获取与长期表现挂钩。论文中所有 13 项带编号的理论结果均已在 Lean 中完成条件证明链形式化。