論文の概要: Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

• arxiv url: http://arxiv.org/abs/2504.11354v1
• Date: Tue, 15 Apr 2025 16:23:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-16 22:10:23.453155
• Title: Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
• Title（参考訳）: Kimina-Proverプレビュー:強化学習による大規模形式推論モデルを目指して
• Authors: Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, Jia Li,
• Abstract要約: Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。 Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。 Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
• 参考スコア（独自算出の注目度）: 38.4246156415702
• License:
• Abstract: 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
• Abstract（参考訳）: 我々は、このプレビューリリースで紹介されているように、フォーマルな定理証明のための新しい推論駆動探索パラダイムを開拓した、大規模な言語モデルであるKimina-Prover Previewを紹介します。 大規模な強化学習パイプラインをQwen2.5-72BからトレーニングしたKimina-Prover氏は,“textit{formal reasoning pattern}”という構造的推論パターンを用いることで,Lean 4の証明生成において強力なパフォーマンスを示す。 このアプローチによって、モデルがリーンで人間の問題解決戦略をエミュレートすることが可能になる。 Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。 ベンチマーク性能の改善に加えて,本研究は,(1)最小サンプリング(pass@1)でも高いサンプル効率を示し,その特異な推論パターンとRLトレーニングから起因して,計算予算を効果的にスケールアップする,(2)モデルサイズによる明確なパフォーマンススケーリングを示す,(3)従来の検索アルゴリズムとは異なる学習的推論スタイルは,形式的検証と形式的数学的直観のギャップを埋める可能性を示唆する,といった重要な知見を得た。 我々はKimina-Proverの1.5Bおよび7Bパラメータによる蒸留版をオープンソース化した。

関連論文リスト

• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Metastable Dynamics of Chain-of-Thought Reasoning: Provable Benefits of Search, RL and Distillation [40.861314212279474]
  メタスタブルマルコフプロセスとしてチェーン・オブ・シント(CoT)生成による推論時間計算について検討する。 スパースエッジに報酬を与える検索プロトコルの実装は、異なるクラスタに到達するための期待するステップ数を減らし、CoTを改善することを実証する。 また,検索によって得られる情報を利用して,より優れた推論モデルが得られることを示す。
  論文  参考訳（メタデータ） (2025-02-02T18:19:14Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な機能を示した。 本稿では,新しいグラフィカルモデルを用いてLLM推論を定式化する統一確率的フレームワークを提案する。 本稿では,Bootstrapping Reinforced Thinking Process (BRiTE)アルゴリズムについて述べる。
  論文  参考訳（メタデータ） (2025-01-31T02:39:07Z)
• The Surprising Effectiveness of Test-Time Training for Few-Shot Learning [59.309477460893916]
  言語モデル(LM)は、トレーニングディストリビューション内のタスクにおいて印象的なパフォーマンスを示しているが、しばしば構造的に新しいタスクで苦労している。 LMの推論と少数ショット学習能力を改善するメカニズムとして,テストタイムトレーニング(TTT)の有効性を検討する。 本研究は,新しいタスクにおける文脈内学習の限界を強調し,言語モデルの適応性を高めるためのテストタイムトレーニングの可能性を示した。
  論文  参考訳（メタデータ） (2024-11-11T18:59:45Z)
• Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning [11.268313729426627]
  本稿では,形式的推論の領域,特にニューラル定理証明設定における概念実証について述べる。 古典的な報酬最大化強化学習とは異なり、GFlowNetsは合成対象をサンプリングするための有望なアプローチとして登場した。 我々の初期の結果は、GFlowNetが検索環境におけるモデル性能を向上させる可能性を示している。
  論文  参考訳（メタデータ） (2024-10-17T05:10:12Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• Provable Benefits of Overparameterization in Model Compression: From Double Descent to Pruning Neural Networks [38.153825455980645]
  最近の実証的な証拠は、オーバライゼーションの実践が大きなモデルのトレーニングに利益をもたらすだけでなく、軽量モデルの構築を支援することも示している。 本稿では,モデル刈り込みの高次元ツールセットを理論的に特徴付けることにより,これらの経験的発見に光を当てる。 もっとも情報に富む特徴の位置が分かっていても、我々は大きなモデルに適合し、刈り取るのがよい体制を解析的に特定する。
  論文  参考訳（メタデータ） (2020-12-16T05:13:30Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。