LLM for Mathematical Reasoning：定理证明、形式化验证与奥赛推理

LLM for Mathematical Reasoning：定理证明、形式化验证与奥赛推理

系列：AI 论文盘点 / 技术趋势
日期：2026-07-11
适合读者：研究生、数学推理与形式化方法研究者、LLM 评测研究者、有工程背景的技术读者
检索日期：2026-07-11

目录

• 研究背景：为什么数学推理突然成为主战场
• 核心科学问题：答案、证明与形式化之间的断层
• 近一年论文路线图
• 代表论文分组解读
• 方法对比表
• 实验与 benchmark 如何看
• 可复现性与数据问题
• 局限与争议
• 适合研究生继续做的选题
• 总结
• 参考资料

研究背景：为什么数学推理突然成为主战场

早期 LLM 数学能力常被 GSM8K、MATH、AIME 子集这类题目衡量。GSM8K 证明了小学应用题也需要多步推理；MATH 把题目难度推进到竞赛数学，并提供逐步解答；Minerva 则说明在科学论文、LaTeX 和技术文本上继续预训练，可以显著增强定量推理。随后，self-consistency、verifier、process reward model 和 test-time scaling 让“多采样、再筛选”成为数学任务的常用范式。

但这个阶段有两个结构性问题。第一，最终答案正确不代表证明正确。模型可能用错误步骤碰巧得到正确数值，也可能给出看似严谨但存在断裂的推导。第二，公开 benchmark 很快被训练数据、题库讲解、解析视频和模型蒸馏污染。越是热门的 AIME、MATH 和 Olympiad 题，越难分辨模型是在推理，还是在回忆题型与解法模板。

因此，数学推理研究开始向“可验证”迁移。Lean、Isabelle、Coq/Rocq、Metamath 等 proof assistant 提供了小内核检查机制：只要形式化命题和证明被系统接受，证明的局部正确性就不再依赖 LLM 自述。Lean 4 和 mathlib 的扩张尤其重要，因为它们把形式化数学、程序验证和 LLM 工具交互放到同一个可执行环境里。Lean 官方网站强调，Lean 是开源编程语言和证明助手，能用于可维护代码与形式化证明；mathlib 则提供跨代数、分析、拓扑、概率和计算机科学的大规模数学库。

核心科学问题：答案、证明与形式化之间的断层

这条路线至少有五个核心问题。

第一，自然语言推理是否可靠。长链 CoT、反思、树搜索和多样化采样能提高命中率，但也会放大幻觉。数学文本很容易“局部合理、全局错误”，尤其是组合、数论和几何构造题。

第二，证明是否可机器检查。形式化证明把“看起来对”变成“编译器接受”。问题是，从自然语言题面到 Lean 命题、从人类草稿到完整 proof script，本身就是困难的 autoformalization 任务。

第三，搜索空间如何压缩。形式化证明不是简单生成一段代码。模型需要选择引理、展开定义、调用 tactic、处理类型错误、读懂 proof state，并在大量失败分支里回溯。

第四，评测是否抗污染。固定公开题库会迅速失效。MathArena 这类实时竞赛评测，以及 FrontierMath、IMO-Bench、VAR-MATH 等更难或可变形 benchmark，试图把评价从“历史题库”推向“新鲜题、原创题、参数化题、证明题”。

第五，数学能力是否能迁移到科研。IMO gold-level 结果很吸引眼球，但竞赛数学和研究数学不同。竞赛题短、边界清楚、通常有优雅解；研究数学可能需要定义新对象、构建理论、处理长依赖链和多年协作。

近一年论文路线图

2025-2026 年最明显的变化是形式化证明模型的快速上升。DeepSeek-Prover-V2 把 DeepSeek-V3 的自然语言分解能力接入 Lean 4 证明生成，通过子目标分解和强化学习缩小 informal 与 formal 的差距。Kimina-Prover Preview 从 Qwen2.5-72B 出发，强调“formal reasoning pattern”和大规模 RL，在 miniF2F 上报告了强 pass@8192 表现，并开源蒸馏模型。Leanabell-Prover-V2 继续沿着 verifier-integrated RL 走，把 Lean 编译器反馈作为多轮交互信号。2026 年的 LEAP 则把 general-purpose LLM 变成 agentic formal math 框架：先形成非形式化蓝图，再与 Lean 编译器持续交互、分解子问题、修正 proof state。

第二条线是自然语言奥赛推理。Google DeepMind 在 2025 年发布的官方博客称，Gemini Deep Think 的高级版本在 IMO 2025 达到金牌标准，提交解答经 IMO 确认为完整正确；同一页面也注明，IMO 的确认不等于验证系统、流程或底层模型。这个 caveat 很关键：数学解答可被判分，系统实验条件是否等同人类竞赛、是否可复现、是否使用未公开后处理，仍需要独立审查。同期 IMO-Bench 提供 AnswerBench、ProofBench 和 GradingBench，目标是评估短答案、长证明和自动评分。

