从求解器到研究者：大型语言模型驱动的前沿形式化数学

# 从求解者到研究者：大语言模型驱动的前沿形式化数学

来源：https://arxiv.org/html/2607.07779  
Eric Jiang¹,∗, Xiao Liang¹,∗, Yikai Zhang¹, Yingjia Wan¹, Mengting Li¹, Haikang Deng¹, Alexander K Taylor¹, Justin Baker¹, Rushil Raghavan¹, Junyi Zhang¹, Ying Nian Wu¹, Andrea L. Bertozzi¹, Kai-Wei Chang¹, Raghu Meka¹, Matthew Sottile², Nanyun Peng¹, Amit Sahai¹, Terence Tao¹, Wei Wang¹  
¹加州大学洛杉矶分校  
²劳伦斯利弗莫尔国家实验室  

###### 摘要  
近年来，数学人工智能（AI4Math），尤其是大语言模型（LLM）驱动的定理证明器，在通过交互式定理证明（ITP）语言为定义明确的数学问题生成形式化证明方面取得了显著成功。然而，当前系统在应对前沿研究数学方面仍存在根本性局限，例如发现新定理或解决开放猜想，这些问题往往是开放式的、定义不明确的，并涉及多个抽象层次。我们认为，AI4Math 系统的下一次飞跃需要决定性地*从预定义的问题求解者转向研究智能体*，能够以前沿数学挑战为目标，进行严谨的形式化数学推理。在这篇立场论文中，我们对该领域进行了系统性回顾，涵盖了数据集、自动形式化和证明合成。更重要的是，我们识别了现有系统在作为数学研究智能体方面的核心局限，考察了数据集、关系结构、数学探索、工具生态和人机协作等问题，并勾勒出 AI4Math 未来的战略路线图。  

