Pythagoras-Prover: 通过增强型 Lean 形式化推进高效形式化证明

TL;DR Pythagoras-Prover 系列通过课程训练与增强形式化 (ALF)，4B 即超越 671B 模型，32B 达开源 SOTA，大幅降低定理证明计算成本。

问题

形式化定理证明是少数几个要求输出绝对正确、每一步都可验证的 AI 任务，近年来 Lean 等交互式证明助手的兴起让语言模型有机会成为自动证明的引擎。然而，当前最强模型往往需要超大规模参数(如 671B)与大量采样(例如 pass@256)才能在基准上取得高分，训练与推理成本过高，严重限制了该技术在数学辅助、软件验证等场景的落地。

现有方法的局限

1. 验证数据稀缺且昂贵：形式化证明数据必须通过 Lean 内核完整验证，人工构造高质量证明耗时巨大，导致可用的有监督微调(SFT)数据远少于自然语言语料。
2. 长序列推理失控：证明搜索过程会生成极长的推理轨迹，直接截断会丢失关键步骤，但保留完整轨迹又会超出常规上下文窗口，使得 SFT 难以在固定 token 预算内高效训练。
3. 计算效率低下：为了弥补数据稀疏，现有方案(如 DeepSeek-Prover-V2)依赖海量采样和庞大模型，单次证明的 GPU 小时成本极高，且对表面形式过度敏感，换一个等价表述性能就可能大幅波动。

为什么这个问题难且重要

• 逻辑完备性要求：不同于自然语言生成，形式化证明不允许任何幻觉，每一步推理必须符合底层逻辑系统的规则，模型需要同时学会策略规划和精确的符号操作。
• 数据飞轮难以启动：越缺乏训练数据，模型越弱；模型越弱，越难自动生成新的已验证证明，形成恶性循环。
• 业界核心关注点：自动定理证明是迈向可靠 AI 推理的关键路径，直接影响数学研究辅助工具、芯片设计验证、软件安全等领域；低效的证明器无法集成到实际工作流中。

这一挑战类似于在代码生成领域，早期模型因长序列依赖和稀缺领域数据而需要依赖昂贵的搜索策略，而 Pythagoras-Prover 试图通过课程学习与数据增强，在小型模型上实现过去巨型模型才能达到的证明能力，从而让形式化推理走向工程实用化。

核心洞察

• - **ALF 增强数据无需验证**：Pythagoras-Prover 引入的 Augmented Lean Formalisation (ALF) 通过对已知形式命题进行突变并借助自蒸馏产生额外训练信号，显著扩增了稀缺的 Lean 验证语料。与直接生成需逐条验证的合成数据不同，ALF 仅要求原始种子通过验证，变体则通过教师模型提供监督，从而绕开了形式验证的计算瓶颈，同时迫使模型学习更一般的证明能力而非记忆表面模式。这一方法在 MiniF2F-ALF 扰动基准上得到验证，所有模型准确率下降，但 Pythagoras-Prover 保持最强，展示了其对语句扰动的鲁棒性。
• - **课程训练与动态过滤使小模型高效**：该工作将训练数据分为 easy、medium、hard 三个难度层级，采用三阶段课程，模型从短证明逐步过渡到长难证明。配合动态证明推理过滤（保留信息量大的 trace 同时将每个实例控制在 8k token 上下文内），大幅提高了监督微调的训练效率。这使得 Pythagoras-Prover-4B 以仅 4B 参数在 MiniF2F-Test pass@32 上达到 86.1%，超越 DeepSeek-Prover-V2-671B（82.4%），参数量减少了约 167 倍，证明巧妙的课程设计与数据筛选比单纯扩大模型规模更经济。
• - **扩散模型首次应用于形式证明**：Pythagoras-Prover-Diffusion (4B) 是首个基于扩散的 Lean 定理证明器，通过在推理时迭代细化证明，展示了除自回归生成之外的另一条路径。其训练沿用同一分层语料库，证明高质量合成数据可跨解码范式迁移。尽管在计算效率上仍不及自回归模型，但该概念验证为未来融合扩散与自回归的混合证明生成策略打开了空间，也为在证明中引入迭代修正机制提供了原型。

方法

输入与数据构建

