IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
中文摘要
由模型生成 · 人工抽检IneqAgent 是一个在 Lean4 中证明不等式的智能体框架，将 LLM 推理与符号计算结合，用引理级蒙特卡洛树搜索协调引理构造、目标改写与后端选择，并通过平方和、Bernstein、逐次差分代换等后端生成精确证书。在四个基准上以 DeepSeek-V4-Flash 解决 186 题中的 175 题（94.09%），推理成本更低，还验证了 Dittert 猜想的四、五维加强形式。
全文
已译中文arXiv:2610.20681v1 公告类型：新
摘要：形式化不等式证明需要数学推理与精确计算，二者通常通过中间引理和目标重写相连接。我们提出 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 猜想在四维下成立。
本译文由模型自动生成，仅供参考与快速理解；涉及数字、版本、命令、法律条文等请以原文为准。
原文附件
2 个 · 均跳转原站，本站不托管文件正文为原站公开内容的抓取与清洗结果，英文条目附模型生成的中文译文；两者均仅供参考， 准确内容请以原站为准。内容版权归原作者所有，若认为侵权请联系我们下线。