第三条线是几何与 neuro-symbolic。AlphaGeometry2 在 2025 年 arXiv 论文中报告，其语言覆盖从 IMO 2000-2024 几何题的 66% 提升到 88%，整体解决率提升到 84%。它不是通用聊天模型，而是 Gemini 架构语言模型、几何表示语言、符号引擎、合成数据和搜索机制的组合。这说明：在几何这种结构化强、构造关键的领域，神经模型和符号系统的耦合仍然非常有竞争力。

第四条线是 benchmark 反击。Omni-MATH 提供 4428 道奥赛级数学题；FrontierMath 由专家设计未公开新题，避免公开题库污染；MathArena 使用最新竞赛题进行实时评测；VAR-MATH 把固定数值题改造成参数化多实例题，以测试模型是否真正掌握结构。论文之间的共同信号是：旧 benchmark 的高分越来越不够用。

代表论文分组解读

1. 从答案题到 verifier：MATH、GSM8K、Minerva、过程监督

MATH 和 GSM8K 是这条路线的基础设施。MATH 的价值在于提供竞赛级题目和逐步解答；GSM8K 则使“训练 verifier、从多候选答案中选择”成为数学推理的早期成功范式。Minerva 进一步证明，技术语料和 LaTeX 结构对数学能力有直接帮助。

过程监督论文《Let’s Verify Step by Step》把监督信号从最终答案移动到中间步骤，释放了一个重要思想：数学推理训练不能只奖励结论，还要奖励可检查的局部进展。后来的 PRM、ORM、self-consistency、best-of-N 和 test-time compute 都围绕这个思想展开。局限也很明显：人类标注步骤昂贵，LLM judge 容易偏好流畅文本，最终仍无法替代形式化检查。

2. Autoformalization：把自然语言数学翻译到 Lean

ProofNet 是 autoformalization 研究的重要 benchmark：它包含本科数学的自然语言陈述、自然语言证明和 Lean 形式化陈述。LeanDojo 则进一步提供可交互环境、前提检索、proof state 数据和 ReProver，使研究者可以在开源环境里训练 Lean prover。

2024 年的“Improving Autoformalization using Type Checking”提出用类型检查和 self-consistency 过滤形式化结果，并指出评测本身也需要修正。这个方向的关键不是让 LLM 写出漂亮的 Lean 代码，而是判断形式化命题是否忠实表达原题。形式化命题写错时，即使证明通过，也只是在证明另一个问题。

3. Neural theorem proving：检索、搜索、RL 与编译器反馈

DeepSeek-Prover-V1 用大规模合成 Lean 4 数据训练证明模型，DeepSeek-Prover-V1.5 加入 proof assistant feedback、RLPAF 和 RMaxTS 搜索；DeepSeek-Prover-V2 再进一步使用强模型做递归子目标分解，合成 cold-start 数据，再用强化学习提升证明能力。它报告在 miniF2F-test 上达到很高 pass ratio，并引入 ProverBench；这些数字应按论文设置理解，不能直接等价于“自动证明任意数学”。

Kimina-Prover Preview 的启发在于，它把证明过程视为一种显式的 formal reasoning pattern：模型不只输出 tactic，而是围绕 proof state 做规划、试错和修正。Leanabell-Prover-V2 则更强调 verifier-integrated long CoT，让模型在 Lean 错误信息中学习自我修正。LEAP 的贡献是把 agentic framework 引入正式数学：一般 LLM 可以先写蓝图，再不断调用 Lean 编译器反馈，逐步压缩证明空间。

这条线的工程瓶颈非常具体：Lean 环境版本、mathlib commit、依赖索引、proof state 序列化、premise retrieval、tactic 超时、并行采样预算，都会显著影响结果。论文里的 pass@k 不是单一模型能力，而是模型、搜索器、检索器、编译器和计算预算的组合指标。

4. 几何路线：AlphaGeometry2 与符号引擎仍然重要

AlphaGeometry 和 AlphaGeometry2 提醒我们，不要把数学推理简化成“更大 LLM + 更长 CoT”。几何题的关键经常是构造辅助点、线、圆或发现隐藏相似关系。纯自然语言模型可能知道很多定理，但缺少系统搜索构造的机制。

AlphaGeometry2 通过扩展几何语言、改进符号引擎、知识共享搜索树和合成数据，把覆盖率和解题率推高。它的强项也正是局限：系统依赖领域表示语言和专门符号引擎，迁移到代数、数论、组合或研究数学时需要重新设计结构。

