从解题到科研：LLM 驱动的形式化数学如何走向研究前沿
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
一篇综述系统梳理了 LLM 驱动的形式化数学如何从孤立定理证明扩展到选题、定义与猜想构建、结果关联等研究活动，并将证明生成方法归为训练策略、推理时搜索与适配、智能体工作流三类。文章强调形式证明通过检查并不等于捕捉到原问题或构成新数学贡献，据此区分定理基准、代码库任务、形式化项目与研究主张四类证据。作者提出数据与评估、数学关系表示、猜想与概念生成、可靠工具集成、人机协作五项优先方向。
作者：Eric Jiang、Xiao Liang、Junyi Zhang、Justin Baker、Zhi Zhang、Yingjia Wan、Yubei Li、Jinxi Yu、Mengting Li、Haikang Deng、Alexander Taylor、Rushil Raghavan、Michael Simon、Hyunsik Chae、Jia-Chen Gu、Xinjie He、Kyle Hess、Ethan Ji、Yiwen Kou、Tzu-Han Lin、Jiachen Lu、Jack Mauro、Vigyan Sahai、Zheng Tan、Hengli Li、Yikai Zhang、Kyle Zheng、Lunji Zhu、Dong Liu、Jasdeep Sidhu、Isaac Hair、Eniuce Jun、Ying Nian Wu、Andrea L. Bertozzi、Kai-Wei Chang、Raghu Meka、Matthew Sottile、Nanyun Peng、Amit Sahai、Terence Tao、Wei Wang
摘要：大语言模型在为定义明确的数学问题生成机器可验证证明方面已取得快速进展。要将这一进展扩展到研究数学领域，仅解决孤立定理是不够的。研究涉及选择问题、发展定义与猜想、连接结果，以及将形式化证明与专家判断相结合。本综述考察了 LLM 驱动的系统如何支持这些更广泛的活动。我们回顾了形式数学任务、数据集和自动形式化，并将证明生成方法归纳为三个相互重叠的领域：训练策略、推理时搜索与适配，以及智能体工作流。随后，我们考察了基准测试结果、部分研究项目以及协作式数学工作平台。本综述贯穿一个核心区分：检查一个形式化证明本身并不能证明它捕捉到了预期问题或做出了新的数学贡献。因此，我们区分了定理基准、代码库任务、形式化项目和研究主张，并讨论了评估各类别所需的证据。最后，我们确定了五个推进优先事项：更好的数据与评估、数学关系的表示、猜想与概念生成、可靠的工具集成，以及人机协作。这些视角共同将证明生成的进展与数学研究的实际需求联系起来。
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI） |
| 引用为： | arXiv:2607.07779 [cs.CL] |
| （或 arXiv:2607.07779v4 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2607.07779 由 DataCite 颁发的 arXiv DOI |
提交历史
发件人：Eric Jiang [查看邮件]
[v1]
2026年7月8日 星期三 17:46:36 UTC（1,544 KB）
[v2]
2026年10月19日 星期一 16:53:53 UTC（2,981 KB）
[v3]
2026年11月2日 星期一 19:18:01 UTC（7,892 KB）
[v4]
2026年11月4日 星期三 11:31:48 UTC（7,902 KB）
来源：arXiv cs.CL · arxiv.org