Pythagoras-Prover：通过增强型Lean形式化方法推进高效形式化证明
形式化证明是确保数学定理和软件正确性的关键工具，但长期以来面临数据稀缺和计算成本高昂的挑战。近日，来自爱丁堡大学等机构的研究团队发布了 Pythagoras-Prover，一个计算高效的Lean定理证明器开源家族，旨在以更低的计算预算实现顶尖性能。
核心创新：从数据到架构的全链路优化
Pythagoras-Prover 包含两种生成范式的模型：自回归模型（4B和32B参数）以及首个基于扩散的证明器（4B参数），后者在推理时通过迭代精炼Lean证明。研究团队从三个层面解决效率问题：
课程式监督微调（Curriculum SFT）：构建了一个按难度分层（简单、中等、困难）的Lean验证语料库，让模型从短而简单的证明逐步学习到长而复杂的证明。在SFT过程中，动态的证明推理过滤机制保留了信息量丰富的证明轨迹，同时将每个实例控制在8k token的上下文预算内。
增强型Lean形式化（ALF）：针对已验证语料库稀缺的问题，ALF通过扰动已知问题生成形式化语句的变体，并利用自蒸馏产生额外训练信号，无需逐一验证每个变异实例。这降低了对特定语句表面形式的依赖，提升了模型的泛化能力。
扩散模型试水：4B参数的扩散证明器作为概念验证，展示了在推理时迭代精炼证明的潜力，为形式化证明开辟了新路径。
惊人性能：小模型逆袭大模型
在标准基准测试 MiniF2F-Test 上，Pythagoras-Prover-4B 以 86.1% 的 pass@32 成绩超越了拥有 671B 参数的 DeepSeek-Prover-V2（82.4%），参数规模缩小约 167倍。而 32B 版本以 93.0% 的成绩创下了开源模型的新纪录。在更具挑战性的 PutnamBench 上，32B模型解决了 93道 题目，展示了强大的数学推理能力。
研究团队还发布了 MiniF2F-ALF 基准，该基准通过ALF变异增加了污染敏感性，所有模型在该基准上的准确率均有所下降，但Pythagoras-Prover-32B仍然最强，4B版本则追平了此前最先进的Goedel-Prover-V2-32B。
行业意义：降低形式化证明的门槛
形式化证明领域长期被大模型垄断，但Pythagoras-Prover证明，通过高效的数据增强和训练策略，小模型也能达到甚至超越超大模型的性能。这为资源受限的研究团队和工业应用提供了可行方案，有望加速形式化方法在关键软件验证、数学定理证明等领域的普及。同时，扩散模型的引入也为未来探索更高效的推理范式打开了大门。