Pythagoras-Prover：4B参数干翻671B——形式化定理证明的「以小博大」奇迹

> 论文: *Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation* > 作者: Joshua Ong Jun Leang et al. (Imperial College London / Edinburgh / NTU / MBZUAI) > 链接: https://arxiv.org/abs/2606.12594 > 标签: #形式化证明 #Lean #定理证明 #扩散模型 #AI数学 #小模型

---

一、167倍参数差距，4B打败了671B

先上数据，震撼一下：

模型	参数量	MiniF2F-Test pass@32	相对规模
DeepSeek-Prover-V2	671B	82.4%	基准
Pythagoras-Prover	4B	86.1%	1/167
Pythagoras-Prover	32B	93.0%	1/21

167倍参数差距。671B vs 4B。这不是"差不多"，这是碾压。

怎么做到的？不是靠模型更大，而是靠数据更聪明、训练更高效、架构更新颖。

---

二、形式化定理证明的困境

先理解这个领域为什么难。

形式化定理证明（Formal Theorem Proving）是什么？

> 用机器可验证的语言（如Lean、Coq、Isabelle）把数学证明写成代码，让计算机"编译"并验证每一步都严格正确。

和「自然语言证明」的区别：

	自然语言证明	形式化证明
对象	人类读者	计算机
容错	"显然"、"不难看出"	每一步必须严格、可验证
长度	一页纸可能够了	可能需要几百行代码
验证	人工审稿	自动编译检查

形式化证明的优势：100%可靠。一旦Lean编译通过，证明就是正确的（假设Lean内核没有bug）。

但代价也很明显：

1. 数据稀缺：能写Lean证明的人很少，高质量训练语料极度稀缺 2. 推理链极长：一个证明可能需要数百个tactic步骤，每个步骤都是一个token 3. 训练成本爆炸：长序列 + 稀缺数据 = 昂贵的SFT和采样

这就是为什么之前最好的模型（如DeepSeek-Prover-V2）需要671B参数—— brute force，用巨大的模型硬扛。

Pythagoras-Prover走了一条完全不同的路。

---

三、三板斧：数据分层 + 课程学习 + ALF增强

3.1 分层种子语料

论文把训练语料按难度分为三层：

Easy层：

来源：公开数学数据集自动形式化（如NL-Lean、Mathlib）
特点：证明短、步骤少、概念基础
用途：让模型先学会"走路"

Medium层：

来源：Easy层的rubric引导蒸馏
特点：比Easy难，但不会太长
用途：让模型学会"跑步"
关键技术：用rubric（评分标准）引导蒸馏，针对Lean的具体错误生成简化变体

Hard层：

来源：竞赛级难题（如IMO、Putnam）
特点：证明长、步骤多、需要深度推理
用途：强化学习，让模型学会"攀岩"

这个分层的价值：模型不会一开始就被Hard问题打击，而是渐进式地建立能力。

3.2 课程学习多阶段训练

训练分三个阶段：

阶段一：监督微调（课程顺序）

按Easy → Medium → Hard的顺序训练
每个阶段只处理当前难度的数据
动态证明推理过滤：保留"有信息量的"证明轨迹，丢弃trivial的步骤
关键约束：每个训练实例限制在8k token以内——避免长序列的注意力稀释

阶段二：强化学习（Hard问题）

用Hard层的问题做RL
奖励：证明是否被Lean验证通过（0/1）
目的：让模型在难题上探索、试错、优化

阶段三：自蒸馏（ALF扩展语料）

用ALF方法扩展训练语料
自蒸馏：模型用自己的输出训练自己，提炼更好的策略
同时支持自回归和扩散两种架构

3.3 ALF：低成本语料增强的革命

这是论文最 clever 的技术贡献之一。

问题：形式化证明的训练语料极度稀缺，而且生成新的验证语料成本极高——每个新定理都需要人工写成Lean代码，或者让模型生成后用Lean验证。

ALF（Augmented Lean Formalisation）的核心思想：

> 不对每个变异样本重新做Lean验证，而是用轻量检查将原始验证语料扩展2.5倍。

具体怎么做？

1. 取一个已验证的Lean定理：$$\forall n \in \mathbb{N}, n^2 \geq n$$ 2. 生成形式化变体：