5. 奥赛与前沿 benchmark：高分之后更需要谨慎

Gemini Deep Think 在 IMO 2025 的表现说明，自然语言 reasoning model 已经能在极高难度的短题上给出可判分证明。Google DeepMind 官方博客写明其方法基于自然语言，而非 2024 年 AlphaProof/AlphaGeometry 那样的形式化翻译流程；同时也说明，未来更有价值的系统可能结合自然语言流畅性和形式化验证。

但评测解释必须克制。IMO 题每年只有 6 道，统计样本很小；公开声明通常无法完全复现实验条件；证明评分需要专家；模型可能经过大量 test-time compute、专门提示和人工流程设计。MathArena 的发现也说明，在 USAMO 这类 proof-writing 任务上，顶级模型与答案题表现之间仍有明显落差。

方法对比表

实验与 benchmark 如何看

读数学推理论文时，建议先看任务类型。短答案题、证明题、形式化证明题和研究级开放题不能混在一起比较。AIME 可能只需要一个整数答案；USAMO 需要完整证明；miniF2F 需要 proof assistant 接受；FrontierMath 则试图逼近专业数学家数小时到数天的工作量。

第二，看是否区分 pass@1、pass@k、best-of-N 和搜索预算。一个模型 pass@1 强，说明单次生成质量高；pass@8192 强，可能说明大规模采样和验证器很有效。两者都重要，但研究含义不同。

第三，看形式化环境是否固定。Lean 4 版本、mathlib commit、允许使用的 tactic、超时设置、检索库和是否允许sorry都会改变结果。没有这些信息，形式化证明实验很难复现。

第四，看 benchmark 是否新鲜。MathArena 的思路值得关注，因为它在竞赛题发布后尽快评测，减少数据污染。VAR-MATH 的参数化多实例也很重要，因为它测试的是结构泛化，而不是记住某个数值题。

第五，看 human grading 与 auto-grading 的关系。IMO-Bench 的 GradingBench 试图评估自动评分与人工评分的一致性，这是长证明评测必须面对的问题。一个 AI 解答“看起来像证明”，不等于在竞赛规则下能拿满分。

可复现性与数据问题

数学推理的可复现性比普通 NLP 更复杂。对于自然语言模型，研究者需要公布提示、采样温度、候选数、工具权限、是否使用搜索、是否使用人工筛选。对于 Lean prover，还要公布 Lean 版本、mathlib commit、依赖安装方式、编译缓存、搜索器配置和硬件预算。

数据污染是最大隐患之一。MATH、GSM8K、AIME、IMO 历史题、ProofNet、miniF2F 的题面和解答都高度公开，许多模型训练集可能已经间接包含。即使题目本身没进入训练集，讲义、论坛、解析视频和模型生成数据也可能包含类似解法。未来更可信的评测会依赖三类设计：未公开原创题、实时竞赛题、参数化变体题。

另一个被低估的问题是“形式化命题忠实性”。如果 autoformalizer 把自然语言题面翻译成更弱命题，prover 很容易通过；如果翻译成更强命题，模型可能被不公平惩罚。因此，autoformalization 评测需要人工或符号等价检查，而不能只看 type-check。

局限与争议

第一，奥赛表现不等于研究数学。IMO 题很难，但通常是短程、封闭、可判分问题。研究数学需要定义新概念、整合长文献、构建理论框架和写出可复用引理库。

第二，形式化证明不等于数学理解。Lean 接受一个 proof script，说明它在给定形式系统中成立；但模型是否理解证明的关键想法、能否迁移到相邻定理、能否解释给数学家，仍需额外评测。

第三，test-time scaling 有成本问题。大量采样、树搜索、编译器交互和 verifier reranking 可以显著提升得分，但也会带来算力不可比、延迟过高和不可复现实验设置。

第四，自动评分会被优化。只要 benchmark 与 judge 固定，模型就可能学会迎合评分器，而不是提升数学能力。证明任务尤其需要独立专家抽查和 adversarial grading。

第五，公开代码与模型仍不充分。DeepSeek、Kimina、LeanDojo 等开放路线很有价值，但许多最强系统只发布博客或有限技术细节。对学术研究者来说，可复现系统比 headline 更重要。

适合研究生继续做的选题

1. 忠实 autoformalization 评测：构建自然语言命题、Lean 命题和人工等价标签，研究“证明通过但题意错”的检测方法。
2. Lean proof state 诊断数据集：收集失败 proof state、错误信息、修复动作和人类解释，训练更可靠的 verifier-aware prover。
3. 参数化奥赛 benchmark：把 AIME/AMC/USAMO 风格题改造成可生成族，评估模型是否掌握不变量而非记忆数字。
4. 低预算 theorem proving：研究 pass@1、pass@8 或单 GPU 条件下的证明策略，避免只靠海量采样。
5. 自然语言证明到 Lean 蓝图：让模型先生成结构化 proof plan，再由专门 prover 填 tactic，分析蓝图质量与最终通过率关系。
6. 几何构造的可解释搜索：复现或改造 AlphaGeometry 式思路，比较神经构造、Wu 方法、DDAR 和人类辅助构造。
7. 长证明自动评分：围绕 IMO-Bench/MathArena 风格任务，研究 rubric-aware grading、局部错误定位和人机一致性。

