反思型语言智能体的反事实遗憾：Lean 形式化验证的长期性能保证

针对反思型语言智能体在资源约束下局部反思能否带来长期性能保证的问题，研究推导出从局部生成与部署保证到次线性反事实遗憾的充分条件，并建立资源敏感的迁移界，沿实际执行路径约束全状态部署偏差。局部生成可靠性给出累积生成机会上界，将策略获取与长期性能通过质量、覆盖和硬预算的权衡联系起来。全部 13 项编号理论结果的证明链已在 Lean 中形式化验证，包含一个策略反复增长且验证不完美的原生实例。