論文の概要: Leanabell-Prover: Posttraining Scaling in Formal Reasoning

• arxiv url: http://arxiv.org/abs/2504.06122v2
• Date: Wed, 09 Apr 2025 04:03:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-10 09:45:06.286959
• Title: Leanabell-Prover: Posttraining Scaling in Formal Reasoning
• Title（参考訳）: Leanabell-Prover: 形式推論におけるポストトレーニングスケーリング
• Authors: Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai,
• Abstract要約: 本稿では, 自然言語の推論モデルにおけるブレークスルーと整合性を持たせることを目的として, ATPのポストトレーニング全体について検討する。 我々は,DeepSeek-Prover-v1.5やGoedel-Proverなど,既存のフォーマルプロバーの改良に成功した。
• 参考スコア（独自算出の注目度）: 26.534511088861446
• License:
• Abstract: Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages. To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.
• Abstract（参考訳）: LLMによる自動定理証明(ATP)の最近の進歩は、Lean 4コードによる正式な推論の可能性を強調している。 しかし、Open AI O1/O3とDeepseek R1が示すように、ATPは最近のポストトレーニングスケーリングによってまだ革新されていない。 本研究では, 自然言語の推論モデルにおけるブレークスルーと整合性を持たせることを目的として, ATPのポストトレーニング全体について検討する。 まず,人間の推論と仮説の洗練をエミュレートする認知行動を統合することを目的とした,多くの文対からなるハイブリッドデータセットを用いて,現行のATPモデルを継続的に訓練する。 次に、Lean 4コンパイラが返した成果報酬を使って強化学習について検討する。 本研究では,DeepSeek-Prover-v1.5 や Goedel-Prover など,既存のプロデューサの改良に成功し,全能発電分野における最先端のパフォーマンスを実現した。 例えば、MiniF2F上で59.8%のパスレート(pass@32)を達成する。 これは現在進行中のプロジェクトであり、調査結果を段階的に更新し、データとトレーニングの詳細を公開します。

関連論文リスト

• Escaping Collapse: The Strength of Weak Data for Large Language Model Training [15.77316232527746]
  LLMの性能を継続的に向上させるために、どの程度のキュレーションが必要なのかを理論的に検討する枠組みを開発する。 非合成トレーニングデータのほとんどすべてが品質が悪い場合でも、最適なLCMに収束する訓練手順を述べる。
  論文  参考訳（メタデータ） (2025-02-13T03:20:37Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  推論能力は汎用知能の重要な構成要素である。 OpenAIのoシリーズモデルなどのプロプライエタリ企業による最近の進歩は、推論タスクに顕著な進歩をもたらした。 本稿では、数学的推論タスクのための textbfOutcome textbfREwtextbfArd ベースの強化 textbfLearning により達成できる性能限界を追求する新しい RL フレームワーク OREAL を提案する。
  論文  参考訳（メタデータ） (2025-02-10T18:57:29Z)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs [25.69931278771869]
  本稿では,形式的推論の即時適用シナリオである形式的検証に焦点を当てる。 我々は5つの形式仕様言語で18kの高品質な命令応答ペアを構築した。 フォーマルなデータによる微調整は、数学、推論、コーディング能力も強化する。
  論文  参考訳（メタデータ） (2025-01-27T17:00:56Z)
• Advancing Language Model Reasoning through Reinforcement Learning and Inference Scaling [52.34735382627312]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な能力を示した。 既存のアプローチは主に、効果的なテストタイムスケーリングを達成するために、模倣学習と苦労に依存しています。 我々は、探索を奨励し、推論スケーリングを理解することで、強化学習をスケールするためにT1を提案する。
  論文  参考訳（メタデータ） (2025-01-20T18:33:33Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• InternLM2 Technical Report [159.70692271378581]
  本稿では,オープンソースのLarge Language Models (LLM) であるInternLM2を紹介する。 InternLM2の事前トレーニングプロセスは細部まで詳細に書かれており、多様なデータ型の準備が強調されている。 InternLM2は、4kトークンでトレーニングされた長期的依存関係を効率的にキャプチャし、事前トレーニングおよび微調整の段階で32kトークンに進む。
  論文  参考訳（メタデータ） (2024-03-26T00:53:24Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)

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

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