論文の概要: Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

• arxiv url: http://arxiv.org/abs/2509.06493v2
• Date: Thu, 09 Oct 2025 17:45:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-10 17:54:14.593633
• Title: Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
• Title（参考訳）: LLMステッププローバのマルチターンオフポリシィRLとマルチエージェントツリー探索のスケールアップ
• Authors: Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, Xia Xiao,
• Abstract要約: 本稿では,2つのスケーリング問題に対処するシステムである textttBFS-Prover-V2 を紹介する。 1つ目は、トレーニング時にLLMのステッププロデューサの性能を継続的に改善する、新しいマルチターンオフポリチフレームワークである。 第二のイノベーションは、推論時に推論能力を拡大するプランナーによるマルチエージェント検索アーキテクチャである。
• 参考スコア（独自算出の注目度）: 16.135928990655422
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The integration of Large Language Models (LLMs) into automated theorem proving has shown immense promise, yet is fundamentally constrained by challenges in scaling up both training-time reinforcement learning (RL) and inference-time compute. This paper introduces \texttt{BFS-Prover-V2}, a system designed to address this dual scaling problem. We present two primary innovations. The first is a novel multi-turn off-policy RL framework for continually improving the performance of LLM step-prover at training time. This framework, inspired by the principles of AlphaZero, utilizes a multi-stage expert iteration pipeline featuring adaptive tactic-level data filtering and periodic retraining to surmount the performance plateaus that typically curtail long-term RL in LLM-based agents. The second innovation is a planner-enhanced multi-agent search architecture that scales reasoning capabilities at inference time. This architecture employs a general reasoning model as a high-level planner to iteratively decompose complex theorems into a sequence of simpler subgoals. This hierarchical approach substantially reduces the search space, enabling a team of parallel prover agents to collaborate efficiently by leveraging a shared proof cache. We demonstrate that this dual approach to scaling yields state-of-the-art results on established formal mathematics benchmarks. \texttt{BFS-Prover-V2} achieves 95.08\% and 41.4\% on the MiniF2F and ProofNet test sets respectively. While demonstrated in the domain of formal mathematics, the RL and inference techniques presented in this work are of broader interest and may be applied to other domains requiring long-horizon multi-turn reasoning and complex search.
• Abstract（参考訳）: LLM(Large Language Models)を自動定理証明に統合することは、非常に有望であるが、トレーニング時強化学習(RL)と推論時計算の両方をスケールアップする際の課題により、根本的な制約が課されている。 本稿では、この二重スケーリング問題に対処するために設計されたシステムである「texttt{BFS-Prover-V2}」を紹介する。 主なイノベーションは2つある。 1つ目は、トレーニング時にLLMのステッププロデューサの性能を継続的に改善する、新しいマルチターンオフポリチフレームワークである。 AlphaZeroの原理にインスパイアされたこのフレームワークは、適応的な戦術レベルのデータフィルタリングと周期的リトレーニングを備えた多段階のエキスパートイテレーションパイプラインを使用して、LLMベースのエージェントで通常、長期RLを縮小するパフォーマンスプレートを克服する。 第二のイノベーションは、推論時に推論能力を拡大するプランナーによるマルチエージェント検索アーキテクチャである。 このアーキテクチャは、複素定理をより単純な部分ゴールの列に反復的に分解するために、高レベルプランナーとして一般的な推論モデルを用いる。 この階層的なアプローチは検索スペースを大幅に削減し、並列証明エージェントのチームが共有証明キャッシュを利用することで効率よく協調することを可能にする。 このスケーリングに対する2つのアプローチは、確立された公式な数学ベンチマークにおける最先端の結果をもたらすことを実証する。 \texttt{BFS-Prover-V2} はそれぞれ MiniF2F と ProofNet のテストセットで 95.08\% と 41.4\% を達成する。 形式数学の分野において実証されているが、この研究で提示されたRLおよび推論技術はより広い関心を持ち、長い水平多重ターン推論と複素探索を必要とする他の領域に適用することができる。

関連論文リスト

• Answer First, Reason Later: Aligning Search Relevance via Mode-Balanced Reinforcement Learning [7.006180736433431]
  低レイテンシと高パフォーマンスを実現する検索関連モデルを構築することは、検索業界において長年の課題である。 我々は,新しいtextbfAnswer-First, Reason Later(AFRL)パラダイムを提案する。 このパラダイムでは、モデルが第1のトークンで決定的な関連性スコアを出力し、続いて構造化された論理的説明を行う必要がある。
  論文  参考訳（メタデータ） (2026-02-10T17:28:12Z)
