Pythagoras-Prover：高效形式证明的突破

形式化定理证明是人工智能与数学交叉领域的前沿方向，旨在通过计算机严格验证数学命题的正确性。然而，现有Lean定理证明器在取得强劲性能的同时，也面临着训练和推理计算成本高昂的困境。这主要源于两方面：一是经过验证的证明数据稀缺，二是形式化证明搜索过程产生冗长的推理轨迹，使得监督微调和采样过程都变得异常昂贵。

针对这一挑战，研究团队推出了Pythagoras-Prover，一个计算高效的Lean定理证明器家族，专为实际计算预算设计。该家族涵盖两种生成范式：自回归模型（4B和32B参数）以及首个基于扩散的证明器概念验证（4B），后者能在推理时迭代优化Lean证明。这一多元化的技术路线，为不同规模的计算资源提供了灵活的选择。

在训练效率方面，研究团队构建了一个Lean验证语料库，并将其按难度分层为简单、中等和困难三个级别，用于课程式监督微调。这种渐进式学习策略，使模型能够从更短、更简单的证明逐步过渡到更长、更复杂的证明，从而更高效地掌握证明技能。在微调过程中，一种动态的证明推理过滤方案被引入，它保留了信息丰富的证明轨迹，同时将每个实例控制在8k token的上下文预算内，有效避免了长序列带来的计算负担。

更值得关注的是，研究团队提出了增强型Lean形式化方法（ALF）。该方法将稀缺的验证语料库扩展为形式化语句的变体，并通过自蒸馏技术提供额外的训练信号，而无需对每个变异实例进行形式化验证。通过扰动已知问题同时保留其形式化特征，ALF减少了对任何语句表面形式的依赖，从而增强了模型的泛化能力。

实验结果表明，Pythagoras-Prover-4B在MiniF2F-Test基准上以pass@32指标达到86.1%的准确率，超越了拥有671B参数的DeepSeek-Prover-V2（82.4%），而参数量仅为后者的约1/167。Pythagoras-Prover-32B则进一步将开源模型的性能推向新高，在MiniF2F-Test上达到93.0%的准确率，并在更具挑战性的PutnamBench问题上成功解决了93道题（共672道）。

此外，研究团队还发布了MiniF2F-ALF基准，这是一个经过ALF变异处理的污染敏感测试集。在该基准上，所有被评估的模型准确率均有所下降，但Pythagoras-Prover-32B依然保持最强性能，而4B模型也达到了此前最先进模型Goedel-Prover-V2-32B的水平。这充分证明了Pythagoras-Prover在应对数据污染和泛化挑战方面的卓越能力。

Pythagoras-Prover的出现，不仅为形式化定理证明领域提供了高效、开源的新工具，更通过ALF方法开辟了数据增强的新路径。它预示着，在有限计算资源下，通过巧妙的数据组织和训练策略，小型模型同样能实现甚至超越巨型模型的性能，这对推动AI在数学、软件验证等领域的实际应用具有重要意义。