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持平。