Math Agents：大模型的数学推理与形式化证明

2026-04-08 约 3251 字预计阅读 7 分钟

数学，一直被认为是通往智能（Intelligence）的根节点。它要求极强的推理与规划能力、泛化与抽象能力，且具有开放式的无限复杂性。近年来，AI 领域掀起了一场在数学和代码能力上的“军备竞赛”，例如 OpenAI 的 o3/o4-mini、Google 的 Gemini Deep Think、DeepSeekMath-V2 以及字节跳动的 Seed Prover 等等。为什么大家都盯上了数学？

因为数学是复杂推理与规划的最佳代理（Proxy），且非常容易评估（数学题有标准答案可对，代码有单元测试可跑）。如果我们能让 AI 自主掌握数学，这种能力就可以泛化到现实世界中无限的复杂任务（如高级旅行规划、日程调度，甚至是科学发现）。

本文将带你详细梳理大模型解决数学问题的主流范式，探讨其瓶颈，并深入解析基于“形式化验证”的下一代 Math Agents（如 AlphaProof）的底层逻辑与技术细节。

1. 大模型如何学数学：当前的主流配方

目前，业界顶尖的数学大模型几乎都遵循一个标准范式：强大的预训练基座 + 两种后训练（Post-training）技术 + 极致的工程化。

1.1 SFT（监督微调）：好数据就是一切

要让模型学会一步步推导，首先需要高质量的训练数据。研究者们利用人工和强大 LLM 共同精选和构建大量的“题目 + 步骤化/工具集成的解答”。目前最大的开源数学数据集之一 NuminaMath-1.5 包含了近 90 万条高质量的数学数据。但是，如果数据集中只有最终答案，而缺乏中间推理步骤怎么办？这就引出了第二种技术。

1.2 RL（强化学习）：可验证性就是一切

当模型有了基础推理能力后，强化学习（RL）登场。通过将模型生成的最终答案与真实答案（Ground Truth）进行对比，我们能够为模型提供一个绝对客观的反馈信号（Reward）。像 DeepSeek-R1 这样的大模型，正是通过基于规则的自动验证，结合 GRPO 等算法，让模型在不断的试错中最大化奖励，从而涌现出自我反思、“顿悟（Aha moment）”和长链条推理能力。

2. 当前数学大模型的两大鸿沟（Gaps）

尽管大模型在 GSM8K、MATH 甚至 IMO（国际奥数）等有明确数值答案的题目上表现惊艳，但它们仍面临两大鸿沟：

2.1 从初等数学到高等数学的鸿沟

目前的成功主要集中在大学以前的数学题（Pre-college math，如 AIME、IMO），因为这些领域数据丰富。在缺乏训练数据的科研级高等数学领域，模型举步维艰。

2.2 从“猜答案”到“写严格证明”的鸿沟

现有的模型极度依赖数据的“可验证性”。如果题目是求出一个具体的数字，系统很容易自动对答案打分（GRPO 就可以工作）。然而，如果是高等数学中的定理证明（Proofs），模型就会暴露短板。它们可能会生成看似合理实则胡说八道（Bluff）的证明过程。因为无法用简单的脚本去自动验证一段长篇大论的自然语言证明是否正确，强化学习也就无从谈起。

3. 破局之道：形式化数学与 Lean 语言

为了打破数据稀缺和无法自动验证的困境，研究者们将目光转向了形式化数学（Formal Mathematics）。

3.1 非形式化 vs 形式化

非形式化数学（Informal Math）：用自然语言（文本、图像等）书写，非常灵活且被广泛使用，但人类或机器都极难自动检查其逻辑漏洞（所谓的 Reasoning Gaps）。
形式化数学（Formal Math）：将数学变成源代码（如使用交互式定理证明器 Lean）。你用代码写下定理（如 1+1=2 的规范）和证明过程，编译器会自动检查这段代码能否跑通。代码编译成功 $\equiv$ 证明完全正确。

目前在开源社区中，Lean Mathlib 项目已经拥有超过 100 万行形式化代码，涵盖了 10 万个定义和 20 万个定理。这种可以提供“即时且绝对正确反馈”的环境，正是强化学习梦寐以求的乐园。

4. AlphaProof：RL 遇见形式化数学的里程碑

2025年登上 Nature 的 AlphaProof 是 AI 结合形式化系统的杰作，它在 IMO 级别的问题上达到了银牌水平。

AlphaProof 继承了 AlphaGo 的“从零学习（Tabula Rasa）”哲学：如果智能体能在一个环境中通过纯试错掌握规律，它就能自己发现新知识。它的工作流（Master Plan）包含以下关键步骤：