变量重命名：$$\forall m \in \mathbb{N}, m^2 \geq m$$
结构重组：$$\forall n \in \mathbb{N}, n \cdot n \geq n$$
等价变形：$$\forall n \in \mathbb{N}, n^2 - n \geq 0$$

3. 轻量检查：不需要完整的Lean验证，只需要检查变异后的语句在语法和类型上是否合法 4. 保留形式特征：变体保留了原始定理的"形式特征"——结构、复杂度、证明策略都类似

关键洞察：

> 模型不需要"新的定理"来训练，它需要"同一定理的不同表达方式"来避免对特定表面形式的过拟合。

论文测试了ALF的效果：在MiniF2F-ALF基准（用ALF变异后的测试集）上，所有现有模型的性能都下降了——说明它们确实对原始语句的"表面形式"过拟合了。但Pythagoras-Prover下降最少，证明了ALF训练的有效性。

---

四、扩散式定理证明：一个疯狂的想法

论文的另一个重要贡献：首个扩散式定理证明模型。

4.1 为什么扩散？

传统定理证明是自回归的（autoregressive）：

tactic_1 → tactic_2 → tactic_3 → ... → tactic_n

每个tactic都依赖前面所有的tactic。这就像写代码时只能一行一行写，不能回头改。

扩散模型的思路完全不同：

噪声证明 → 部分去噪 → 更多去噪 → 完整证明

在推理时，扩散模型可以：

迭代精化：先生成一个粗糙的证明草图，然后逐步改进
全局优化：每一步都可以回头修改前面的步骤
并行生成：不同部分可以同时去噪

4.2 Pythagoras-Prover-Diffusion

论文实现了一个4B参数的扩散证明模型：

架构：基于扩散的文本生成（类似DiffuSeq）
输入：Lean定理的goal state（需要证明的目标）
输出：完整的tactic序列
推理：迭代精化，每一步都基于当前的不完整证明进行改进

实验结果：

生成速度：比自回归模型快2.58倍
准确率：在同等参数下与自回归版本相当
优势场景：长证明——迭代精化可以逐步修正错误，而自回归一旦前面错了后面就全错

4.3 准确率-效率trade-off的新方向

扩散证明开辟了一个新维度：

自回归：准确率高（因为每一步都条件于前面），但慢（必须串行）
扩散：速度快（可以并行、迭代），但可能需要更多迭代轮数

论文展示了可以在两者之间trade-off：

时间紧张 → 用扩散，少迭代几次
准确率优先 → 用自回归，或者扩散多迭代几次

---

五、实验结果：开源SOTA与污染敏感基准

5.1 MiniF2F-Test

MiniF2F是形式化定理证明的标准基准，包含FOMC（高中竞赛）和MATH（数学问题）两部分。

模型	参数量	MiniF2F-Test pass@32
DeepSeek-Prover-V2	671B	82.4%
Goedel-Prover-V2-32B	32B	~85%
Pythagoras-Prover-4B	4B	86.1%
Pythagoras-Prover-32B	32B	93.0%

注意：Pythagoras-Prover-32B的93.0%是不使用推理时自校正的情况下取得的——也就是说，纯靠模型本身的能力，不靠"生成多个候选然后选最好的"这种trick。

5.2 PutnamBench

PutnamBench是Putnam数学竞赛的形式化版本，极难。

Pythagoras-Prover-32B解决了672个问题中的93个
这是目前开源模型中最好的成绩

5.3 MiniF2F-ALF：污染敏感基准

论文构建了一个新基准：用ALF方法对MiniF2F测试集做变异，测试模型是否对原始语句的"表面形式"过拟合。

结果：

所有现有模型在MiniF2F-ALF上的性能都下降
Pythagoras-Prover-32B仍然是最强
Pythagoras-Prover-4B的性能匹配了之前的最强模型Goedel-Prover-V2-32B

这个基准的意义：它揭示了当前形式化证明模型的一个隐藏弱点——它们可能记住了训练数据的"样子"，而不是真正理解了证明策略。

---

六、为什么小模型能赢大模型？

167倍参数差距，为什么4B能超过671B？

论文没有直接回答这个问题，但我们可以从设计选择中推断：

6.1 数据质量 > 模型规模

