Kimina-Proverプレビュー：強化学習を用いた大規模形式的推論モデルの構築へ

本稿では、形式定理証明における新しい推論駆動型探索パラダイムを先導する大規模言語モデル「Kimina-Prover Preview」を紹介する。本プレビュー版では、このアプローチの有効性が実証されている。Kimina-Proverは、Qwen2.5-72Bを基盤とする大規模強化学習パイプラインで訓練されており、我々が「形式的推論パターン（formal reasoning pattern）」と呼ぶ構造化された推論フレームワークを用いることで、Lean 4における証明生成において優れた性能を発揮している。このアプローチにより、モデルは人間の問題解決戦略を模倣し、証明ステップを反復的に生成・改善することが可能となる。Kimina-ProverはminiF2Fベンチマークにおいて、pass@8192で80.7％の精度を達成し、新たな最先端水準を樹立した。本研究の成果は、ベンチマーク性能の向上にとどまらず、以下の重要な知見をもたらしている。（1）Kimina-Proverは高いサンプル効率を示し、最小限のサンプリング（pass@1）でも優れた結果を達成でき、計算リソースの増加に伴って効果的にスケーリングする。これは、独自の推論パターンと強化学習による訓練の結果である。（2）モデルサイズの増大に伴い明確な性能向上が確認された。これは、従来の神経ネットワークベース定理証明器においては観察されていなかった傾向である。（3）従来の探索アルゴリズムとは異なる、学習された推論スタイルは、形式的検証と直感的な数学的洞察の間のギャップを埋める可能性を示している。本研究では、Kimina-Proverの蒸留版（1.5Bおよび7Bパラメータ）をオープンソースとして公開する。