論文の概要: Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

• arxiv url: http://arxiv.org/abs/2507.02726v1
• Date: Thu, 03 Jul 2025 15:41:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-04 15:37:16.568065
• Title: Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
• Title（参考訳）: Bourbaki:理論実証のための自己生成型および目標設定型MDP
• Authors: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, Haitham Bou Ammar,
• Abstract要約: 自己生成目標条件付きMDP(sG-MDP)を導入する。 次に,モンテカルロ木探索(MCTS)のようなアルゴリズムを用いて問題を解く。 パットナムベンチでは、Bourbaki (7B) が26の問題を解く。
• 参考スコア（独自算出の注目度）: 11.39477477478338
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.
• Abstract（参考訳）: 推論は大きな言語モデル(LLM)にとって難しい課題であり、特に論理的に制約された自動定理証明(ATP)の環境において、粗末な報酬と大規模な証明のためである。 これらの課題は、複雑で多段階の推論を必要とする大学レベルの問題を含むPutnamBenchのようなベンチマークで増幅されている。 そこで我々は, 自己生成目標条件付きMDP(sG-MDPs)を導入し, エージェントが進化する証明状態に基づいて, サブゴールを生成・追跡する新たなフレームワークを提案する。 このより構造化されたゴールの生成を考えると、結果の問題はより探索しやすくなります。 次に,モンテカルロ木探索 (MCTS) のようなアルゴリズムを用いてsG-MDPを解く。Bourbaki (7B) は,サブゴール生成と戦術合成のために,複数の7B LLMをアンサンブルできるモジュールシステムである。 パットナムベンチでは、Bourbaki (7B) が26の問題を解く。

関連論文リスト

• Discriminative Policy Optimization for Token-Level Reward Models [55.98642069903191]
  プロセス報酬モデル(PRM)は、結果報酬モデル(ORM)と比較して、よりきめ細かい監督を提供する。 Q-RMは、微粒なアノテーションに頼ることなく、優先データからトークンレベルのQ関数を明示的に学習する。 Q-RMによる強化学習は、トレーニング効率を大幅に向上させ、GSM8KでのORMの12倍、MATHでのステップレベルPRMの11倍の収束を実現した。
  論文  参考訳（メタデータ） (2025-05-29T11:40:34Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。 思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。 SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
  論文  参考訳（メタデータ） (2025-04-13T13:35:41Z)
• 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)
• A Notion of Complexity for Theory of Mind via Discrete World Models [2.487142846438629]
  ToM(Theory of Mind)は、社会的推論が必要な複雑なシナリオにおいて、LLM(Large Language Models)の機能を評価するために用いられる。 本研究では,ToMタスクの複雑さを測定するための認知負荷理論に着想を得たフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-06-16T16:46:55Z)
• Faithful Question Answering with Monte-Carlo Planning [78.02429369951363]
  本稿では,FAME(Fithful Questioning with Monte-carlo planning)を提案する。 我々は,タスクを離散的な意思決定問題として定式化し,推論環境とコントローラの相互作用によって解決する。 FAMEは標準ベンチマークで最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2023-05-04T05:21:36Z)
• Deep Generalized Schr\"odinger Bridge [26.540105544872958]
  平均フィールドゲーム(Mean-Field Game)は、個々のエージェントの集合的振る舞いをモデル化する重要な数学的枠組みとして機能する。 エントロピー規則化された最適輸送モデルとして、Schr"odinger Bridgeは平均場構造を受け入れるために一般化可能であることを示す。 我々の手法はDeep Generalized Schr"odinger Bridge (DeepGSB) と呼ばれ、古典的な集団ナビゲーションMFGの解法よりも優れている。
  論文  参考訳（メタデータ） (2022-09-20T17:47:15Z)
• Lookback for Learning to Branch [77.32867454769936]
  Bipartite Graph Neural Networks (GNN) は、ディープラーニングに基づくMixed-Integer Linear Program (MILP) の重要コンポーネントであることが示されている。 近年の研究では、分岐とバウンド(B&B)の解法における分岐(可変選択)を置き換える上で、そのようなGNNの有効性が実証されている。
  論文  参考訳（メタデータ） (2022-06-30T02:33:32Z)

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

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