Kimina-Prover: 形式的定理証明のためのテスト時RL探索

概要

Kimina-Prover-72Bは、Lean 4言語向けに設計された最先端の自動定理証明（ATP）モデルであり、miniF2F-testベンチマークで92.2%の合格率を達成しました。テスト時強化学習（TTRL）探索と新しいエラー修正メカニズムを統合することで、このシステムは単一ステップの推論を超え、複雑な数学的問題を自律的に扱いやすいサブ補題へと分解します。

テスト時強化学習（TTRL）探索

TTRL探索フレームワークは、定理証明をランダムな探索から目標指向のエージェントプロセスへと移行させます。このフレームワークは「補題有効パターン」を利用しており、モデルは中間的な補題を特定し、それを証明構築に組み込むように訓練されています。

TTRLフレームワークの主要なコンポーネントは以下の通りです：

• 動的補題スコアリング: システムは探索範囲内での補題の有用性を追跡し、成功した証明に頻繁に寄与するものを優先しつつ、最小利用しきい値（τ=0.10）を満たさないものを剪定します。
• 再帰的分解: 定理や補題が128回の試行後に証明できなかった場合、システムはサブ補題生成プロセスをトリガーします。これにより、モデルは困難な問題を再帰的に分解し、より小さく証明可能なコンポーネントに分割できます。
• 論理的健全性: モデルが矛盾を悪用して自明な証明を生成することを防ぐため、システムは「否定証明プロセス」を採用しています。生成された補題の論理的否定が証明可能な場合、元の補題は矛盾しているとして破棄されます。

エラー修正とサンプル効率

Kimina-Proverは、Leanのエラーメッセージを解釈して反復的な修正を行うことでサンプル効率を向上させており、証明を最初からやり直す必要はありません。チームは（誤った証明、Leanのフィードバック、正しい証明）のトリプレットで構成される専門的な教師あり微調整（SFT）データセットを開発し、Claude 3.7 Sonnetによって合成されたステップバイステップの推論チェーンで拡張しました。

これを強化学習ループに統合するために、チームは「バッチ失敗リプレイ」戦略を実装しました。過去の失敗と標準的な問題の固定サイズの結合データで訓練することで、モデルは複雑な論理的ミスや構文エラーを解決することを学習し、同等の計算予算下で総当たりサンプリング戦略を一貫して上回る性能を発揮します。

モデルのバリエーションとパフォーマンス

フラッグシップである72Bパラメータモデルに加え、多様なデプロイニーズをサポートするために蒸留されたバリエーションもリリースされています：

• Kimina-Prover-72B: Qwen2.5-72Bベース、miniF2F-testで92.2%を達成。
• Kimina-Prover-Distill-8B: Qwen3-8Bベース。
• Kimina-Prover-1.7B: Qwen3-1.7Bベース。

パフォーマンスデータによると、初期のモデルはサンプリング予算に対して線形にスケーリングしていましたが、現在のシステムではpass@1024を超えると収穫逓減が見られます。これは、さらなる改善が単なるサンプリング量よりも、TTRLが提供する高度な探索戦略に依存していることを示唆しています。