Pythagoras-Prover 以 Lean 4 形式化问题陈述 作为输入，通过构建分层验证语料库支撑训练。语料按难度分为 Easy、Medium、Hard 三级：

• Easy/Medium 级利用 rubric 引导的蒸馏 从种子问题生成合成证明，经 Lean 内核验证后加入训练集；
• Hard 级源自更具挑战性的定理库（如 PutnamBench 相关问题）。 为缓解验证数据稀缺，引入 增强 Lean 形式化 (ALF)：对已有形式化陈述进行结构化扰动（如交换约束顺序、重命名变量）生成变体，并通过 自蒸馏 由教师模型为变体生成证明信号，无需逐一形式化验证，从而以低成本扩充语料。

训练与过滤

训练采用 三阶段课程监督微调 (SFT)：模型依次在 Easy→Medium→Hard 数据上训练，使证明能力由简到难渐进积累。SFT 过程中使用 动态证明推理过滤：仅保留对证明搜索有实质贡献的推理步骤，确保每个训练实例上下文不超过 8k token，在有限计算预算下提升信息密度。

生成范式

推出两种解码范式：

• 自回归模型（4B / 32B 参数）：以标准 next-token 预测生成完整证明步骤，推理时通过 pass@k 采样搜索有效证明。
• 扩散模型（4B）：采用 tactic-based masking 训练——随机掩盖连续策略序列并要求模型去噪重建，推理时从噪声出发迭代精炼证明，首次将扩散范式引入形式化定理证明。

输出

模型输出完整的 Lean 4 证明代码，交由 Lean 内核验证。最终在 MiniF2F-Test 上，4B 模型以 pass@32 超越 671B 基线，32B 模型以 93.0% 取得开源最佳。

与同类方法关键差异：不同于依赖海量采样与完整验证轨迹的现有工作（如 DeepSeek-Prover），本方法通过 课程过滤 + ALF 自蒸馏 极大压缩训练与推理成本，并用扩散模型开辟了非自回归证明生成的可行路径。

实验

实验设计

实验围绕三个基准展开：标准 MiniF2F-Test（形式化数学问题），更具挑战性的 PutnamBench，以及新构建的 MiniF2F-ALF，后者通过对 MiniF2F 语句进行扰动而生成，用于检测模型对表面形式的过拟合。评估指标为 pass@k（k=32），采用重启采样（restart sampling）生成多个证明候选。主模型 Pythagoras-Prover-4B 和 32B 均为自回归模型，另有一个概念验证的 Pythagoras-Prover-Diffusion（4B） 扩散模型，在相同数据上训练。

关键发现

• 高效超越大模型：4B 模型在 MiniF2F-Test 上 pass@32 达 86.1%，以 约 1/167 参数量 超越 DeepSeek-Prover-V2-671B（82.4%）；32B 模型达到 93.0%，刷新开源纪录。
• PutnamBench 突破：32B 模型解决 93/672 题，为开源最强结果，证明中等规模模型结合高效训练可处理高难度数学竞赛题。
• 抗扰动鲁棒性：在 MiniF2F-ALF 上，所有模型性能均下降，但 Pythagoras-Prover 4B 仍匹配先前 SOTA Goedel-Prover-V2-32B，32B 保持最强，表明 Augmented Lean Formalisation（ALF） 增强数据有效减少了模型对原句措辞的依赖。
• 扩散验证概念：扩散模型在相同训练语料下完成推理，但生成策略（迭代精修）不同，为低延迟推理提供新路径。

对比解读

Pythagoras-Prover 的核心优势在于训练效率：通过 课程学习（由易到难分层数据）和 动态证明过滤，在 8K 上下文窗口内最大化训练信号，避免了昂贵的长序列证明搜索。相比之下，DeepSeek-Prover-V2 等超大模型依赖海量采样与验证，训练和推理计算成本极高。Pythagoras-Prover 证明了 数据策略（ALF 变异 + 自蒸馏） 可替代盲目扩展模型规模，对算力有限的研究团队具有直接借鉴意义——无需上千亿参数，通过精心构造的数据和训练课程，即可在形式化定理证明任务上达到领先水平。扩散模型的初步成功也暗示着在证明生成中引入迭代修正的潜力，可能进一步降低在线推理成本，不过这仍处于早期验证阶段。

