Kimina-Prover: 大規模形式推論モデルへのテスト時強化学習探索の適用
Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
Numina & Kimi Teamは、Qwen2.5-72BをベースにKimi k1.5強化学習パイプラインで訓練された最先端の定理証明モデル「Kimina-Prover-72B」を発表しました。また、Qwen3-8BおよびQwen3-1.7Bをベースにした蒸留バリアント「Kimina-Prover-Distill-8B」と「1.7B」もリリースしました。主な革新点として、複数の補題を再帰的に発見、結合、適用して複雑な証明を構築する訓練可能なエージェンティック証明フレームワーク「Test-Time Reinforcement Learning Search」と、Leanのエラーメッセージを解釈しターゲットを絞った修正を提案できる「Error-Fixing Capability」が挙げられます。これらの進歩により、Kimina-ProverはミニF2Fベンチマークで92.2%の最先端パスレートを達成し、従来のメソッドを上回りました。このモデルは、テスト時強化学習探索フレームワークとエラー修正機能を統合し、自動定理証明の分野で大幅な進歩を示しています。
- Numina & Kimi TeamがKimina-Prover-72Bおよび蒸留バリアントを発表
- Kimina-ProverがミニF2Fベンチマークで92.2%のパスレートを達成
Kimina-Proverは、Kimi k1.5の強化学習パイプラインとテスト時探索を定理証明に応用した点が注目に値する。数学的推論はLLMの収益化において最も価値の高いユースケースの一つであり、ミニF2Fベンチマークで92.2%のパスレートを達成したことは、形式的検証やコード生成分野での応用可能性を示唆する。NuminaとKimi(Moonshot AI)の協業は、中国AIスタートアップによるオープンソースモデル戦略の一環として、基盤モデル競争における差別化要因になり得る。