• DiRL: An Efficient Post-Training Framework for Diffusion Language Models [54.405206032785706]
  Diffusion Language Models (dLLMs) はAuto-Regressive(AR)モデルに代わる有望な代替品として登場した。 既存の手法は、訓練と推論の間の計算の非効率性と客観的なミスマッチに悩まされている。 我々は,FlexAttention-accelerated blockwise trainingとLMDeploy-timized inferenceを密接に統合した,効率的なポストトレーニングフレームワークであるDiRLを紹介した。
  論文  参考訳（メタデータ） (2025-12-23T08:33:19Z)
• Eliciting Chain-of-Thought Reasoning for Time Series Analysis using Reinforcement Learning [2.426309874608745]
  複雑な数値時系列解析は、しばしば現在のモデルの範囲を超えて多段階の推論能力を必要とする。 我々は,大規模言語モデルを訓練して,多種多様な時系列タスクに対して,検証可能な報酬付き強化学習(RL)を用いた推論を行うための,最初のフレームワークであるCOUNTS(Chain Of thought for Understanding Numerical Time Series)を紹介した。 実験により、中間CoT推論を用いたこのRL駆動方式は、様々な時系列解析タスクにおけるLLM性能を大幅に向上させ、複雑な時間的データ推論の新たな可能性を開くことを実証した。
  論文  参考訳（メタデータ） (2025-10-01T17:02:28Z)
• Pangu Embedded: An Efficient Dual-system LLM Reasoner with Metacognition [95.54406667705999]
  Pangu Embeddedは、Ascend Neural Processing Units (NPU) 上で開発された効率的なLarge Language Model (LLM) 推論器である。 既存の推論最適化 LLM でよく見られる計算コストと推論遅延の問題に対処する。 単一の統一モデルアーキテクチャ内で、迅速な応答と最先端の推論品質を提供する。
  論文  参考訳（メタデータ） (2025-05-28T14:03:02Z)
• Reinforcing Multi-Turn Reasoning in LLM Agents via Turn-Level Reward Design [35.544075583073685]
  マルチターンRLアルゴリズムとエージェント応用のためのテキストターンレベルの報酬設計に関する最初の体系的研究について述べる。 我々は、多ターン推論強化検索エージェントのケーススタディを行い、検証可能とLCM-as-judgeの2種類のターンレベルの報酬を慎重に設計する。 マルチターン探索タスクの実験により、適切に設計されたターンレベルの報酬を組み込むことで、RLアルゴリズムは軌道レベルの報酬でベースライン法を大幅に上回ることを示す。
  論文  参考訳（メタデータ） (2025-05-17T04:09:46Z)
• R1-Searcher: Incentivizing the Search Capability in LLMs via Reinforcement Learning [87.30285670315334]
  textbfR1-Searcherは、大規模言語モデルの検索能力を高めるために設計された、2段階の結果に基づく新しいRLアプローチである。 本フレームワークは, コールドスタート時に, プロセス報酬や蒸留を必要とせず, RLのみに依存している。 提案手法は, クローズドソースGPT-4o-miniと比較して, 従来の強力なRAG法よりも有意に優れていた。
  論文  参考訳（メタデータ） (2025-03-07T17:14:44Z)
• Boost, Disentangle, and Customize: A Robust System2-to-System1 Pipeline for Code Generation [58.799397354312596]
  大規模言語モデル(LLM)は、様々な領域、特にシステム1タスクにおいて顕著な機能を示した。 System2-to-System1法に関する最近の研究が急増し、推論時間計算によるシステム2の推論知識が探索された。 本稿では,システム2タスクの代表的タスクであるコード生成に注目し,主な課題を2つ挙げる。
  論文  参考訳（メタデータ） (2025-02-18T03:20:50Z)
• Satori: Reinforcement Learning with Chain-of-Action-Thought Enhances LLM Reasoning via Autoregressive Search [57.28671084993782]
  大規模言語モデル(LLM)は、様々な領域にまたがる顕著な推論能力を示している。 近年の研究では、テスト時間計算の増加はLLMの推論能力を高めることが示されている。 そこで我々は,1)COAT推論形式を内部化するための小規模な形式調整段階,2)強化学習を活用した大規模自己改善段階を提案する。
  論文  参考訳（メタデータ） (2025-02-04T17:26:58Z)
• ArCHer: Training Language Model Agents via Hierarchical Multi-Turn RL [80.10358123795946]
  大規模言語モデルを微調整するためのマルチターンRLアルゴリズムを構築するためのフレームワークを開発する。 我々のフレームワークは階層的なRLアプローチを採用し、2つのRLアルゴリズムを並列に実行している。 実験により,ArCHerはエージェントタスクの効率と性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-02-29T18:45:56Z)

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

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