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

• arxiv url: http://arxiv.org/abs/2502.03438v1
• Date: Wed, 05 Feb 2025 18:33:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-06 14:27:31.619731
• 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要約: 本稿では,Best-First Searchが大規模定理証明タスクにおいて競争性能を達成できるかどうかを考察する。 textttBFS-Proverは,3つの重要なイノベーションを特徴とする,スケーラブルなエキスパートイテレーションフレームワークです。 textttBFS-ProverはMiniF2Fテストセットで71.31ドルのスコアを獲得し、複雑な木探索方法の必要性を認識している。
• 参考スコア（独自算出の注目度）: 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 proof search spaces. While the existing approaches primarily rely on value functions and Monte Carlo Tree Search (MCTS), the potential of simpler methods like Best-First Search (BFS) remains underexplored. This paper investigates whether BFS can achieve competitive performance in large-scale theorem proving tasks. We present \texttt{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. \texttt{BFS-Prover} achieves a score of $71.31$ 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.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩はLean4を用いた自動定理証明への関心の高まりに拍車をかけた。 既存のアプローチは主に値関数とMCTS(Monte Carlo Tree Search)に依存しているが、Best-First Search(BFS)のような単純な手法の可能性はまだ未定である。 本稿では,BFSが大規模定理証明タスクにおいて競争性能を達成できるかどうかを考察する。 スケーラブルなエキスパートイテレーションフレームワークである‘texttt{BFS-Prover}’を紹介する。 まず,ビーム探索ノード拡張によって解決可能な問題を除いて,各専門家の反復ラウンドで戦略的データフィルタリングを実装した。 第2に,コンパイラエラーフィードバックを付加した状態-戦術ペアに適用したDPO(Direct Preference Optimization)により,BFSのサンプル効率を向上し,生産的拡張を優先するLLMのポリシーを改良する。 第3に、より深い証明経路の探索を促進するために、BFSにおける長さ正規化を用いる。 texttt{BFS-Prover} は MiniF2F テストセットで 711.31$ のスコアを達成し、複雑な木探索法の必要性に挑戦し、BFS が適切にスケールした場合に競争性能を達成できることを実証した。

関連論文リスト

• 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)

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

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