1. 论文到底在解决什么问题1.1 为什么数学推理被当成AI的“硬骨头”先聊一个基础问题为什么偏偏是数学推理这几年大语言模型在写代码、写文章、做问答上已经很能打了但一碰到需要多步逻辑推导的数学题经常会出现“看起来答案很对、过程全是编的”的情况。原因在于自然语言本身是有歧义的模型学会的往往是语言的统计规律而不是真正可靠的推理规则。这篇论文选择了一个很“激进”的切入点与其在自然语言里做数学不如换到形式化数学语言里做。形式化数学指的是把数学定理、定义、证明全部写成机器可以严格检查的形式比如 Metamath、Lean、HOL Light 这些证明助手系统。在形式化系统里每个证明步骤都被拆成极小的一步程序可以在几秒钟内验证它是真还是假。换句话说模型不再需要“看起来对”而是必须“真的对”。这篇论文的核心价值就在于它证明了基于 Transformer 的模型在形式化数学证明这个严谨到近乎残酷的领域里能够学会比此前最好方法更强的证明策略甚至用远小于 GPT-3 的模型达到远超 GPT-3 的成绩。如果你关注 AI for Math、自动定理证明或者单纯好奇“大模型到底能不能做真正的推理”这篇论文是绕不开的一篇。1.2 为什么选定理证明而不是应用题有人可能会问为什么不训练模型直接解应用题那样更贴近“人类数学”。原因很现实应用题没有绝对客观的判定标准。模型写出来一个解法你很难判断它对不对更难自动判断。定理证明就不一样。证明助手系统里每一条推理规则都是预先定义好的证明文件可以通过类型检查就说明这个定理成立。这就把“模型有没有推理能力”这个问题转化成了“模型能不能在有限步内找到一条从公理到目标的合法路径”可以自动化评估也可以无限生成训练数据。这和 AlphaGo 用自对弈刷新围棋认知是一个逻辑只有规则是确定的AI 才能真正放开手脚去搜索和学习。这篇论文选用的是 Metamath 系统尤其是其中的 set.mm 库一个积累了数十年、包含数万个已证明定理的庞大知识库。Metamath 的语法极其朴素基本就是一阶逻辑加集合论token 化非常规整对 Transformer 来说老少皆宜。这也是论文作者选择它的重要原因之一。1.3 论文的研究对象与基础设定论文全名是《Formal Mathematical Reasoning: A New Frontier in AI》出自 OpenAI 团队作者包括 Christian Szegedy 等人2022 年发表。核心研究对象叫 GPT-f是一个专门为形式化定理证明训练的 Transformer 模型。整个思路可以简化成一句话把“找一个证明”变成“做文本生成”。先给出要证明的目标再让模型一步步生成证明步骤每一步生成后立刻交给 Metamath 验证如果验证通过就更新状态继续下一步直到最终证明完成。这里有一个很关键的点GPT-f 不是拿普通文本训练的而是直接拿“证明过程中的每一步状态”训练。模型看到的每个输入包含当前已证明的步骤集合、目标表达式、允许使用的规则和已定义的定理输出是下一步该做什么。这就让模型真正贴近“证明者”的身份而不是一个只会背题面的答题机器。2. 论文的核心方法怎么训练一个会证明定理的 Transformer2.1 把证明搜索改造成序列到序列生成要理解 GPT-f 的方法先得理解 Metamath 的证明状态长什么样。Metamath 里的证明本质是一个栈式推导过程每一步可以引入一个新断言比如某个公理或已证明定理也可以做替换与合一来消化当前目标。每一步之后整个证明状态都会变化。GPT-f 的做法是把“当前状态”转换成一个 token 序列把“下一步应该应用的断言”也转换成一个 token 序列然后训练模型做条件生成。模型输入当前状态输出下一步操作。这本质上是一个序列到序列模型但因为解码只需要输出一个断言所以推理时很轻量。训练数据的来源很有意思。set.mm 库里有大量人工写好的证明这些证明文件经过 Metamath 验证后内部每一步状态和对应的断言都是已知的。论文直接把每一对状态断言抽取出来构成监督训练集。相当于是“拿着标准答案教模型如何走棋”。这里我不展开内部 token 的具体设计因为论文附录里写得很细但你只需要知道Metamath 本身的语法足够简单任何表达式都可以无歧义地线性化这对 Transformer 的 tokenizer 极其友好。换个更复杂的证明助手可能光表示状态就够头疼了。2.2 自监督数据生成解决语料不足问题有人担心靠已有的几万个证明够用吗论文的实验告诉我们不够但也不是无解。GPT-f 在训练集规模不足的情况下引入了一个叫“自监督目标生成”的机制。具体做法是从已有的证明库中取出中间状态把中间状态“伪装”成一个新的目标然后让模型尝试证明它。你能做到这一点是因为 Metamath 中每个中间状态本身就是一个合法的待证明目标它不一定能从公理推出但对模型来说多一个目标就多一条训练样本。更重要的是这些中间状态往往比最终定理更小、更简单适合模型从易到难地学习。这个思路和课程学习curriculum learning是高度一致的。模型在大量中等级别的目标上训练逐步学到如何处理子目标然后再挑战完整定理。论文数据里这种合成目标的数量可以达到百万级远超过原始证明库本身的样本量。这是整个方法在工程上能跑通的关键。2.3 策略模型、价值模型和教材生成器的三角配合如果只训练一个模型做“下一步预测”效果已经不错但这种贪心策略很容易走进死胡同。论文引入了三个组件配合起来完成完整的证明搜索策略模型policy model给定当前证明状态输出多个可能的下一步断言候选。价值模型value model给定当前证明状态输出一个分数表示这个状态距离证明完成还有多远。教材生成器proof assistant负责从已有的证明库中“出题”生成大量可供训练的自监督目标。搜索时策略模型先给出 k 个候选动作Metamath 逐个验证哪些合法然后进入新状态价值模型再给这些新状态打分保留分数较高的状态进入下一轮。这本质上是一个集束搜索beam search与价值函数引导的混合算法。看到这里你可能想到了 AlphaGo 里的 MCTS。没错论文在附录中明确提到了受 AlphaGo 启发只不过围棋的状态是棋盘而这里的状态是一个公式栈。价值模型的训练数据也来自策略模型的自我对弈式探索模型自己尝试证明目标记录每个状态的后续走向能最终证明的状态打高分走入死胡同的状态打低分。这里我要单独提一句“教材生成器”。它真的很有巧思。它不仅仅是“随机抽中间状态”而是会根据当前模型的水平动态选择难度适中的中间状态作为目标。模型初期只能证非常简单的目标教材生成器就多抽短证明的中间状态模型能力提升后再逐步增加复杂目标。这让训练过程变得非常顺滑也是论文中消融实验里贡献最大的组件之一。2.4 与 GPT-3 的对比为什么小模型能赢过大模型论文里有一个很有意思的对比实验直接用 GPT-3 做 few-shot 提示让它输出 Metamath 证明步骤效果并不好。而 GPT-f 虽然模型规模远小于 GPT-3却能在 miniF2F 基准上取得大约两倍于 GPT-3 的成绩。为什么小模型反而更强核心差别在训练目标。GPT-3 学的是“自然语言文本的规律”它的训练语料里虽然包含数学但那是人类读的数学不是机器验证的形式化证明。形式化证明的 token 分布和自然语言差别巨大GPT-3 从来没见过那么多“状态断言”的配对数据自然做不好。GPT-f 则完全为证明生成任务定制它的输入输出格式、训练语料、学习目标全部围绕 Metamath 证明过程展开。这给我们的启示很朴素模型不是越大越好而是越匹配任务越好。你用通用模型做专用事很多时候不如一个精心调校的小模型。这个观点在后来很多领域比如代码生成、SQL 生成也反复得到验证。3. 实验结果与评估细节到底提升了多少3.1 miniF2F 基准是什么要判断一个定理证明系统强不强不能只看它在自己熟悉的题库上的正确率需要一个跨系统的统一基准。论文里用的基准叫 miniF2F一个包含约 488 道数学题的测试集题目来源包括竞赛数学、高中数学、国际数学奥林匹克中的简单题等。miniF2F 最值得称道的一点是它同时支持多个证明助手语法。同一条数学命题会同时提供 Metamath、Lean、Isabelle 等不同系统下的版本。这意味着你可以公平比较不同系统上的 AI 证明方法。GPT-f 主要在 Metamath 语法版本上评测因为它的训练数据就是 Metamath。我在精读时特意数了一下这些题的难度基本都是初等到中等难度的数学竞赛题比如“任意三角形内角和为180度”“某个不等式恒成立”之类。对人类来说这些题不算特别难但对自动定理证明系统来说每一步都得从公理出发一步都不能跳难度完全不亚于人类做高难竞赛。3.2 核心结果一览论文报告的主要结果大致如下不同版本论文数字会略有出入以正式发表版为准在 miniF2F 测试集上GPT-f 解决了大约 29.3% 的题目。作为对比当时已知最好的非学习型传统方法如 hammer 类方法大概只能解决 20% 出头。GPT-3 的 few-shot 方法解决率约为 13.1%不到 GPT-f 的一半。如果移除教材生成器或价值函数GPT-f 的性能都会明显下降说明这些组件并非可有可无。这个成绩放在今天的大模型时代看可能不算惊艳因为后来 Lean 生态上的方法比如 DeepSeek-Prover、ReProver 等已经解决率更高。但你要放到当时的语境里看这是第一次有人用纯 Transformer 强化学习的方法在形式化数学证明这一“硬核推理”指标上显著超越传统搜索工具而且模型规模还很小。论文的实验设计也给后来者提供了一个标准范式用什么数据训练、怎么生成目标、如何用搜索树增强后续论文大量沿用了这套框架。3.3 手工形式化证明的案例分析论文除了跑 benchmark还挑了一个比较有代表性的定理做案例研究。我记得比较清楚的是它对某个数论或分析性质的证明过程做了解析并和人类证明做了对比。有个细节让我印象很深模型产出的证明路径和人类教材里的标准证明并不一样但每一步都是合法的。这说明模型不是简单记忆了某个标准解法而是真的在搜索空间里找到了一条可行路径。这在自动定理证明里是很有价值的因为很多拓扑、代数问题的证明路径不唯一模型能找到一条不常见但正确的路径意味着它具备了一定程度的“创造性”。当然论文也坦诚说明了当前模型找到的证明往往比较长、比较绕人类读者可能觉得不太优雅。这提醒我们AI 的形式化推理能力还处于“能证明”阶段距离“优雅地证明”还有距离。3.4 消融实验里藏着哪些门道消融实验是论文里信息密度最高、最值得仔细读的部分。作者逐个移除组件看最终指标变化我挑几个重点说去掉教材生成器后模型只能依靠原始证明库做监督训练性能显著下降。这说明自监督数据是训练的核心燃料。去掉价值模型、只用贪心搜索时性能同样下降因为模型在某个局部状态犯错后无法回溯。增大集束搜索宽度比如从 beam size 1 增加到 32可以提升性能但收益会递减同时计算成本增长很快。这些实验看起来简单但对复现者来说是极好的调参指南。比如你想在 Lean 上复现类似方法第一步就该考虑怎么构造一个“教材生成器”而不是急着堆模型参数量。4. 这篇论文的真正意义与还存在的问题4.1 把“推理能力”变成可训练的工程问题过去哲学层面讨论“AI 到底能不能推理”往往众说纷纭。这篇论文的聪明之处在于它不跟你争论抽象定义而是把一个严格的推理任务形式化为“搜索合法证明步骤”然后用标准的机器学习流程把它解掉了。形式化数学的好处是证明过程可以被机器完全验证所以模型的错误不会像自然语言回答一样被掩盖。这让论文的每一个结论都极其扎实GPT-f 会证明就真的能给出可通过验证的证明链。你完全可以把这套“可验证环境 合成目标 策略学习”的框架平移到其他领域比如程序合成、芯片验证、协议分析。只要环境能提供严格的反馈信号方法就有用武之地。4.2 局限一搜索成本仍然高得吓人论文里的模型虽然小但证明搜索过程的计算量可不小。为了证明 miniF2F 上的几十道题算法需要探索成千上万条证明路径每条路径又涉及多次模型前向推理和环境验证。论文在附录里给出了详细的计算资源清单动用了几十块 GPU 和大量 CPU 验证节点。这对复现者来说是很现实的挑战。如果你只有一块消费级显卡想完整复现论文的实验并不容易。我的建议是先从少量题目、较小规模开始比如只跑 miniF2F 中的 20 道简单题把训练和搜索流程打通再逐步放大。论文本身也提供了开源代码和预训练模型权重这大大降低了入门门槛。4.3 局限二对已有证明语料的强烈依赖GPT-f 的成功离不开 set.mm 和 Metamath 生态的数十年积累。不是每个领域都有这样高质量、大规模、严格验证过的形式化知识库。如果你想把这套方法迁移到新的数学分支或者迁移到物理、工程领域第一个卡点就是没有足够的“已经证明过的定理”来生成训练数据。论文中“教材生成器”能工作是因为 set.mm 里已经有大量中等难度的中间状态可以抽取。换一个只有几十条定理的冷门领域这个方法就转不动了。这也是为什么后来很多团队把精力放在自动构建形式化语料库上比如从 LaTeX 论文中半自动抽取数学命题并翻译成 Lean 语句。4.4 与后续工作的演进关系这篇论文发表后自动定理证明ATD社区迅速“卷”了起来。它直接启发了后来的很多研究方向用更强的预训练语言模型如 Codex、GPT-4替换 GPT-f 作为策略模型大幅提升 zero-shot 泛化能力。引入更先进的搜索算法比如 Best-first Search、MCTS 的变体替代简单的集束搜索。在 Lean 生态上构建了更大的证明语料库和基准测试比如 ProofNet、Mathlib 等。将证明搜索与强化学习结合得更紧密让模型直接通过尝试证明来学习而不是依赖大量人工标注。如果你读完这篇论文后想继续深入我建议按这个顺序读先读附录里的证明示例理解 Metamath 的证明格式再复现论文的 baselines最后再看 Lean 方向的相关工作。这样一路下来你会对“AI 形式化推理”这个方向形成比较完整的认知。最后分享一点个人体会我最欣赏这篇论文的地方是它把“数学推理”这个宏大命题拆解成了可以迭代优化的工程问题。它没有等待某个“通用推理能力”的神话降临而是就用已有的 Transformer、已有的证明库、已有的搜索算法认认真真做了一套在标准评测上跑得通的系统。这种务实的研究态度比任何花哨的模型架构都更值得学习。
GPT-f解析：用Transformer攻克形式化数学推理与自动定理证明
1. 论文到底在解决什么问题1.1 为什么数学推理被当成AI的“硬骨头”先聊一个基础问题为什么偏偏是数学推理这几年大语言模型在写代码、写文章、做问答上已经很能打了但一碰到需要多步逻辑推导的数学题经常会出现“看起来答案很对、过程全是编的”的情况。原因在于自然语言本身是有歧义的模型学会的往往是语言的统计规律而不是真正可靠的推理规则。这篇论文选择了一个很“激进”的切入点与其在自然语言里做数学不如换到形式化数学语言里做。形式化数学指的是把数学定理、定义、证明全部写成机器可以严格检查的形式比如 Metamath、Lean、HOL Light 这些证明助手系统。在形式化系统里每个证明步骤都被拆成极小的一步程序可以在几秒钟内验证它是真还是假。换句话说模型不再需要“看起来对”而是必须“真的对”。这篇论文的核心价值就在于它证明了基于 Transformer 的模型在形式化数学证明这个严谨到近乎残酷的领域里能够学会比此前最好方法更强的证明策略甚至用远小于 GPT-3 的模型达到远超 GPT-3 的成绩。如果你关注 AI for Math、自动定理证明或者单纯好奇“大模型到底能不能做真正的推理”这篇论文是绕不开的一篇。1.2 为什么选定理证明而不是应用题有人可能会问为什么不训练模型直接解应用题那样更贴近“人类数学”。原因很现实应用题没有绝对客观的判定标准。模型写出来一个解法你很难判断它对不对更难自动判断。定理证明就不一样。证明助手系统里每一条推理规则都是预先定义好的证明文件可以通过类型检查就说明这个定理成立。这就把“模型有没有推理能力”这个问题转化成了“模型能不能在有限步内找到一条从公理到目标的合法路径”可以自动化评估也可以无限生成训练数据。这和 AlphaGo 用自对弈刷新围棋认知是一个逻辑只有规则是确定的AI 才能真正放开手脚去搜索和学习。这篇论文选用的是 Metamath 系统尤其是其中的 set.mm 库一个积累了数十年、包含数万个已证明定理的庞大知识库。Metamath 的语法极其朴素基本就是一阶逻辑加集合论token 化非常规整对 Transformer 来说老少皆宜。这也是论文作者选择它的重要原因之一。1.3 论文的研究对象与基础设定论文全名是《Formal Mathematical Reasoning: A New Frontier in AI》出自 OpenAI 团队作者包括 Christian Szegedy 等人2022 年发表。核心研究对象叫 GPT-f是一个专门为形式化定理证明训练的 Transformer 模型。整个思路可以简化成一句话把“找一个证明”变成“做文本生成”。先给出要证明的目标再让模型一步步生成证明步骤每一步生成后立刻交给 Metamath 验证如果验证通过就更新状态继续下一步直到最终证明完成。这里有一个很关键的点GPT-f 不是拿普通文本训练的而是直接拿“证明过程中的每一步状态”训练。模型看到的每个输入包含当前已证明的步骤集合、目标表达式、允许使用的规则和已定义的定理输出是下一步该做什么。这就让模型真正贴近“证明者”的身份而不是一个只会背题面的答题机器。2. 论文的核心方法怎么训练一个会证明定理的 Transformer2.1 把证明搜索改造成序列到序列生成要理解 GPT-f 的方法先得理解 Metamath 的证明状态长什么样。Metamath 里的证明本质是一个栈式推导过程每一步可以引入一个新断言比如某个公理或已证明定理也可以做替换与合一来消化当前目标。每一步之后整个证明状态都会变化。GPT-f 的做法是把“当前状态”转换成一个 token 序列把“下一步应该应用的断言”也转换成一个 token 序列然后训练模型做条件生成。模型输入当前状态输出下一步操作。这本质上是一个序列到序列模型但因为解码只需要输出一个断言所以推理时很轻量。训练数据的来源很有意思。set.mm 库里有大量人工写好的证明这些证明文件经过 Metamath 验证后内部每一步状态和对应的断言都是已知的。论文直接把每一对状态断言抽取出来构成监督训练集。相当于是“拿着标准答案教模型如何走棋”。这里我不展开内部 token 的具体设计因为论文附录里写得很细但你只需要知道Metamath 本身的语法足够简单任何表达式都可以无歧义地线性化这对 Transformer 的 tokenizer 极其友好。换个更复杂的证明助手可能光表示状态就够头疼了。2.2 自监督数据生成解决语料不足问题有人担心靠已有的几万个证明够用吗论文的实验告诉我们不够但也不是无解。GPT-f 在训练集规模不足的情况下引入了一个叫“自监督目标生成”的机制。具体做法是从已有的证明库中取出中间状态把中间状态“伪装”成一个新的目标然后让模型尝试证明它。你能做到这一点是因为 Metamath 中每个中间状态本身就是一个合法的待证明目标它不一定能从公理推出但对模型来说多一个目标就多一条训练样本。更重要的是这些中间状态往往比最终定理更小、更简单适合模型从易到难地学习。这个思路和课程学习curriculum learning是高度一致的。模型在大量中等级别的目标上训练逐步学到如何处理子目标然后再挑战完整定理。论文数据里这种合成目标的数量可以达到百万级远超过原始证明库本身的样本量。这是整个方法在工程上能跑通的关键。2.3 策略模型、价值模型和教材生成器的三角配合如果只训练一个模型做“下一步预测”效果已经不错但这种贪心策略很容易走进死胡同。论文引入了三个组件配合起来完成完整的证明搜索策略模型policy model给定当前证明状态输出多个可能的下一步断言候选。价值模型value model给定当前证明状态输出一个分数表示这个状态距离证明完成还有多远。教材生成器proof assistant负责从已有的证明库中“出题”生成大量可供训练的自监督目标。搜索时策略模型先给出 k 个候选动作Metamath 逐个验证哪些合法然后进入新状态价值模型再给这些新状态打分保留分数较高的状态进入下一轮。这本质上是一个集束搜索beam search与价值函数引导的混合算法。看到这里你可能想到了 AlphaGo 里的 MCTS。没错论文在附录中明确提到了受 AlphaGo 启发只不过围棋的状态是棋盘而这里的状态是一个公式栈。价值模型的训练数据也来自策略模型的自我对弈式探索模型自己尝试证明目标记录每个状态的后续走向能最终证明的状态打高分走入死胡同的状态打低分。这里我要单独提一句“教材生成器”。它真的很有巧思。它不仅仅是“随机抽中间状态”而是会根据当前模型的水平动态选择难度适中的中间状态作为目标。模型初期只能证非常简单的目标教材生成器就多抽短证明的中间状态模型能力提升后再逐步增加复杂目标。这让训练过程变得非常顺滑也是论文中消融实验里贡献最大的组件之一。2.4 与 GPT-3 的对比为什么小模型能赢过大模型论文里有一个很有意思的对比实验直接用 GPT-3 做 few-shot 提示让它输出 Metamath 证明步骤效果并不好。而 GPT-f 虽然模型规模远小于 GPT-3却能在 miniF2F 基准上取得大约两倍于 GPT-3 的成绩。为什么小模型反而更强核心差别在训练目标。GPT-3 学的是“自然语言文本的规律”它的训练语料里虽然包含数学但那是人类读的数学不是机器验证的形式化证明。形式化证明的 token 分布和自然语言差别巨大GPT-3 从来没见过那么多“状态断言”的配对数据自然做不好。GPT-f 则完全为证明生成任务定制它的输入输出格式、训练语料、学习目标全部围绕 Metamath 证明过程展开。这给我们的启示很朴素模型不是越大越好而是越匹配任务越好。你用通用模型做专用事很多时候不如一个精心调校的小模型。这个观点在后来很多领域比如代码生成、SQL 生成也反复得到验证。3. 实验结果与评估细节到底提升了多少3.1 miniF2F 基准是什么要判断一个定理证明系统强不强不能只看它在自己熟悉的题库上的正确率需要一个跨系统的统一基准。论文里用的基准叫 miniF2F一个包含约 488 道数学题的测试集题目来源包括竞赛数学、高中数学、国际数学奥林匹克中的简单题等。miniF2F 最值得称道的一点是它同时支持多个证明助手语法。同一条数学命题会同时提供 Metamath、Lean、Isabelle 等不同系统下的版本。这意味着你可以公平比较不同系统上的 AI 证明方法。GPT-f 主要在 Metamath 语法版本上评测因为它的训练数据就是 Metamath。我在精读时特意数了一下这些题的难度基本都是初等到中等难度的数学竞赛题比如“任意三角形内角和为180度”“某个不等式恒成立”之类。对人类来说这些题不算特别难但对自动定理证明系统来说每一步都得从公理出发一步都不能跳难度完全不亚于人类做高难竞赛。3.2 核心结果一览论文报告的主要结果大致如下不同版本论文数字会略有出入以正式发表版为准在 miniF2F 测试集上GPT-f 解决了大约 29.3% 的题目。作为对比当时已知最好的非学习型传统方法如 hammer 类方法大概只能解决 20% 出头。GPT-3 的 few-shot 方法解决率约为 13.1%不到 GPT-f 的一半。如果移除教材生成器或价值函数GPT-f 的性能都会明显下降说明这些组件并非可有可无。这个成绩放在今天的大模型时代看可能不算惊艳因为后来 Lean 生态上的方法比如 DeepSeek-Prover、ReProver 等已经解决率更高。但你要放到当时的语境里看这是第一次有人用纯 Transformer 强化学习的方法在形式化数学证明这一“硬核推理”指标上显著超越传统搜索工具而且模型规模还很小。论文的实验设计也给后来者提供了一个标准范式用什么数据训练、怎么生成目标、如何用搜索树增强后续论文大量沿用了这套框架。3.3 手工形式化证明的案例分析论文除了跑 benchmark还挑了一个比较有代表性的定理做案例研究。我记得比较清楚的是它对某个数论或分析性质的证明过程做了解析并和人类证明做了对比。有个细节让我印象很深模型产出的证明路径和人类教材里的标准证明并不一样但每一步都是合法的。这说明模型不是简单记忆了某个标准解法而是真的在搜索空间里找到了一条可行路径。这在自动定理证明里是很有价值的因为很多拓扑、代数问题的证明路径不唯一模型能找到一条不常见但正确的路径意味着它具备了一定程度的“创造性”。当然论文也坦诚说明了当前模型找到的证明往往比较长、比较绕人类读者可能觉得不太优雅。这提醒我们AI 的形式化推理能力还处于“能证明”阶段距离“优雅地证明”还有距离。3.4 消融实验里藏着哪些门道消融实验是论文里信息密度最高、最值得仔细读的部分。作者逐个移除组件看最终指标变化我挑几个重点说去掉教材生成器后模型只能依靠原始证明库做监督训练性能显著下降。这说明自监督数据是训练的核心燃料。去掉价值模型、只用贪心搜索时性能同样下降因为模型在某个局部状态犯错后无法回溯。增大集束搜索宽度比如从 beam size 1 增加到 32可以提升性能但收益会递减同时计算成本增长很快。这些实验看起来简单但对复现者来说是极好的调参指南。比如你想在 Lean 上复现类似方法第一步就该考虑怎么构造一个“教材生成器”而不是急着堆模型参数量。4. 这篇论文的真正意义与还存在的问题4.1 把“推理能力”变成可训练的工程问题过去哲学层面讨论“AI 到底能不能推理”往往众说纷纭。这篇论文的聪明之处在于它不跟你争论抽象定义而是把一个严格的推理任务形式化为“搜索合法证明步骤”然后用标准的机器学习流程把它解掉了。形式化数学的好处是证明过程可以被机器完全验证所以模型的错误不会像自然语言回答一样被掩盖。这让论文的每一个结论都极其扎实GPT-f 会证明就真的能给出可通过验证的证明链。你完全可以把这套“可验证环境 合成目标 策略学习”的框架平移到其他领域比如程序合成、芯片验证、协议分析。只要环境能提供严格的反馈信号方法就有用武之地。4.2 局限一搜索成本仍然高得吓人论文里的模型虽然小但证明搜索过程的计算量可不小。为了证明 miniF2F 上的几十道题算法需要探索成千上万条证明路径每条路径又涉及多次模型前向推理和环境验证。论文在附录里给出了详细的计算资源清单动用了几十块 GPU 和大量 CPU 验证节点。这对复现者来说是很现实的挑战。如果你只有一块消费级显卡想完整复现论文的实验并不容易。我的建议是先从少量题目、较小规模开始比如只跑 miniF2F 中的 20 道简单题把训练和搜索流程打通再逐步放大。论文本身也提供了开源代码和预训练模型权重这大大降低了入门门槛。4.3 局限二对已有证明语料的强烈依赖GPT-f 的成功离不开 set.mm 和 Metamath 生态的数十年积累。不是每个领域都有这样高质量、大规模、严格验证过的形式化知识库。如果你想把这套方法迁移到新的数学分支或者迁移到物理、工程领域第一个卡点就是没有足够的“已经证明过的定理”来生成训练数据。论文中“教材生成器”能工作是因为 set.mm 里已经有大量中等难度的中间状态可以抽取。换一个只有几十条定理的冷门领域这个方法就转不动了。这也是为什么后来很多团队把精力放在自动构建形式化语料库上比如从 LaTeX 论文中半自动抽取数学命题并翻译成 Lean 语句。4.4 与后续工作的演进关系这篇论文发表后自动定理证明ATD社区迅速“卷”了起来。它直接启发了后来的很多研究方向用更强的预训练语言模型如 Codex、GPT-4替换 GPT-f 作为策略模型大幅提升 zero-shot 泛化能力。引入更先进的搜索算法比如 Best-first Search、MCTS 的变体替代简单的集束搜索。在 Lean 生态上构建了更大的证明语料库和基准测试比如 ProofNet、Mathlib 等。将证明搜索与强化学习结合得更紧密让模型直接通过尝试证明来学习而不是依赖大量人工标注。如果你读完这篇论文后想继续深入我建议按这个顺序读先读附录里的证明示例理解 Metamath 的证明格式再复现论文的 baselines最后再看 Lean 方向的相关工作。这样一路下来你会对“AI 形式化推理”这个方向形成比较完整的认知。最后分享一点个人体会我最欣赏这篇论文的地方是它把“数学推理”这个宏大命题拆解成了可以迭代优化的工程问题。它没有等待某个“通用推理能力”的神话降临而是就用已有的 Transformer、已有的证明库、已有的搜索算法认认真真做了一套在标准评测上跑得通的系统。这种务实的研究态度比任何花哨的模型架构都更值得学习。
