arXiv cs.AI· Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang·· 2 天前AI 评分34
IneqAgent：结合符号计算的 Lean 不等式证明智能体
IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
AI 导读
IneqAgent 是一个将 LLM 推理与符号计算结合、在 Lean4 中证明不等式的智能体框架，采用引理级蒙特卡洛树搜索协调引理构造、目标重写与符号后端选择。
正文 · AI 翻译
摘要：形式化不等式证明需要数学推理和精确计算，二者通常通过中间引理和目标重构相互关联。我们提出 IneqAgent，一个将 LLM 推理与符号计算相结合用于 Lean4 不等式证明的智能体框架。引理级蒙特卡洛树搜索协调引理构造、目标重构和符号后端选择。互补的平方和、Bernstein 和逐次差分代换后端为局部 Lean 证明生成提供精确证书。该智能体将这些证明与 LLM 生成的步骤整合，并利用 Lean 反馈构建对照原始定理陈述检查的完整证明。在四个基准上，使用 DeepSeek-V4-Flash 的 IneqAgent 解决了 186 个问题中的 175 个（94.09%），在所评估方法中取得了最高的总体成功率。在四个骨干模型上，与使用相同骨干模型的 Direct Agent 相比，它在低 LLM 推理成本阈值下取得了更高的成功率，且在各方法成功运行中的平均推理成本更低。我们还获得了 Dittert 猜想在四维和五维上经 Lean 验证的强化形式，并证明了 Holens--Djokovic $(4,4)$ 不等式，从而蕴含 Merris 猜想在四维上的成立。
| 学科： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.20681 [cs.AI] |
| （或 arXiv:2610.20681v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.20681 arXiv 颁发的 DOI 通过 DataCite |
提交历史
来自：Gaolei He [查看邮箱]
[v1]
2026年10月14日星期三 16:29:11 UTC（203 KB）
来源：arXiv cs.AI · arxiv.org