自动形式化（Autoformalization）：为了获得足够的题目，首先训练一个 Formaliser 模型，将人类用自然语言写的海量数学题自动翻译成 Lean 形式化代码。
在 Mathlib 上预训练（SFT）：让 Prover 模型在 Mathlib 庞大的代码库上进行监督学习，建立选择证明步骤（Tactic）的优良先验直觉。
AlphaZero 强化学习：在形式化的问题上进行 RL 训练。模型在 Lean 环境中搜索证明步骤，Lean 编译器充当完美的裁判。验证成功的轨迹（Experience）被用来强化 Prover 网络。
Test-Time RL（测试时强化）：在推理阶段，面对具体的新问题时，系统会生成该问题的多种变体，并在这些变体上继续进行与训练时相同的 RL 搜索过程。

除 OpenAI 和 DeepMind 外，其他机构也在迅猛推进：

DeepSeek Prover 系列：从 V1（大规模合成数据 SFT），到 V1.5（引入 Lean 编译器反馈的 RL 和蒙特卡洛树搜索 MCTS），再到 V2（强化学习结合子目标分解 Subgoal Decomposition）。
LeanDojo (ReProver)：开源的检索增强证明器，在每一步证明时从全量定理库中检索相关前提（Premises）作为上下文。
Seed Prover 1.5：将其设计为一个 Agent 架构，它不再依赖模型脆弱的隐式记忆，而是能自主调用 Mathlib 搜索引擎查找定理，甚至能写 Python 代码验证直觉，并将复杂问题增量拆解为子引理（Lemmas）。

5. 前沿挑战与探索

尽管形式化证明为 RL 铺平了道路，但构建 Math Agents 依然面临巨大挑战。

5.1 驯服无限的证明搜索空间

下围棋的棋盘只有 19x19，而数学证明的动作空间（Action Space）是无限的。如何在无限的空间中进行高效的树搜索？

结合符号推理（LIPS 系统）：ICLR 2025 提出的 LIPS 系统专门针对奥数不等式证明。它将证明步骤分类为“缩放（Scaling，如代入柯西不等式）”和“重写（Rewriting，等价代数变形）”。LIPS 利用符号计算工具（Symbolic Tools）对 Scaling 操作进行穷举和剪枝（Pruning），结合 LLM 的重写能力，最终发现了连人类专家都认为不可能的全新证明路径。

5.2 自动形式化（Autoformalization）的评估难题

将非形式化（自然语言）的定理和证明翻译为形式化代码（Lean）至关重要。但我们面临一个极度困难的问题：如何评估翻译得对不对？

严谨的等价性检查（Equivalence checking）在计算上不可行。
人工检查成本太高。
常规的文本代理指标（如 BLEU）毫不准确。
自然语言证明中经常存在大量的“跳步（Reasoning gaps）”（比如一句“易证”带过），而形式化证明必须是“无缝隙（Gap-free）”的。

为此，研究界提出了 FormalAlign（自动对齐评估）和 FormalRx 框架。FormalRx 建立了一套 SCI（语义 Semantic、约束 Constraint、实现 Implementation）错误分类学，能够自动识别语义故障，并对自动形式化的结果进行修正和审查（Rectify and eXamine）。

5.3 从非形式化数学回流：Agentic AI

形式化数学虽然严谨，但目前仍有其局限性（它无法轻易涵盖 Mathlib 尚未支持的新前沿数学领域）。因此，像 Aletheia（基于 Gemini Deep Think）这样的纯自然语言数学研究智能体依然至关重要。Aletheia 引入了一个自然语言验证器（Natural language verifier）来识别候选解答中的逻辑漏洞，使得 Agent 能够进行“生成-验证-修改”的迭代。至关重要的是，这个 Agent 学会了“承认失败”，这极大地提高了人类研究人员与它协作时的效率。

6. 结语

从解决“1+1=2”到挑战费马大定理，大语言模型正在重新定义数学研究的边界。

无论是通过 Lean 编译器获取绝对正确的反馈（AlphaProof），利用符号系统剪枝无限的搜索树（LIPS），还是构建基于自然语言的迭代修正智能体（Aletheia），Math Agents 正在展示出前所未有的领域智能（Domain Intelligence）。随着“Vibe-Proving（直觉证明验证）”等人类与 AI 协作模式的成型，这些底层技术不仅将彻底改变理论数学，更将辐射至物理、计算机科学等更加广阔的基础科学研究中。

目录