Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

要約

このプレビューリリースで紹介されているように、正式な定理を証明するための新しい推論主導型の探索パラダイムを開拓する大規模な言語モデルであるKimina-Prover Previewを紹介します。
QWEN2.5-72Bの大規模な強化学習パイプラインで訓練されたKimina-Proverは、構造化された推論パターンを使用することにより、リーン4プルーフ生成の強力なパフォーマンスを示します。
このアプローチにより、モデルは、無駄のない、繰り返し生成および洗練された証明ステップで人間の問題解決戦略をエミュレートすることができます。
Kimina-Proverは、Minif2Fベンチマークで新しい最先端のベンチマークを設定し、Pass@8192で80.7％に達しました。
ベンチマークのパフォーマンスの改善を超えて、私たちの作業はいくつかの重要な洞察をもたらします。（1）キミーナプロバーが高いサンプル効率を示し、最小限のサンプリング（パス@1）でも強力な結果をもたらし、そのユニークな推論パターンとRLトレーニングに起因する計算予算で効果的にスケーリングします。
（2）モデルサイズの明確なパフォーマンススケーリングを示します。これは、正式な数学の神経定理プローバーには以前は観察されていなかった傾向です。
（3）従来の検索アルゴリズムとは異なる学習された推論スタイルは、正式な検証と非公式の数学的直観と​​のギャップを埋める可能性を示しています。
キミーナプロバーの1.5bおよび7bパラメーターを備えたオープンソース蒸留バージョン

要約(オリジナル)

We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term \textit{formal reasoning pattern}. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover

arxiv情報

提供元, 利用サービス

arxiv.jp, Google