IneqAgent：通过符号计算在精益中证明代理不等式

摘要

arXiv:2610.20681v1 Announce Type: new Abstract: Formal inequality proving requires mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. We...

and the with four inequality LLM Lean proving reasoning exact

2026-10-16 1 阅读约1分钟阅读 Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang

arXiv:2610.20681v1 公告类型：新摘要：形式不等式证明需要数学推理和精确计算，通常通过中间引理和目标重新表述来连接。我们引入 IneqAgent，一个将 LLM 推理与符号计算相结合的代理框架，用于 Lean4 中的不等式证明。引理级蒙特卡罗树搜索协调引理构建、目标重新表述和符号后端选择。互补平方和、Bernstein 和连续的差异替换后端为本地精益证明生成生成精确的证书。该代理将这些证明与 LLM 生成的步骤集成，并使用精益反馈来构造针对原始定理陈述进行检查的完整证明。在四个基准测试中，IneqAgent 与 DeepSeek-V4-Flash 解决了 186 个问题中的 175 个问题 (94.09%)，在评估的方法中实现了最高的总体成功率。在四个主干网中，与使用相同主干网的 Direct Agent 相比，它在低 LLM 推理成本阈值下实现了更高的成功率，并且每种方法成功运行的平均推理成本更低。我们还获得了迪特尔猜想在第四维和第五维上经过精益验证的强化，并证明了霍伦斯-德约科维奇 $(4,4)$ 不等式，暗示了梅里斯在第四维上的猜想。

订阅66必读