精选理由
形式化证明领域终于有了计算高效的实用方案——4B 模型就能超越 671B 巨无霸，做定理证明或形式化验证的团队可以直接用，省下大量算力成本。
Pythagoras-Prover 是一个计算高效的 Lean 定理证明器系列，包含 4B 和 32B 参数的自回归模型，以及首个基于扩散的证明器（4B）。通过课程式监督微调和动态证明过滤，训练效率大幅提升。其 4B 模型在 MiniF2F-Test 上以 86.1% 的 pass@32 超越 DeepSeek-Prover-V2-671B（82.4%），参数减少约 167 倍；32B 模型达到 93.0%，创下开源新纪录。团队还提出了增强型 Lean 形式化方法（ALF），通过扰动已知问题生成变体，减少对表面形式的依赖，并发布了 MiniF2F-ALF 基准。
AI 翻译 · 中文
Pythagoras-Prover 是一个计算高效的 Lean 定理证明器系列，包含 4B 和 32B 参数的自回归模型，以及首个基于扩散的证明器（4B）。通过课程式监督微调和动态证明过滤，训练效率大幅提升。其 4B 模型在 MiniF2F-Test 上以 86.1% 的 pass@32 超越 DeepSeek-Prover-V2-671B（82.4%），参数减少约 167 倍；32B 模型达到 93.0%，创下开源新纪录。团队还提出了增强型 Lean 形式化方法（ALF），通过扰动已知问题生成变体，减少对表面形式的依赖，并发布了 MiniF2F-ALF 基准。
Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both …