Kimi 技術團隊近日發佈了 Kimina-Prover 預覽版的技術報告，並開源了1.5B 和7B 參數的模型蒸餾版本、用於數據生成的 Kimina-Autoformalizer-7B 模型以及修訂過的 miniF2F 基準測試數據集。Kimina-Prover 是由 Numina 和 Kimi 團隊聯合研發的一款數學定理證明模型，它在形式化定理證明領域採用了一種新穎的、由推理驅動的探索範式，展現出極佳的性能。

Kimina-Prover 基於 Qwen2.5-72B 模型，並結合 Kimi k1.5的大規模強化學習（RL）流程進行訓練。在權威的 miniF2F 形式化數學基準測試中，Kimina-Prover 預覽版以更低的採樣預算(pass@8192)達到了80.7% 的通過率，顯著超越了之前的最佳結果:BFS Prover 的72.95%(pass@2048×2×600+)和 DeepSeek-Prover 的50.0%(pass@65536)。

微信截圖_20250417082955.png

形式化定理證明是數學和計算機科學領域的一個重要方向，它應用嚴格的數學邏輯和計算機程序來驗證數學定理的正確性。然而，讓 AI 掌握形式化證明極具挑戰，傳統方法往往難以應對複雜、需要深刻洞察力和創造力的數學問題。近年來，大語言模型（LLM）的興起爲這一領域帶來了新的希望，但現有方法大多存在侷限，如依賴外部搜索、難以捕捉深度推理、缺乏模型規模效應等。

爲了克服這些侷限，Kimina-Prover 採用了新的路徑，將大規模強化學習（RL）與“形式化推理模式”深度結合，直接優化模型生成完整證明的內部“策略”。這種方法使得模型能夠在生成 token 的過程中隱式地探索龐大的證明空間，自主地導航推理路徑，極大地降低了計算開銷，並賦予了模型更靈活、更接近人類直覺的探索方式。此外，Kimina-Prover 還引入了基於最終結果的獎勵信號，強化學習的訓練過程是目標導向的，只有完全正確、能通過編譯的證明才能獲得正獎勵。

Kimina-Prover 的初步研究成果取得了顯著進展。在 miniF2F 基準測試中，Kimina-Prover 達到了80.7% 的通過率，顯著超越了之前的最佳結果。它還展現出極高的樣本效率，即使在極少採樣次數下也能取得有競爭力的結果。此外，Kimina-Prover 的性能隨着模型參數規模的增大而持續提升，這是首次在形式化數學領域的神經定理證明器中觀察到如此明確的規模效應。與頂尖的通用推理大模型相比，Kimina-Prover 在形式化數學任務上展現出壓倒性優勢，能夠穩定生成形式正確、可通過 Lean 編譯器檢查的證明。

Kimina-Prover 的思考過程具有很高的可解釋性，用戶可以查看模型是如何一步步推導出證明的，這爲理解模型行爲、診斷失敗原因提供了便利，也使其具備成爲數學教育輔助工具的潛力。研究團隊表示，Kimina-Prover 的性能能夠隨着模型規模和上下文長度的增加而顯著擴展，初步驗證了“基於推理的神經證明器”的潛力。這種結合了大規模強化學習和類人推理模式的方法，將爲自動化推理乃至通用人工智能（AGI）的發展開闢新思路。

爲了推動社區的參與和研究進展，Kimi 技術團隊開源了 Kimina-Prover 的1.5B 和7B 參數的蒸餾版本，用於數據生成的 Kimina-Autoformalizer-7B 模型，以及修訂過的 miniF2F 基準測試數據集。

  • Arxiv 技術報告:https://arxiv.org/abs/2504.11354

  • GitHub 代碼庫:‍https://github.com/MoonshotAI/Kimina-Prover-Preview‍

  • Hugging Face 模型下載:https://huggingface.co/collections/AI-MO/kimina-prover-preview-67fb536b883d60e7ca25d7f9