AI智能体攻克Lean不等式证明，186题解出175题成功率94%！
IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
📖 AI 总结
本文提出 IneqAgent，一个将大语言模型推理与符号计算相结合的不等式证明框架，用于在 Lean4 中完成形式化证明。该框架通过引理级蒙特卡洛树搜索协调引理构造、目标重写与符号后端选择，并整合平方和、Bernstein 及逐次差分代换三种后端，为局部 Lean 证明生成精确证书，再借助 Lean 反馈将符号证明与 LLM 生成的步骤拼接为完整证明。在四个基准测试上，使用 DeepSeek-V4-Flash 的 IneqAgent 解决了 186 道题中的 175 道，成功率达 94.09%，为所评估方法中最高；在四种骨干模型上，其低推理成本阈值下的成功率均高于同骨干的直接智能体方法，且平均推理成本更低。此外，该工作还获得了 Dittert 猜想在四维和五维下经 Lean 验证的强化结果，并证明了 Holens–Djokovic (4,4) 不等式，从而推出四维情形下的 Merris 猜想。
🔑 关键词速览
| IneqAgent | 一个结合大语言模型推理与符号计算，用于在 Lean4 中证明不等式的智能体框架。 |
| Lean4 | 一种交互式定理证明器，用于形式化数学证明和验证。 |
| 蒙特卡洛树搜索 | 一种启发式搜索算法，通过随机模拟和树结构来优化决策过程。 |
| 平方和 | 一种将多项式表示为平方和的方法，常用于不等式证明和优化。 |
| Dittert 猜想 | 关于矩阵永久量和行列式的一个数学猜想，涉及矩阵的优化问题。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