Kimina-Prover-RL: Lean 4向け定理証明器学習パイプラインの公開

NuminaとKimiは、Lean 4における形式定理証明のためのオープンソース学習パイプライン「kimina-prover-rl」を公開した。これはDeepSeek-R1に着想を得た構造化された推論・生成パラダイムに基づき、Verlフレームワークと互換性がある。このパイプラインを用いて、1.7Bパラメータモデル「AI-MO/Kimina-Prover-RL-1.7B」はMiniF2Fベンチマークで76.63%のPass@32を達成し、0.6Bパラメータモデル「AI-MO/Kimina-Prover-RL-0.6B」は71.30%を達成した。これらは同サイズのオープンソースモデルとして最高性能である。学習にはGRPO(DrGPOを使用)が採用され、推論ブロックとLeanコードブロックの二段階構造、フォーマットチェック報酬、エラー訂正メカニズムが特徴である。また、高スループットな並列証明チェックサーバー「kimina-lean-server」も同時に公開された。学習データには、Geminiで生成された問題のバリアントや重複が含まれるKimina-Prover-Promptsetが使用された。