![[无标题图片]](https://arxiv.org/html/2607.07779v1/figs/ucla_lawrence/github.png)  
资源集合 (https://github.com/ericjiang18/Awesome-Formal-Mathematics/tree/main)  

††footnotetext:∗同等贡献。  

## 1 引言  

数学人工智能（AI4Math）长期以来一直是机器智能的核心和基础领域，反映了赋予机器严谨的形式化数学推理能力的长期愿景。该领域的早期工作集中于神经符号方法 [Yue 等，2023 (https://arxiv.org/html/2607.07779#bib.bib208)]，旨在将神经模式识别与交互式定理证明系统（ITP）的结构化逻辑相结合。这些方法在形式化环境中的高精度证明合成方面取得了显著成功 [Yang 和 Deng，2019 (https://arxiv.org/html/2607.07779#bib.bib12)；Bansal 等，2019b (https://arxiv.org/html/2607.07779#bib.bib11)；Lample 等，2022 (https://arxiv.org/html/2607.07779#bib.bib59)]，但往往依赖于固定的、手动设计的启发式方法，限制了其在不同数学领域的可扩展性和适用性 [Abdelaziz 等，2022 (https://arxiv.org/html/2607.07779#bib.bib209)]。  

最近，大语言模型（LLM）的出现推动了非形式化数学推理的显著进展。像 DeepSeek-R1 [DeepSeek-AI，2025 (https://arxiv.org/html/2607.07779#bib.bib84)] 和 o-series [Jaech 等，2024 (https://arxiv.org/html/2607.07779#bib.bib81)] 这样的模型在众多基准测试中取得了强劲表现 [MAA，2024 (https://arxiv.org/html/2607.07779#bib.bib334)；Hendrycks 等，2021b (https://arxiv.org/html/2607.07779#bib.bib13)]。然而，这些生成自然语言非形式化推理的 LLM 推理器从根本上受到缺乏精确、机器可检查语义的限制，使其输出容易产生幻觉 [Huang 等，2025b (https://arxiv.org/html/2607.07779#bib.bib210)]，并无法实现自主验证——这是解决开放式数学研究的先决条件。  

为弥补这一差距，研究已转向 LLM 驱动的形式化数学推理系统。通过利用像 Lean [de Moura 和 Ullrich，2021 (https://arxiv.org/html/2607.07779#bib.bib52)] 这样的 ITP 进行严格验证，包括 DeepSeek-Prover [DeepSeek-AI，2024a (https://arxiv.org/html/2607.07779#bib.bib17)；Xin 等，2024b (https://arxiv.org/html/2607.07779#bib.bib61)] 和 Seed-Prover [Chen 等，2025c (https://arxiv.org/html/2607.07779#bib.bib102)] 在内的系统在竞赛级别数学的形式化证明生成方面设立了新标准 [Zheng 等，2022 (https://arxiv.org/html/2607.07779#bib.bib9)]。与此同时，将 LLM 与几何推理引擎相结合的混合方法 [Zhang 等，2026 (https://arxiv.org/html/2607.07779#bib.bib44)；Chervonyi 等，2025 (https://arxiv.org/html/2607.07779#bib.bib86)] 已超越人类在国际数学奥林匹克（IMO）几何问题上的金牌表现。这些进展凸显了 LLM 在不同数学领域生成形式化证明的潜力。  

尽管取得了这些进展，我们认为当前 AI4Math 系统在很大程度上仍作为*求解者*运作，擅长孤立、定义明确的证明生成，而非作为能够拓展数学知识边界的*研究者*。虽然最近的系统声称解决了 [Erdős 问题 (https://www.erdosproblems.com/)] 中的一些开放问题（Paul Erdős 提出的一系列极具挑战性的前沿数学问题），但其解决方案大多来自对已有文献结果的重新发现 [Erdős，1957 (https://arxiv.org/html/2607.07779#bib.bib197)]。此外，这些系统仍然缺乏解决许多困难数学开放问题的能力，例如 [千禧年大奖难题 (https://en.wikipedia.org/wiki/Millennium_Prize_Problems)]，这些问题需要真正新颖的想法，如第 4.4 节 (https://arxiv.org/html/2607.07779#S4.SS4) 和表 7 (https://arxiv.org/html/2607.07779#S4.T7) 所示。这些观察凸显了现有系统在探索开放式研究前沿方面的持续局限。  

AI4Math 系统的下一次飞跃需要决定性地*从预定义的问题求解者转向前沿数学的研究智能体。*  

为论证这一论点，我们分析了该领域的基础（第 2 节 (https://arxiv.org/html/2607.07779#S2)），制定了近期方法的分类（第 3 节 (https://arxiv.org/html/2607.07779#S3)），评估了当前技术水平，包括 AI 对开放 Erdős 问题的贡献（第 4 节 (https://arxiv.org/html/2607.07779#S4)），并识别了需要解决的关键挑战，以缩小竞赛求解者与研究智能体之间的差距（第 5 节 (https://arxiv.org/html/2607.07779#S5)）。我们的贡献如下：  

1. **LLM 形式化数学的统一分析**。我们提供了一个连贯的分类法，涵盖数据集、自动形式化、训练策略、推理时推理和智能体工作流，将这些线索联系起来，识别当前系统能做什么和不能做什么。  
2. **研究前沿 AI 的经验性全景**。我们系统性地阐述了 AI 对开放 Erdős 问题的贡献，按六种贡献类型进行分类并附有时间进程分析，首次提供了 AI 在真正研究级别数学上能力的结构化快照。  
3. **识别关键差距与具体方向**。我们指出了将竞赛级别求解者与研究级别智能体区分开来的五大障碍：数据和评估局限性、缺乏关系结构、数学探索的障碍、碎片化的工具生态以及不足的人机协作，并为每个障碍提出了切实可行的方向。  

## 2 基础与预备知识  

本节提供自动化定理证明历史发展、数学基础模型全景以及神经定理证明标准流程的必要背景。  

### 2.1 自动定理证明的历史背景  

机械化数学推理的梦想早于现代计算数百年。戈特弗里德·威廉·莱布尼茨在 1666 年提出的*推理演算*愿景设想了一种通用的逻辑语言，能够将争议简化为计算，这是对形式化验证极具远见的预测。这一哲学抱负通过 19 和 20 世纪形式逻辑的发展逐步实现，哥特洛布·弗雷格的*概念文字*、伯特兰·罗素和阿尔弗雷德·诺斯·怀特海的*数学原理*以及库尔特·哥德尔的不完备定理构成了基础性贡献，既确立了形式系统的力量，也揭示了其固有限制。  

现代自动定理证明时代真正始于 1956 年由艾伦·纽厄尔、J.C. 肖和赫伯特·A. 西蒙开发的逻辑理论家 [Newell 等，1956 (https://arxiv.org/html/2607.07779#bib.bib241)]。这一开创性系统成功证明了怀特海和罗素*数学原理*中前 52 个定理中的 38 个，首次展示了机器能够进行真正的数学推理。逻辑理论家采用了模仿人类问题解决某些方面的启发式搜索策略，建立了一种影响 AI 研究数十年的范式。  

1965 年，约翰·艾伦·罗宾逊提出了归结原理 [Robinson，1965 (https://arxiv.org/html/2607.07779#bib.bib242)]，为一阶逻辑提供了完整的证明过程。归结的优雅在于其简洁性：通过将公式转换为子句范式并反复应用单一推理规则，可以从一组前提中推导出任何有效结论。这项工作为后续几代自动定理证明器奠定了基础，并在现代系统中仍然具有影响力。  

随后的几十年见证了日益复杂的 ATP 范式的发展，每个范式针对定理证明挑战的不同方面进行了优化。基于饱和的证明器，如 E [Schulz 等，2019 (https://arxiv.org/html/2607.07779#bib.bib243)]、Vampire [Kovács 和 Voronkov，2013 (https://arxiv.org/html/2607.07779#bib.bib244)] 和 SPASS [Weidenbach 等，2007 (https://arxiv.org/html/2607.07779#bib.bib245)]，使用复杂的项排序和冗余消除技术系统地从公理推导出结论，在一阶问题上实现了显著的效率。这些系统赢得了多次 ATP 竞赛，并且至今仍是许多应用领域中自动推理的主力。  

一个并行的发展方向集中于特定逻辑理论的决策过程。SAT 求解器（确定命题公式可满足性）通过冲突驱动子句学习（CDCL）等技术经历了巨大改进，能够解决具有数百万变量的工业问题。SMT（可满足性模理论）求解器，如 Z3 [De Moura 和 Bjørner，2008 (https://arxiv.org/html/2607.07779#bib.bib246)] 和 CVC5 [Barbosa 等，2022 (https://arxiv.org/html/2607.07779#bib.bib247)]，通过将 SAT 求解与针对算术、数组、位向量及其他在软件和硬件验证中常见理论的专门决策过程相结合，扩展了这一成功。  

交互式定理证明器（ITP）作为一种互补范式出现，用完全自动化换取表达能力和人类引导。像 Mizar [Trybulec，1993 (https://arxiv.org/html/2607.07779#bib.bib248)]、HOL [Gordon 和 Melham，1993 (https://arxiv.org/html/2607.07779#bib.bib249)]、Coq [Team，2013 (https://arxiv.org/html/2607.07779#bib.bib55)]、Isabelle [Paulson，1994 (https://arxiv.org/html/2607.07779#bib.bib53)] 和 Lean [de Moura 和 Ullrich，2021 (https://arxiv.org/html/2607.07779#bib.bib52)] 这样的系统使人类数学家能够构建任意复杂度的机器验证证明，计算机充当不可错的检查者而非自主证明器。这种人机协作取得了卓越成就：在 Coq 中形式化四色定理 [Gonthier，2008 (https://arxiv.org/html/2607.07779#bib.bib250)]，在 HOL Light 和 Isabelle 中验证开普勒猜想 [Hales 等，2017 (https://arxiv.org/html/2607.07779#bib.bib251)]，以及在 Coq 中完成奇数阶定理的机器检查证明 [Gonthier 等，2013 (https://arxiv.org/html/2607.07779#bib.bib252)]。这些里程碑式的项目需要专家团队多年的专注努力，生动地说明了形式化验证的强大力量以及对更好自动化的迫切需求——神经方法现在有望满足这一需求。  

### 2.2 形式化数学与 ITP  

形式化数学使用交互式定理证明器（ITP）提供机器可检查的正确性保证，这是高风险领域所必需的能力。证明过程的核心在于使用**策略**将**证明状态**（包含当前目标和可用假设）转换为无任何目标残留的已解决状态。策略是状态转换函数，例如 `intro`、`apply`、`rewrite` 和 `induction`。策略通过证明器基础逻辑的可靠推理规则进行验证。这些系统由庞大的**形式化库**支持，如 Lean 的 mathlib [The mathlib Community，2020 (https://arxiv.org/html/2607.07779#bib.bib57)；van Doorn 等，2020 (https://arxiv.org/html/2607.07779#bib.bib157)] 和 Rocq 的 math-comp [Mahboubi 和 Tassi，2022 (https://arxiv.org/html/2607.07779#bib.bib58)]，提供了成千上万个定义和引理，对于前提选择和证明生成至关重要。这些库对于允许数学家在超出证明器核心基础逻辑的抽象层面工作至关重要。  

现代 ITP 可根据其逻辑基础和自动化范式分类如下：  

- **❶ 依赖类型理论**：像 Lean [de Moura 等，2015 (https://arxiv.org/html/2607.07779#bib.bib39)；de Moura 和 Ullrich，2021 (https://arxiv.org/html/2607.07779#bib.bib52)] 和 Coq [Team，2013 (https://arxiv.org/html/2607.07779#bib.bib55)；Bertot 和 Castéran，2013 (https://arxiv.org/html/2607.07779#bib.bib54)] 这样的系统允许高度表达性的证明构建。Lean 已通过 LeanDojo [Yang 等，2023b (https://arxiv.org/html/2607.07779#bib.bib8)] 和 TheoremLlama [Wang 等，2024e (https://arxiv.org/html/2607.07779#bib.bib89)] 等生态系统成为基于学习的研究的中心平台，而 Coq 支持像 CoqGym [Yang 和 Deng，2019 (https://arxiv.org/html/2607.07779#bib.bib12)] 这样的基准测试。  
- **❷ 一阶逻辑 (FOL)**：像 ACL2 [Kaufmann 和 Moore，1996 (https://arxiv.org/html/2607.07779#bib.bib231)] 这样的框架基于带有递归函数的 FOL，并强调强大的自动化能力。此外，强大的一阶自动定理证明器，包括 Vampire [Kovács 和 Voronkov，2013 (https://arxiv.org/html/2607.07779#bib.bib244)] 和 E-prover [Schulz，2002 (https://arxiv.org/html/2607.07779#bib.bib236)]，经常通过 hammer 风格的框架集成到 ITP 中，以增强证明自动化。  
- **❸ 高阶逻辑 (HOL)**：像 Isabelle/HOL [Paulson，1994 (https://arxiv.org/html/2607.07779#bib.bib53)] 这样的系统通过像 `sledgehammer` [Paulson 和 Blanchette，2012 (https://arxiv.org/html/2607.07779#bib.bib91)] 这样的工具强调自动化。这种方法启发了神经符号系统 [Jiang 等，2022 (https://arxiv.org/html/2607.07779#bib.bib94)；McGinness 和 Baumgartner，2024 (https://arxiv.org/html/2607.07779#bib.bib168)] 以及像 IsarStep [Li 等， 2020 (https://arxiv.org/html/2607.07779#bib.bib87)] 和 LISA [Jiang 等，2021 (https://arxiv.org/html/2607.07779#bib.bib88)] 这样的基准测试。  
- **❹ 混合系统**：PVS [Owre 等，1992 (https://arxiv.org/html/2607.07779#bib.bib237)] 代表了一种混合方法，通过使用谓词子类型在 HOL 和依赖类型之间架起桥梁。这在表达能力与自动化之间实现了平衡。