論文の概要: LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

• arxiv url: http://arxiv.org/abs/2505.12031v1
• Date: Sat, 17 May 2025 14:47:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-20 14:57:10.99893
• Title: LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
• Title（参考訳）: スケーラブルな合成データ生成に基づくLLM自動定理証明
• Authors: Junyu Lai, Jiakun Zhang, Shuo Xu, Taolue Chen, Zihang Wang, Yao Yang, Jiarui Zhang, Chun Cao, Jingwei Xu,
• Abstract要約: 本研究では,幅広い中間的証明状態にまたがる多様な戦術を創出するために設計された,データ合成の訓練のための新しい実証状態探索手法を提案する。 また,データ合成手法を効果的に活用し,木探索における探索と利用のトレードオフを実現する適応ビームサイズ戦略を提案する。
• 参考スコア（独自算出の注目度）: 11.045086599038338
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、自動定理証明に大きな関心を喚起し、顕著な研究ラインは、段階的にLLMベースのプローバーをツリーサーチに統合している。 本稿では,多岐にわたる中間的証明状態の多様な戦術を創出することを目的とした,データ合成の訓練のための新しい実証状態探索手法を提案する。 また,データ合成手法を効果的に活用し,木探索における探索と利用のトレードオフを実現する適応ビームサイズ戦略を提案する。 MiniF2F と ProofNet のベンチマークによる評価では、この手法は、厳密な Pass@1 メトリックで強いベースラインを上回り、MiniF2F の平均パスレートが 60.74 %、ProofNet が 21.18 % となる。 これらの結果は、自動定理証明の進歩における大規模合成データの影響を裏付けるものである。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• LLM-based MOFs Synthesis Condition Extraction using Few-Shot Demonstrations [31.35595673239483]
  大規模言語モデル(LLM)は、この長年の問題に対する破壊的な新しい解決策を提供する。 本稿では,LLMの文脈内学習パラダイムについて紹介する。 提案した少数ショットLLMの合成,構造推定,材料設計性能は,いずれもゼロショットLLMとベースライン法を大きく上回っている。
  論文  参考訳（メタデータ） (2024-08-06T14:53:25Z)
• Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learning [55.96599486604344]
  本稿では,Large Language Models (LLMs) の推論能力向上を目的とした,反復的な選好学習プロセスによるアプローチを提案する。 我々は、MCTS(Monte Carlo Tree Search)を用いて好みデータを反復的に収集し、そのルックアヘッド機能を利用して、インスタンスレベルの報酬をよりきめ細かいステップレベルの信号に分解する。 提案アルゴリズムはDPO(Direct Preference Optimization)を用いて,新たに生成されたステップレベルの優先度データを用いてLCMポリシーを更新する。
  論文  参考訳（メタデータ） (2024-05-01T11:10:24Z)
• Self-Play Fine-Tuning Converts Weak Language Models to Strong Language Models [52.98743860365194]
  本稿では,SPIN(Self-Play fIne-tuNing)と呼ばれるファインチューニング手法を提案する。 SPINの中心には自己再生機構があり、LLMは自身のインスタンスと対戦することでその能力を洗練させる。 このことは、自己プレイの約束に光を当て、熟練した相手を必要とせずに、LSMにおける人間レベルのパフォーマンスの達成を可能にする。
  論文  参考訳（メタデータ） (2024-01-02T18:53:13Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)

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

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