論文の概要: BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

• arxiv url: http://arxiv.org/abs/2502.03438v2
• Date: Mon, 24 Feb 2025 10:56:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-25 15:48:04.893981
• Title: BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
• Title（参考訳）: BFS-Prover: LLMに基づく自動定理証明のためのスケーラブルなベストファーストツリー探索
• Authors: Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, Kai Shen,
• Abstract要約: スケーラブルなエキスパートフレームワークであるBFS-Proverを紹介します。 BFS-Proverは、MiniF2Fテストセットで72.95%の最先端スコアを達成している。
• 参考スコア（独自算出の注目度）: 19.55767322738915
• License:
• Abstract: Recent advancements in large language models (LLMs) have spurred growing interest in automatic theorem proving using Lean4, where effective tree search methods are crucial for navigating the underlying large proof search spaces. While the existing approaches primarily rely on value functions and/or Monte Carlo Tree Search (MCTS), the potential of simpler methods like Best-First Tree Search (BFS) remains underexplored. In this paper, we investigate whether BFS can achieve competitive performance in large-scale theorem proving tasks. We present BFS-Prover, a scalable expert iteration framework, featuring three key innovations. First, we implement strategic data filtering at each expert iteration round, excluding problems solvable via beam search node expansion to focus on harder cases. Second, we improve the sample efficiency of BFS through Direct Preference Optimization (DPO) applied to state-tactic pairs automatically annotated with compiler error feedback, refining the LLM's policy to prioritize productive expansions. Third, we employ length normalization in BFS to encourage exploration of deeper proof paths. BFS-Prover achieves a state-of-the-art score of $72.95\%$ on the MiniF2F test set and therefore challenges the perceived necessity of complex tree search methods, demonstrating that BFS can achieve competitive performance when properly scaled. To facilitate further research and development in this area, we have open-sourced our model at https://huggingface.co/bytedance-research/BFS-Prover.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩はLean4を用いた自動定理証明への関心の高まりに拍車をかけた。 既存のアプローチは主に値関数と/またはモンテカルロ木探索(MCTS)に依存しているが、Best-First Tree Search(BFS)のような単純な手法の可能性はまだ検討されていない。 本稿では,BFSが大規模定理証明タスクにおいて競争性能を達成できるかどうかを検討する。 スケーラブルなエキスパートイテレーションフレームワークであるBFS-Proverを紹介します。 まず,ビーム探索ノード拡張によって解決可能な問題を除いて,各専門家の反復ラウンドで戦略的データフィルタリングを実装した。 第2に,コンパイラエラーフィードバックを付加した状態-戦術ペアに適用したDPO(Direct Preference Optimization)により,BFSのサンプル効率を向上し,生産的拡張を優先するLLMのポリシーを改良する。 第3に、より深い証明経路の探索を促進するために、BFSにおける長さ正規化を用いる。 BFS-Proverは、MiniF2Fテストセットで72.95 %の最先端スコアを達成し、複雑な木探索法の必要性を克服し、BFSが適切にスケールした場合に競争性能を達成できることを実証した。 この領域のさらなる研究と開発を容易にするため、私たちはhttps://huggingface.co/bytedance-research/BFS-Prover.comでモデルをオープンソース化しました。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。 このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
  論文  参考訳（メタデータ） (2024-10-03T18:12:29Z)
• IDEAL: Leveraging Infinite and Dynamic Characterizations of Large Language Models for Query-focused Summarization [59.06663981902496]
  クエリ中心の要約(QFS)は、特定の関心事に答え、より優れたユーザ制御とパーソナライゼーションを可能にする要約を作成することを目的としている。 本稿では,LLMを用いたQFSモデル,Longthy Document Summarization,およびクエリ-LLMアライメントの2つの重要な特徴について検討する。 これらのイノベーションは、QFS技術分野における幅広い応用とアクセシビリティの道を開いた。
  論文  参考訳（メタデータ） (2024-07-15T07:14:56Z)
• Uncertainty-Guided Optimization on Large Language Model Search Trees [42.71167208999792]
  大規模言語モデル(LLM)の復号過程における最大可能性列の探索においては,greedy や beam search などの木探索アルゴリズムが標準となっている。 LLMの遷移確率に関する事前の信念を定義し、各反復において最も有望な経路についての後続の信念を得る。 モンテカルロ木探索のような高価なシミュレーションに基づく非光学的手法とは異なり、我々の手法は信念からのサンプルのみを必要とする。
  論文  参考訳（メタデータ） (2024-07-04T14:08:50Z)
• AQA-Bench: An Interactive Benchmark for Evaluating LLMs' Sequential Reasoning Ability [29.1826948551409]
  AQA-Benchは、大規模言語モデルの逐次推論能力を評価するための新しいベンチマークである。 AQA-Benchは,2進探索,深さ優先探索,幅優先探索という3つのアルゴリズムで構築されている。 我々の調査では興味深い発見がいくつか示されている。
  論文  参考訳（メタデータ） (2024-02-14T18:59:33Z)
• Autonomous Tree-search Ability of Large Language Models [58.68735916408101]
  大規模言語モデルは、高度なプロンプト技術で顕著な推論能力に優れています。 近年の研究では、LLMがより困難な推論タスクを解くために受動的木探索を行えるように、検索ロジックを定義するために外部プログラムを活用することが提案されている。 我々は,LLMの自律木探索能力という新しい概念を提案し,正しい解を求める探索軌跡を含む応答を自動生成する。
  論文  参考訳（メタデータ） (2023-10-14T14:14:38Z)
• UNSAT Solver Synthesis via Monte Carlo Forest Search [10.754275929551593]
  木MDPにおける学習ポリシーのための強化学習(RL)アルゴリズムであるモンテカルロ森林探索(MCFS)を紹介する。 そのような問題の例としては、SAT公式の不満足性の証明、SAT公式の解の数を数えることがある。 我々は,満足度(SAT)問題を解決するためにDPLL分岐ポリシーを学習するMCFSアルゴリズムであるKnuth Synthesisをダブした。
  論文  参考訳（メタデータ） (2022-11-22T20:52:50Z)
• Efficient Non-Parametric Optimizer Search for Diverse Tasks [93.64739408827604]
  興味のあるタスクを直接検索できる,スケーラブルで汎用的なフレームワークを初めて提示する。 基礎となる数学表現の自然木構造に着想を得て、空間を超木に再配置する。 我々は,モンテカルロ法を木探索に適用し,レジェクションサンプリングと等価形状検出を備える。
  論文  参考訳（メタデータ） (2022-09-27T17:51:31Z)
• Reinforcement Learning for Branch-and-Bound Optimisation using Retrospective Trajectories [72.15369769265398]
  機械学習は分岐のための有望なパラダイムとして登場した。 分岐のための単純かつ効果的なRLアプローチであるレトロ分岐を提案する。 我々は現在最先端のRL分岐アルゴリズムを3～5倍に上回り、500の制約と1000の変数を持つMILP上での最高のILメソッドの性能の20%以内である。
  論文  参考訳（メタデータ） (2022-05-28T06:08:07Z)

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

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