论文

用AI驱动的形式化证明搜索推进数学研究

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri来源日期：2026.05.22

智能体系统Agent任务评测

摘要

大语言模型（LLM）在数学推理上日益出色，但其不可靠性限制了它们在数学研究中的效用。一种缓解手段是让LLM生成以Lean等形式化语言书写的证明。我们首次对这种方法解决开放问题的能力进行了大规模评估。我们能力最强的代理自主解决了353个开放Erdős问题中的9个，单问题成本仅几百美元；证明了44/492个OEIS猜想；并正被部署于组合数学、优化、图论、代数几何与量子光学研究。一个以LLM生成与Lean验证交替进行的基础代理复现了Erdős问题上的成功，但在最难的问题上成本更高。这些发现展示了AI辅助形式化证明搜索的威力，并阐明了使其成为可能的代理设计。

用AI驱动的形式化证明搜索推进数学研究：论文配图 — 图 2：全功能 AlphaProof Nexus 代理的设计。数学家提供一个精益定理作为输入，并提供一个证明，并且可选地提供自然语言上下文和以精益编码的附加领域知识。代理架构由基本的生成验证管道和可选的进化框架组成。基于 LLM 的证明者子代理尝试通过细化证明草图来解决问题 (2)。子代理可以选择调用 AlphaProof 作为工具；每次对目标调用 AlphaProof 都会返回是否找到证明或反驳，或者是否未成功解决目标。最终生成的草图由验证器检查，以确保问题陈述没有被不安全地更改，并且证明可以编译。如果所有目标都被成功证明，代理将输出最终的精益证明。这个基本管道可以通过进化种群数据库和评级机制来扩展。在此配置中，经过验证的草图被允许进入总体数据库 (3)。同时，评估者子代理会对之前的尝试进行采样 (4)，然后由 LLM 评论家在匹配中进行排名。比赛结果被重新录入数据库 (5) 以更新草图的 Elo 分数。然后，进化算法使用这些分数从数据库中采样先前的草图，构建一个整体提示（其中包括数学家的任何可选输入）以条件新的情节 (1)。