Kimina-Prover-RL 發佈

Hugging Face 推出了 kimina-prover-rl，這是一個專為 Lean 4 形式化定理證明設計的開源訓練流水線。該系統採用了受 DeepSeek-R1 啟發的結構化「先推理後生成」範式，為 0.6B 到 1.7B 參數範圍內的開源模型實現了頂尖（state-of-the-art）的性能。

全新的頂尖小型模型

kimina-prover-rl 流水線用於產出兩個新模型，它們在 MiniF2F 基準測試中為其尺寸類別設定了新的基準：

  • AI-MO/Kimina-Prover-RL-1.7B：達到 76.63% Pass@32。
  • AI-MO/Kimina-Prover-RL-0.6B：達到 71.30% Pass@32。

技術架構與訓練範式

Kimina-Prover-RL 採用兩階段輸出結構，模型首先生成自然語言推理過程（封裝在 <think> 區塊中），接著生成對應的 Lean 4 程式碼。這種規劃與執行的分離旨在提高可解釋性、錯誤恢復能力和泛化能力。

使用 GRPO 與 DrGPO 的強化學習

該流水線使用 Group Relative Policy Optimization (GRPO)，透過開源框架 Verl 實作。為了減輕優化偏差——特別是 GRPO 容易為錯誤輸出產生人為過長的回答——團隊利用了 DrGPO，透過使用全域常數進行歸一化來聚合 token 級別的損失，從而消除長度偏差。

獎勵機制

獎勵是根據兩個主要標準分配的：

  1. 驗證獎勵：如果 Lean 程式碼成功通過 kimina-lean-server 驗證，則給予 1 分的獎勵。
  2. 格式獎勵：為了確保結構一致性，如果輸出格式錯誤，模型將獲得零分獎勵。格式檢查包括：
    • 驗證每個輸出中恰好包含一個 <think> 區塊和一個 Lean 4 程式碼區塊。
    • 拒絕重複的推理行。
    • 確保 tactic 區塊中有足夠數量的非註解行。
    • 對註解密度應用閾值以懲罰模板化內容。
    • 使用匹配分數（例如 Intersection-over-Union）來衡量描述的 tactics 與最終程式碼之間的語義對齊度。
    • 懲罰不必要的長回答。

錯誤修正機制

為了增強從失敗中學習的能力，該流水線整合了錯誤修正回合。當 rollout 失敗時，系統會儲存 prompt、回答和 Lean 反饋，以建立新的訓練樣本。接著，系統會明確提示模型修正其先前的推理和程式碼，從而實現多輪互動鏈，讓模型因成功調試其自身的輸出而獲得獎勵。

數據與基礎設施

數據集：Kimina-Prover-Promptset

這些模型是在 Kimina-Prover-Promptset 上訓練的，這是 NuminaMath-LEAN 的精選子集。該數據集經過以下優化：

  • 移除容易的問題（歷史勝率 > 0.5）。
  • 使用 Gemini 生成問題變體以增加多樣性。
  • 將困難的問題重複多次以增加其訓練權重。

高吞吐量驗證

為了處理強化學習 rollout 期間所需的並行證明檢查規模，團隊開發了 kimina-lean-server，這是一個用於並行 Lean 4 驗證的開源伺服器。配套的 Python 套件 kimina-client 已在 PyPI 上提供，用於 API 互動。

性能結果

在 8 台 H100 GPU 上訓練 48 小時後，顯示出持續的改進。到第 85 步時，best@8 指標達到 70%，在錯誤修正回合後增加到 74%。

將 RL 微調後的模型與其蒸餾前的版本在 MiniF2F 基準測試上進行比較：

Model Pass@32 Pass@32 with error fixing
AI-MO/Kimina-Prover-Distill-1.7B 72.95% 75.41%
AI-MO/Kimina-Prover-RL-1.7B 76.23% 77.87%

對於 0.6B 模型，該流水線將 Pass@32 的性能從 68.85% (Distill) 提升至 71.30% (RL)。

Sources

相關