Kimina-Prover-RL: Lean 4 定理証明のためのオープンソース強化学習

概要

Kimina-Prover-RL は、Lean 4 で形式証明の目標を解くように大規模言語モデルを訓練するためのオープンソースのトレーニングパイプラインです。DeepSeek-R1 に触発された構造化された推論-生成パラダイムを採用することで、システムはモデルに計画と実行を分離させます。このリリースには、Verl フレームワークと互換性のあるトレーニングレシピと、2つの新しいモデルが含まれています: MiniF2F ベンチマークで Kimina-Prover-RL-1.7B (76.63% Pass@32) と Kimina-Prover-RL-0.6B (71.30% Pass@32)。

トレーニング手法

パイプラインは、グループ相対方策最適化 (GRPO) を使用して、自然言語の推論トレースとそれに続く Lean 4 コードを生成するようにモデルを訓練します。GRPO の既知の最適化バイアス (人為的に長く不正確な出力につながる) を軽減するために、実装では DrGRPO を使用します。これは、トークンレベルの損失をグローバル定数で正規化します。

トレーニングアーキテクチャの主要コンポーネントは次のとおりです:

• 形式報酬: 出力は特定の構造 (1つの thinking... response ブロックと1つの lean4 コードブロック) に対して厳密にチェックされます。不正な形式の出力にはゼロ報酬が与えられます。追加のチェックでは、反復的な推論、幻覚のタクティク、推論とコードの間の意味的整合性の欠如をペナルティします。
• エラー修正: パイプラインにはエラー修正メカニズムが含まれており、証明試行が失敗した場合、モデルは以前の推論とコードを修正するように促されます。これにより、モデルはマルチターン対話で Lean 4 からのフィードバックを学習できます。
• 高スループット検証: 証明チェックの規模を処理するために、システムは kimina-lean-server を使用します。これは、kimina-client Python パッケージを介してアクセスされる並列証明検証をサポートするオープンソースサーバーです。

データセットと設定

モデルは、NuminaMath-LEAN の厳選されたサブセットである Kimina-Prover-Promptset でトレーニングされます。データセットは、「簡単な」問題 (履歴勝率 > 0.5) を削除し、Gemini を使用してバリアントを生成して多様性を高め、難しい問題を複製してトレーニング中の重みを増やすように処理されます。

トレーニング設定は 8 GPU セットアップ用に最適化されており、AI-MO/Kimina-Prover-Distill-1.7B モデル (Qwen/Qwen3-1.7B に基づく) を微調整します。プロセスでは、ステップごとに 256 サンプルを取得し、その半分をエラー修正サンプルとして指定し、サンプルごとに 8 ロールアウトを生成します。

パフォーマンス結果

トレーニングパイプラインは、時間の経過とともに精度と構造的順守の一貫した改善を示しています。8 台の H100 GPU で 48 時間トレーニングした後、1.7B モデルはステップ 85 までに 4 ポイントの精度向上を達成しました。モデルは、MiniF2F でそれぞれのサイズカテゴリの新しい最先端ベンチマークを設定しました:

モデル	Pass@32	エラー修正付き Pass@32
AI-MO/Kimina-Prover-RL-1.7B	76.23%	77.87%
AI-MO/Kimina-Prover-RL-0.6B	71.30%	N/A

トレーニングが進むにつれて、形式エラーの頻度は減少し、出力の平均トークン長は増加します。これは、モデルがより構造化された包括的な推論トレースを開発していることを反映しています。