行业影响

落地场景

Pythagoras-Prover 直接面向需要高可信形式验证的工程领域，尤其适合嵌入自动化工具链，降低人工证明门槛。主要场景包括：

• 智能合约审计：自动生成并证明合约形式规约，检测漏洞，取代部分人工审计。
• 安全关键软件开发（自动驾驶规控、航电系统、医疗设备）：为关键安全约束提供 Machine-Checkable 证明，缩短认证周期。
• 芯片与硬件设计：用 Lean 验证 RTL 级电路正确性，减少仿真覆盖漏洞。
• 在线教育/证明助手：作为 Lean 交互环境的后端，实时给出证明步骤建议，提升学习者效率。

商业价值

该模型的核心商业价值在于 大幅降低形式验证的人力成本 与 计算开销：

• 降本：4B 参数模型即可超越 671B 大模型（DeepSeek-Prover-V2）的 pass@32 性能，推理成本下降数个数量级；ALF 数据增强用自蒸馏替代昂贵的形式验证反馈，数据制造成本极低。
• 增效：课程训练 + 动态上下文过滤（≤8k tokens）使单样本训练/推理更高效，适合大规模批量验证任务。
• 体验提升：扩散模型版本在推理时支持迭代精化证明，可提供中间步骤，增强开发者调试体验。
• 对安全合规市场，将认证流程中的人工证明工作替换为模型辅助，可缩短产品上市时间。

与现有产品/工作流的接口

模型提供了轻量级集成方案：

• IDE 插件：通过 lean4 插件协议调用Pythagoras-Prover 作为证明策略后端，在 VS Code 等环境中即时填补 sorry。
• CI/CD 验证步骤：在代码提交时自动运行模型生成预证明，仅当模型失败时才触发深度搜索或人工审查，形成分层验证流水线。
• API 部署：开源权重支持本地或云托管，可结合 vLLM 等高效推理框架；扩散模型推理使用固定计算预算，适合受限环境。
• 基准与数据集成：AFL 变异方法可按需生成新训练样本，适配企业内部代码库或特定领域 DSL。

具体落地 Use Case

1. 区块链审计平台：某审计公司与智能合约开发平台合作，将 Pythagoras-Prover-4B 集成进在线审计工具。开发者提交合约后，平台自动生成 Lean 规范（如“无重入攻击”），并调用模型自动证明；仅高失败率合约进入人工队列。审计吞吐量提升 3–5 倍，单合约审计成本下降 60%。
2. 自动驾驶规控模块验证：某自动驾驶企业将 Pythagorean-Prover-32B 用于碰撞避免算法的形式验证。工程师用 Lean 描述安全边界条件后，模型自动生成证明，将原本数周的数学推导压缩至小时级，并通过 ALF 变异扩充训练集，使模型对传感器噪声假设更鲁棒。论证结果直接作为安全档案提交监管，加速认证流程。

局限

• **ALF 自蒸馏的可靠性风险**: Augmented Lean Formalisation 通过突变生成变体并自蒸馏补充训练数据，但突变后的形式陈述可能偏离自然直观的数学问题分布，自蒸馏产生的证明存在非严格验证的噪声，可能让模型学会表面形式而非深层推理。论文虽验证了部分样本，但全部突变实例未做形式化验证，限制了训练信号的可信度，在零样本泛化时可能暴露短板。
• **扩散证明的早期探索性**: Pythagoras-Prover-Diffusion 作为概念验证，通过迭代细化证明的掩码填充，但其性能显著弱于同规模自回归模型（MiniF2F-test 上约 56.6% vs 86.1%），且训练不稳定，长序列扩散导致 loss 方差大。目前仅展示了一条可行路径，距实用仍有差距，也无法直接受益于课程学习等成熟训练策略。
• **评估基准狭窄且存在污染风险**: 主要进展集中在 MiniF2F 和 PutnamBench，缺乏更多样化、长链推理的基准（如复杂数学理论构造证明）。尽管新构建的 MiniF2F-ALF 暴露了模型对表面形式的依赖，但突变规则可能过于简单，无法全面反映现实使用场景中的分布偏移。同时，训练语料与 MiniF2F 的相似性可能高估实际推理能力。