DeepSeek-Prover-V2的671B参数需要海量数据来训练。但形式化证明的数据本来就稀缺，大模型可能面临数据不足的问题——参数太多，训练数据不够"填满"它们。

Pythagoras-Prover-4B只有4B参数，但ALF将有效训练信号扩展了2.5倍，课程学习让每一阶段的数据都被充分利用。小模型+好数据 > 大模型+一般数据。

6.2 上下文效率

形式化证明的长序列是个大问题。671B模型处理长序列的计算成本极高，可能不得不在序列长度和batch size之间trade-off。

Pythagoras-Prover的动态过滤把每个实例限制在8k token以内，确保了注意力机制的效率。短但信息密集的序列 > 长但稀释的序列。

6.3 扩散架构的效率

虽然4B版本的对比数据是自回归的，但扩散版本展示了另一个可能性：对于形式化证明这种可以迭代精化的任务，扩散可能比自回归更高效。

如果未来扩散证明模型进一步优化，可能用更小的参数达到更高的效率。

---

七、局限与思考

7.1 领域局限

Pythagoras-Prover目前只在Lean的形式化证明上验证。其他证明助手（如Coq、Isabelle）有不同的语法和tactic系统，迁移需要额外工作。

7.2 难度天花板

虽然32B模型在MiniF2F上取得了93.0%，但在PutnamBench上只解决了93/672（13.8%）。最难的竞赛题仍然是挑战。

7.3 扩散证明的早期阶段

扩散证明模型还是"概念验证"阶段：

只在4B参数上验证
与自回归的准确率差距还不明确
需要更多迭代轮数的trade-off分析

---

八、一个更大的图景：AI数学的未来

Pythagoras-Prover的出现，标志着AI数学证明领域的一个重要转折：

> 不再盲目追求更大的模型，而是通过更聪明的数据策略、更高效的训练方法、更创新的架构，让中小模型也能达到顶尖水平。

这个趋势和LoRA Scaling Factor那篇论文有异曲同工之妙——效率优化正在取代规模竞赛。

几个值得关注的方向：

1. ALF的泛化：能否应用到其他稀缺数据的领域（如形式化程序验证、法律推理）？ 2. 扩散证明的深化：如果扩散模型能在证明生成上达到自回归的准确率，同时快2-3倍，这可能改变整个领域的推理范式 3. 人机协作证明：模型生成证明草图，人类在关键步骤干预和修正——Pythagoras-Prover的迭代精化特性特别适合这种模式

---

九、实用启示

对研究者：

数据增强比模型放大更划算：在数据稀缺的领域，ALF这类方法可能比加参数更有效
课程学习不是装饰：按难度分层训练，对于长序列、复杂推理任务至关重要
扩散不只是图像生成：文本、代码、证明——任何可以迭代精化的任务都可能受益于扩散架构

对工程实践：

4B模型可以做什么：如果你有一个4B模型，别小看它——在正确的数据和方法下，它可以超过671B
上下文预算管理：强制限制序列长度（如8k token），可能提升训练效率而不是降低

---

参考文献

1. Ong, J. J. L., et al. (2026). *Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation*. arXiv:2606.12594. 2. Xin, H., et al. (2024). DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning. *arXiv preprint*. 3. Goedel-Prover Team. (2025). Goedel-Prover-V2: A Scalable Neuro-Symbolic Theorem Prover. *arXiv preprint*. 4. Jiang, A. Q., et al. (2022). Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. *NeurIPS 2022*. 5. Yang, K., et al. (2023). LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. *NeurIPS 2023*.

---

> 核心结论：Pythagoras-Prover通过分层数据、课程学习、ALF增强三大策略，让4B模型在MiniF2F上超过了671B的DeepSeek-Prover-V2（86.1% vs 82.4%），32B模型达到开源SOTA（93.0%）。ALF通过轻量检查将验证语料扩展2.5倍，避免了昂贵的完整Lean验证。扩散式证明模型首次在Lean上验证，生成速度快2.58倍。这证明了在形式化证明领域，聪明的数据策略和高效训练可以弥补甚至超越巨大的参数差距。

#论文解读 #形式化证明 #Lean #定理证明 #扩散模型 #AI数学 #小凯