Kimina-Prover：在大型形式推理模型上應用測試時強化學習搜尋
Hugging Face 已發布 Kimina-Prover-72B，這是一款基於 Qwen2.5-72B、透過 Kimi k1.5 RL 管線訓練的最先進形式定理證明模型。透過引入測試時強化學習（Test-Time Reinforcement Learning，TTRL）搜尋框架與整合式錯誤修正機制，該模型在 miniF2F 基準上達到創紀錄的 92.2% 通過率。
除了 72B 旗艦模型外，還提供兩個蒸餾變體：Kimina-Prover-Distill-8B（基於 Qwen3-8B）和 Kimina-Prover-Distill-1.7B（基於 Qwen3-1.7B）。
在 miniF2F 上的最先進表現
Kimina-Prover-72B 在多種抽樣預算下均優於先前的形式推理模型。根據提供的基準測試，該模型在 pass@1 上達到 63.9%，在 pass@32 上達到 84.0%，在 pass@1024 上達到 87.7%。當完整的 TTRL 搜尋框架被套用時，通過率提升至 92.2%。
| 模型 | pass@1 | pass@32 | pass@1024 |
|---|---|---|---|
| Kimina-Prover-1.7B | 46.7 | 73.4 | — |
| DSP+ | 52.5 | 71.3 | 80.7 |
| DeepSeek-Prover-V2-7B | 58.6 | 75.6 | 79.9 |
| Kimina-Prover-8B | 61.1 | 78.3 | — |
| DeepSeek-Prover-V2-671B | 61.9 | 82.4 | 86.6 |
| Kimina-Prover-72B | 63.9 | 84.0 | 87.7 |
測試時強化學習（TTRL）搜尋
為了解決需要長時間推理的複雜問題，Kimina-Prover 採用了 TTRL 搜尋框架，使模型能自主發現、組合與重複使用中間引理。
引理啟用模式
在 RL 訓練期間，模型會接觸到「引理啟用模式」：隨機選取一至三個形式引理，將其前置於問題上下文。為確保模型真的使用這些引理，我們採用了基於偏好之獎勵塑形策略：利用提供的引理的解答會獲得較高獎勵，忽略引理的解答則會被懲罰。此策略使引理使用率達到 30–40%。
遞迴搜尋與過濾
TTRL 透過以下機制從隨機探索轉向策略性搜尋：
- Dynamic Scoring：系統為每個候選引理追蹤「引理使用分數」。在每次 RL 迭代中，60% 的輸入使用排名最高的引理，40% 的輸入則加入隨機引理以鼓勵探索。
- Pruning：若引理在 50 次嘗試後未達到 $ au=0.10$ 的使用分數，則將其剔除。
- Recursive Decomposition：若在 $N=128$ 次嘗試後仍未解決某個定理或引理，系統會產生新的候選子引理，遞迴地將問題分解為更小的子問題。
- Negation Filtering：為防止模型利用邏輯不一致的引理，系統會嘗試證明每個新引理的否定式；若否定式可證，則該引理被丟棄。
整合式錯誤修正功能
Kimina-Prover 能夠解讀 Lean 4 的錯誤訊息並提出針對性的修正，這比從頭重新生成證明更具樣本效率。
SFT 資料與批次失敗重放
由於一般大型語言模型在處理 Lean 錯誤訊息時表現不佳，團隊建立了一套專門的監督式微調（Supervised Fine-Tuning，SFT）資料集，內容為三元組：(錯誤證明、Lean 反饋、正確證明)，並以 Claude 3.7 Sonnet 生成的推理鏈進行擴充。
為了穩定訓練，團隊實施了 Batched Failure Replay 策略。失敗的嘗試不會立即被修正，而是從第 $N$ 次迭代收集起來，與第 $N+1$ 次迭代的標準問題混合，確保模型持續接觸錯誤修正任務。
效率提升
錯誤修正在固定計算預算下顯著提升成功率。在對 59 題困難 MiniF2F 問題的測試中，「16+16 嘗試與修正」策略（16 次初始嘗試 + 16 次修正）達到 35.6% 的成功率，而使用 32 次獨立嘗試的「32x1 暴力」策略僅為 28.8%。
其他技術增強
- Continuous Pre-training (CPT)：模型在 60 億 token 的資料集上進行持續預訓練，其中包括 2.6 億來自 GitHub 的 token 與 55 億經編譯器驗證的 rollout 資料。
- Random Proof Cut Augmentation：為利用人工標註的證明，團隊使用「Proof truncation」（刪除證明結尾）與「Proof infilling」（以
sorry替換內部區塊）的方法，教導模型填補與銜接邏輯缺口。 - Prompt Set Curation：訓練集被精煉至約 9 萬題以競賽為導向的問題，透過動態過濾剔除過於簡單的題目，並將仍然過難的題目進行分解。
- Non-proof Problem Solving：模型能處理需要最終答案的問題，先推導出答案，再生成形式化證明以作說明。