总结

LLM 数学推理的前沿正在从“会做题”转向“会证明、会验证、会在新题上稳定泛化”。自然语言 reasoning model 给出了强探索能力，Lean 和 mathlib 提供了机器可检查的正确性，实时竞赛和原创 benchmark 正在修补污染问题。未来最值得关注的系统，可能不是单独的聊天模型或单独的证明器，而是能够在自然语言想法、形式化命题、编译器反馈、搜索预算和专家评审之间来回切换的数学研究助手。

对研究者而言，下一步不要只追逐更高 AIME 或 miniF2F 分数。更有价值的问题是：模型证明的到底是不是原题？它为什么选择某个引理？失败时能不能定位错误？在新鲜题、变体题和研究级定理上是否仍然有效？这些问题决定了数学推理能否从竞赛展示走向真正可靠的科研工具。

参考资料

检索日期：2026-07-11。以下链接优先使用论文、官方博客、官方项目页或 benchmark 页面；快速变化的模型可用性、榜单分数、代码仓库状态和未同行评议预印本结论，发布前建议人工复核。

1. Dan Hendrycks et al., “Measuring Mathematical Problem Solving With the MATH Dataset”, arXiv, 2021. https://arxiv.org/abs/2103.03874
2. Karl Cobbe et al., “Training Verifiers to Solve Math Word Problems”, arXiv, 2021. https://arxiv.org/abs/2110.14168
3. Aitor Lewkowycz et al., “Solving Quantitative Reasoning Problems with Language Models”, arXiv, 2022. https://arxiv.org/abs/2206.14858
4. Hunter Lightman et al., “Let’s Verify Step by Step”, arXiv, 2023. https://arxiv.org/abs/2305.20050
5. Kunhao Zheng, Jesse Michael Han, Stanislas Polu, “MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics”, arXiv, 2021. https://arxiv.org/abs/2109.00110
6. Zhangir Azerbayev et al., “ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics”, arXiv, 2023. https://arxiv.org/abs/2302.12433
7. Kaiyu Yang et al., “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”, arXiv, 2023. https://arxiv.org/abs/2306.15626
8. Lean official website, “Lean Programming Language”. https://lean-lang.org/
9. Lean community, “A mathlib overview”. https://leanprover-community.github.io/mathlib-overview.html
10. Huajian Xin et al., “DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data”, arXiv, 2024. https://arxiv.org/abs/2405.14333
11. Huajian Xin et al., “DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search”, arXiv, 2024. https://arxiv.org/abs/2408.08152
12. Z. Z. Ren et al., “DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition”, arXiv, 2025. https://arxiv.org/abs/2504.21801
13. Haiming Wang et al., “Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning”, arXiv, 2025. https://arxiv.org/abs/2504.11354
14. Xingguang Ji et al., “Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning”, arXiv, 2025. https://arxiv.org/abs/2507.08649
15. Po-Nien Kung et al., “LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks”, arXiv, 2026. https://arxiv.org/abs/2606.03303
16. Yuri Chervonyi et al., “Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2”, arXiv, 2025. https://arxiv.org/abs/2502.03544
17. Google DeepMind, “AI achieves silver-medal standard solving International Mathematical Olympiad problems”, 2024. https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/
18. Google DeepMind, “Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad”, 2025. https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/
19. Thang Luong et al., “Towards Robust Mathematical Reasoning”, arXiv, 2025. https://arxiv.org/abs/2511.01846
20. Mislav Balunović et al., “MathArena: Evaluating LLMs on Uncontaminated Math Competitions”, arXiv, 2025. https://arxiv.org/abs/2505.23281
21. Bofei Gao et al., “Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models”, arXiv, 2024. https://arxiv.org/abs/2410.07985
22. Elliot Glazer et al., “FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI”, arXiv, 2024. https://arxiv.org/abs/2411.04872
23. Jian Yao, Ran Cheng, Kay Chen Tan, “VAR-MATH: Probing True Mathematical Reasoning in LLMs via Symbolic Multi-Instance Benchmarks”, arXiv, 2025. https://arxiv.org/abs/2507.12885
24. Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut, “Improving Autoformalization using Type Checking”, arXiv, 2024. https://arxiv.org/abs/2406.07222