反思型 AI 智能体的反事实遗憾分析与 Lean 形式化验证保证

研究者提出了反思型语言 AI 智能体在保留原生控制器下实现次线性反事实遗憾的充分条件，解决局部反思在资源约束下缺乏长期性能保证的问题。该研究建立了资源敏感的转移机制以约束全状态部署偏差，并通过局部生成可靠性推导出累积生成机会界。全部 13 个理论结果的条件证明链均已在 Lean 中完成形式化验证。