UCLA 团队联合 Terence Tao 发表 LLM 驱动形式化数学综述
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
UCLA 团队与 Terence Tao 等人发表综述 arXiv:2607.07779，梳理 LLM 驱动形式化数学的研究进展。论文将证明生成方法归为训练策略、推理时搜索与适配、智能体工作流三类，并强调通过形式化证明检查不等于解决问题或做出新数学贡献，区分定理基准、仓库任务、形式化项目和研究主张的评估证据，最后提出数据与评估、数学关系表示、猜想生成、可靠工具集成和人机协作五个优先方向。
Authors: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
Abstract:Large language models have made rapid progress in generating machine-checked proofs for well-defined mathematical problems. Extending this progress to research mathematics requires more than solving isolated theorems. Research involves choosing questions, developing definitions and conjectures, connecting results, and combining formal proofs with expert judgment. This survey examines how LLM-driven systems can support these broader activities. We review formal-mathematics tasks, datasets, and autoformalization, and organize proof-generation methods into three overlapping areas: training strategies, inference-time search and adaptation, and agentic workflows. We then examine benchmark results, selected research projects, and platforms for collaborative mathematical work. A central distinction runs throughout the survey: checking a formal proof does not by itself establish that it captures the intended problem or makes a new mathematical contribution. We therefore distinguish theorem benchmarks, repository tasks, formalization projects, and research claims, and discuss the evidence needed to assess each. Finally, we identify five priorities for progress: better data and evaluation, representations of mathematical relationships, conjecture and concept generation, reliable tool integration, and human--AI collaboration. Together, these perspectives connect advances in proof generation to the practical demands of mathematical research.
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2607.07779 [cs.CL] |
| (or arXiv:2607.07779v4 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2607.07779 arXiv-issued DOI via DataCite |
Submission history
From: Eric Jiang [view email]
[v1]
Wed, 8 Jul 2026 17:46:36 UTC (1,544 KB)
[v2]
Mon, 19 Oct 2026 16:53:53 UTC (2,981 KB)
[v3]
Mon, 2 Nov 2026 19:18:01 UTC (7,892 KB)
[v4]
Wed, 4 Nov 2026 11:31:48 UTC (7,902 KB)
来源：arXiv cs.AI · arxiv.org