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 中形式化验证，包含一个策略反复增长且验证不完美的原生实例。
正文 · AI 翻译
摘要：反思型语言智能体复用反馈与记忆，在不更新模型权重的情况下跨任务适应。然而，现有的策略选择与动作生成保证本身并不能确立：在资源约束下，局部反思何时能为完整智能体带来长期性能保证。本文通过从局部生成与部署保证中推导出次线性反事实遗憾的充分条件来填补这一空白，同时保留原生控制器。具体而言，我们建立了一种资源敏感的迁移，它沿实际执行路径约束全状态部署差异，并保持学习器与比较器各自的自身历史规律。此外，局部生成可靠性产生了一个累积生成机会界，通过明确的质量、覆盖与硬预算权衡，将策略获取与长期性能联系起来。为验证这些保证，我们在 Lean 中形式化了全部十三项编号理论结果的条件证明链，包括一个具有重复策略增长和不完美验证的原生实例。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.14790 [cs.AI] |
| （或 arXiv:2610.14790v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.14790 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Shi Xu [查看邮箱]
[v1]
2026年10月10日星期六 10:22:39 UTC（94 KB）
来源：arXiv cs.AI · arxiv.org