Kimina-Prover-RL リリース

Hugging Faceは、Lean 4における形式的な定理証明のために設計されたオープンソースのトレーニングパイプラインであるkimina-prover-rlを発表しました。このシステムは、DeepSeek-R1に触発された「思考してから生成する」という構造化された推論パラダイムを利用しており、0.6Bから1.7Bパラメータの範囲のオープンソースモデルにおいて、最先端（SOTA）の性能を達成しています。

新しいSOTA小型モデル

kimina-prover-rlパイプラインを使用して、MiniF2Fベンチマークにおいて、そのサイズカテゴリで新しいベンチマークを確立する2つの新しいモデルが作成されました。

AI-MO/Kimina-Prover-RL-1.7B: **Pass@32で76.63%**を達成。
AI-MO/Kimina-Prover-RL-0.6B: **Pass@32で71.30%**を達成。

技術的アーキテクチャとトレーニングパラダイム

Kimina-Prover-RLは、モデルがまず自然言語による推論プロセス（<think>ブロック内に記述）を生成し、その後に対応するLean 4コードを生成するという、2段階の出力構造を採用しています。この計画と実行の分離は、、説明可能性、エラー回復、および汎化性能の向上を目的として設計されています。

GRPOとDrGPOによる強化学習

このパイプラインは、オープンソースのVerlフレームワークを介して実装されたGroup Relative Policy Optimization (GRPO)を使用しています。最適化のバイアス（具体的には、GRPOが誤った出力に対して不自然に長い回答を生成する傾向）を軽減するため、チームはDrGPOを利用しました。これは、グローバルな定数で正規化することでトークンレベルの損失を合算し、長さのバイアスを排除する手法です。

報酬メカニズム

報酬は、主に2つの基準に基づいて割り当てられます：

検証報酬: kimina-lean-serverによってLeanコードが正常に検証された場合、報酬1が与えられます。
フォーマット報酬: 構造的な一貫性を確保するため、出力が不正な形式である場合、モデルはゼロ報酬を受け取ります。フォーマットチェックには以下が含まれます：
- 出力ごとに、正確に1つの<think>ブロックと1つのLean 4コードブロックが含まれていることの検証。
- 繰り返しの推論行の拒否。
- tacticブロック内の非コメント行が十分な数であることの確認。
- コメント密度に閾値を適用し、ボイラープレート（定型文）を罰する。
- 記述されたtacticと最終的なコードの間の意味的な整合性を、マッチングスコア（例：Intersection-over-Union）を使用して測定する。
- 不必要に長い回答を罰する。

エラー訂正メカニズム

失敗から学ぶ能力を高めるため、パイプラインにはエラー訂正ターンが組み込まれています。ロールアウトが失敗した場合、システムはプロンプト、回答、およびLeanのフィードバックを保存して、新しいトレーニングサンプルを作成します。その後、モデルに対して、以前の推論とコードを修正するように明示的に促すことで、モデルが自身の出力をデバッグすることに成功した場合に報酬を与える、マルチターンな対話チェーンを可能にします。

データとインフラストラクチャ

データセット: Kimina-Prover-Promptset

モデルは、NuminaMath-LEANの精選されたサブセットであるKimina-Prover-Promptsetでトレーニングされました。データセットは、以下の方法で洗練されました：

簡単な問題（過去の勝率 > 0.5）の削除。
Geminiを使用して問題のバリエーションを生成し、多様性を高める。
難しい問題を複製して、トレーニングの重みを増やす。

高スループット検証

RLロールアウト中に必要とされる並列な証明検証の規模に対応するため、チームは、並列Lean 4検証のためのオープンソースサーバーであるkimina-lean-serverを開発しました。APIとのやり取りを行うためのコンパニオンPythonパッケージであるkimina-clientは、PyPIで利用可能です。

パフォーマンス結果

8台のH100 GPUで48時間トレーニングを行った結果、一貫した改善が見られました。ステップ85までに、best@8メトリックは70%に達し、エラー訂正ターンの後には74%に増加しました。

MiniF2Fベンチマークにおいて、RLチューニングされたモデルと、蒸留された以前のモデルを比較すると以下の通りです：

Model	Pass@32	Pass@32 with error fixing
AI-MO/Kimina-Prover-Distill-1.7B	72.95%	75.41%
AI-MO/Kimina-Prover-RL-1.7B	76.23%	77.87%

0.6Bモデルについては、Pass@32において、パフォーマンスが68.85%（Distill）から71.30%（RL）へと向上しました。