arXiv cs.AI· Zhongnian Li, Shi Xu, Mengting Xu, Peng Ying, Xinzheng Xu·· 3 天前AI 评分20
反思型语言智能体的反事实遗憾：Lean 形式化验证的长期性能保证
Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees
AI 导读
研究者为反思型语言智能体推导出次线性反事实遗憾的充分条件，将局部生成与部署保证转化为完整智能体在资源约束下的长期性能保证，并保留原生控制器。该工作建立了资源敏感的迁移界，沿实际执行路径约束全状态部署差异，同时用局部生成可靠性给出累积生成机会界，显式刻画质量、覆盖与硬预算的权衡。全部 13 项编号理论结果的证明链已在 Lean 中形式化验证，包含一个策略反复增长且验证不完美的原生实例。
正文 · 原文
Abstract:Reflective language agents reuse feedback and memory to adapt across tasks without updating model weights. However, existing guarantees for policy selection and action generation do not by themselves establish when local reflection yields long-term performance guarantees for the complete agent under resource constraints. In this paper, we address this gap by deriving sufficient conditions for sublinear counterfactual regret from local generation and deployment guarantees, while retaining the native controller. Specifically, we establish a resource-sensitive transfer that bounds full-state deployment discrepancies along actual execution paths and preserves the own-history laws of both learner and comparator. Besides, local generation reliability yields a cumulative generation opportunity bound, linking policy acquisition to long-term performance through an explicit quality, coverage, and hard-budget tradeoff. To verify these guarantees, we formalize the conditional proof chain for all thirteen numbered theoretical results in Lean, including a native instance with repeated policy growth and imperfect validation.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.14790 [cs.AI] |
| (or arXiv:2610.14790v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.14790 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Shi Xu [view email]
[v1]
Sat, 10 Oct 2026 10:22:39 UTC (94 KB)
来源：arXiv cs.AI · arxiv.org