arXiv：cs.AI· Zhongnian Li, Shi Xu, Mengting Xu, Peng Ying, Xinzheng Xu·· 16 小时前
反思型智能体的反事实遗憾：Lean 验证的长期性能保证
Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees
AI 导读
针对反思型语言智能体在资源约束下缺乏长期性能保证的问题，该论文给出了从局部生成与部署保证推导次线性反事实遗憾的充分条件，并建立一个资源敏感的迁移界限，将策略获取与长期性能通过质量、覆盖与硬预算的权衡联系起来。作者在 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