Pythagoras-Prover：透過擴充 Lean 形式化推進高效形式證明
為何重要
這項研究解決了形式化數學證明中計算成本高昂的痛點，讓資源的模型也能透過創新的資料擴充策略產生高品質證明，降低形式驗證的技術門檻。
研究團隊發表了 Pythagoras-Prover，這是一個計算高效且開源的 Lean 定理證明工具家族，包含 4B 和 32B 引數的自迴歸模型，以及其他一個 4B 引數的擴散式證明模型。透過引入 Augmented Lean Formalisation (ALF) 技術與課程式監督微調策略，研究團隊有效解決了形式化證明中資料稀缺的問題。在效能方面，32B 模型在 MiniF2F-Test 測試上取得 93.0% 的準確率，重新整理了開源領域的最佳成績。