論文の概要: 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-23 23:38:44.199698
• 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: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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パラメータによる蒸留版をオープンソース化した。

関連論文リスト

• 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)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Inference-Aware Fine-Tuning for Best-of-N Sampling in Large Language Models [80.65242356955231]
  本稿では,推論時戦略の性能を直接最適化する手法により,モデルが微調整される,推論対応のファインチューニングパラダイムを提案する。 筆者らは,BoN内における困難で微分不可能なargmax演算子を克服し,BoN対応微調整のための最初の模倣学習と強化学習(RL)手法を考案した。 提案実験では,BoNを意識した微調整の有効性を,性能向上と推論時間計算の両面で実証した。
  論文  参考訳（メタデータ） (2024-12-18T20:43:47Z)
• 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)
• HyperTree Proof Search for Neural Theorem Proving [14.677400513932852]
  本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。 我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
  論文  参考訳（メタデータ） (2022-05-23T17:49:55Z)
• Provable Benefits of Overparameterization in Model Compression: From Double Descent to Pruning Neural Networks [38.153825455980645]
  最近の実証的な証拠は、オーバライゼーションの実践が大きなモデルのトレーニングに利益をもたらすだけでなく、軽量モデルの構築を支援することも示している。 本稿では,モデル刈り込みの高次元ツールセットを理論的に特徴付けることにより,これらの経験的発見に光を当てる。 もっとも情報に富む特徴の位置が分かっていても、我々は大きなモデルに適合し、刈り取るのがよい体制を解析的に特定する。
  論文  参考訳（メタデータ） (2020-12-16T05:13:30Z)

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

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