Pythagoras-Prover: 通过增强型Lean形式化推进高效形式化证明
Pythagoras-Prover是一个计算高效的Lean定理证明器家族，包含4B和32B的自回归模型以及4B的扩散模型。它通过分层课程SFT和动态证明过滤提高训练效率，并引入增强型Lean形式化(ALF)扩展验证语料库。实验显示，4B模型在MiniF2F-Test上以86.1%的pass@32超越DeepSeek-Prover-V2-671B（82.4%），而32B模型达到93.0%的新开源最佳水平，并在PutnamBench上解决93个问题。
现代Lean定理证明器需要大量的训练和推理计算才能实现强劲性能，这主要是由于可验证的证明数据稀缺以及形式化证明搜索涉及较长的推理轨迹，使得监督微调和采样成本高昂。为了应对这一挑战，研究者提出了Pythagoras-Prover，一个计算高效的开源Lean定理证明器家族，专为实用的计算预算而设计。该家族涵盖了两代生成范式：参数规模为4B和32B的自回归模型，以及一个概念验证性的基于扩散的证明器（4B），后者在推理时通过迭代细化Lean证明来工作。
在训练效率方面，研究团队构建了一个经过Lean验证的语料库，并将其按难度分层为简单、中等和困难问题，用于课程式SFT。通过这种方式，模型能够逐步从较短、较简单的证明中学习，进而掌握更长、更复杂的证明技巧。在SFT过程中，一个动态的证明推理过滤方案能够保留信息量丰富的证明轨迹，同时将每个实例控制在8k token的上下文预算内。此外，Pythagoras-Prover引入了增强型Lean形式化（Augmented Lean Formalisation，ALF），该方法通过将稀缺的验证语料库扩展为正式语句的变体，并利用自蒸馏来填充这些变体，从而在不正式验证每个变异实例的情况下提供额外的训练信号。通过对已知问题进行扰动并保持其形式化特征，ALF减少了对任何语句表面形式的依赖。
实验结果表明，Pythagoras-Prover-4B在MiniF2F-Test上以86.1%的pass@32超越了DeepSeek-Prover-V2-671B（82.4%），而其参数量仅为后者的约1/167。同时，Pythagoras-Prover-32B在MiniF2F-Test上达到了93.0%的pass@32，创下了开源模型的新纪录，并在PutnamBench上成功解决了672个问题中的93个。研究团队还发布了MiniF2F-ALF基准测试，该基准测试通过ALF变异实现污染敏感性，所有评估模型在此基准上的准确率均有所下降。在该基准上，32B模型仍表现最强，而4B模型则与先前的领先模型Goedel-Prover-V2-32B持平。