論文の概要: Direct Optimization of Generators for Search in Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2609.25575v1
• Date: Tue, 22 Sep 2026 02:07:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-23 18:04:04.176341
• Title: Direct Optimization of Generators for Search in Automated Theorem Proving
• Title（参考訳）: 自動定理証明における発電機の直接最適化
• Abstract要約: クロスエントロピーは、アグリゲーションやフィルタリングといったフラットな探索戦略で使用されるLLMに最適である。 我々は、ポリシー誘導検索の抽象化により、CAT(Compute-Aligned Training)をこの設定に拡張する。 近似誤差を解消する条件を含む探索対象の重み付けに,オフトレースの挙動がどう影響するかを特徴付ける。
• 参考スコア（独自算出の注目度）: 23.99156538891498
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM used in flat search strategies such as aggregation or filtering and that work has developed new loss functions to correct this misalignment. Extending this alignment to tree search is more challenging: proof discovery depends on exploration and recovery through off-trace states that supervised demonstrations do not reveal. We extend Compute-Aligned Training (CAT) to this setting through an abstraction of policy-guided search, deriving tractable, trace-supported losses. Alongside these search-aware losses, we introduce a search-agnostic uniform-allocation (UA) loss that accounts for the budget without specifying the specific search. Both induce scalar weights on per-tactic cross-entropy gradients. We characterize how off-trace behavior affects the search-aware weights, including conditions for vanishing approximation error at large budgets. On a Lean benchmark, both approaches achieve higher observed proof-success rates than cross-entropy across six search strategies, with strong results from a single shared UA adapter. Budget sweeps show larger gains over cross-entropy at 16 than at 256 expansions, implying CAT scales with test time compute.
• Abstract（参考訳）: 微調整された大言語モデル(LLM)は、ATP(Automated Theorem Proving)を著しく進歩させるが、単対数生成ではなく、木探索の指針としてしばしば展開される。 近年の研究では、アグリゲーションやフィルタリングなどの平坦な探索戦略に使用されるLLMに対して、クロスエントロピーが最適であることが示されており、この誤りを補正する新たな損失関数が開発されている。 証明発見は、教師付きデモンストレーションが明らかにしないオフトレース状態による探索と回復に依存します。 我々はCAT(Compute-Aligned Training)をポリシー誘導検索の抽象化によってこの設定に拡張し、トラクタブルでトレース支援された損失を導出する。 検索を意識した損失に加えて、特定の検索を指定せずに予算を考慮に入れた検索非依存の統一割当(UA)損失も導入する。 どちらも戦術的クロスエントロピー勾配のスカラーウェイトを誘導する。 大予算での近似誤差を解消する条件を含む,追跡外行動が検索対象の重みにどのように影響するかを特徴付ける。 Leanベンチマークでは、どちらの手法も、6つの検索戦略のクロスエントロピーよりも高い実証-成功率を達成する。 予算削減は、256の拡張よりも16エントロピーよりも大きな増加を示し、テスト時間計算によるCATスケールを示唆している。

関連論文リスト

• WIDE: Wildcard Inference with Dynamic Expansion for Cross-Modal Generative Retrieval [11.681276883454288]
  クロスモーダル検索における強制幻覚の問題を解決するために,動的拡張を用いたワイルドカード推論(WIDE)を提案する。 復号生成フェーズでは、非対称性を意識したワイルドカード復号(AWD)が意味的な盲点を検出し、強制決定的な識別子の代わりにワイルドカードを出力する。 BSR(Blind-Spot Re- rank)は、離散生成信頼度と連続的な意味的類似性を組み合わせたハイブリッドスコアリング機構を用いて、拡張候補プールを評価する。
  論文  参考訳（メタデータ） (2026-09-03T08:55:05Z)
• G-ReAct: Graph-Guided Deep Search via Structure-State Co-Evolution [16.818086150132853]
  $textbfG-ReActはディープ検索のための推論フレームワークである。 それは、固定トポロジークエリグラフ上の$textbfstateの進化として推論を整理する。 G-ReActはトレーニングと推論の両方をサポートしている。
  論文  参考訳（メタデータ） (2026-08-02T15:43:37Z)
• LLM-Aided A* Search in Non-Geometric Network Graphs [0.4078247440919473]
  本稿では,LLM が A* 拡張を有望なグラフ領域へ導く中間経路を生成できる大規模言語モデル (LLM) を用いた A* アルゴリズムを提案する。 最大2,000ノードのグラフトポロジに関する実験により,LLMは拡張ノード数を50%程度削減する一方,最適解に比べて限界パスコストの増加しか生じないことが示された。
  論文  参考訳（メタデータ） (2026-06-22T10:26:35Z)
• Learning to Guide Local Search for MPE Inference in Probabilistic Graphical Models [7.287294240824019]
  確率的グラフィカルモデル(PGM)におけるほとんどの確率的説明(MPE)推論は、根本的なが計算的に難しい問題である。 本稿では、繰り返しクエリー方式における局所探索を改善するためのニューラルネットワークのアモート化フレームワークを提案する。 理論的な直観リンクによる距離低減移動選択を行い, 隣り合う選択時の約束を改良する。
  論文  参考訳（メタデータ） (2026-02-01T22:43:28Z)
• LLM-First Search: Self-Guided Exploration of the Solution Space [29.780554400938335]
  大規模言語モデル(LLM)は、テスト時間計算の増加による推論と計画の大幅な改善を示している。 我々は,新しいTextitLLM Self-Guided Search法である textbfLLM-First Search (LFS) を提案する。
  論文  参考訳（メタデータ） (2025-06-05T16:27:49Z)
• ETS: Efficient Tree Search for Inference-Time Scaling [61.553681244572914]
  テストタイムの計算スケーリングにおいて有望なアプローチのひとつは、プロセス報酬モデルに対する検索である。 木探索過程における軌跡の多様性は、多様性の増大がさらなる探索を促進するため、探索の精度に影響を与える。 本稿では,冗長なトラジェクトリを抽出し,必要な多様なトラジェクトリを維持しながら,KVの共有を促進する効率的なツリー探索(ETS)を提案する。
  論文  参考訳（メタデータ） (2025-02-19T09:30:38Z)
• Don't Get Lost in the Trees: Streamlining LLM Reasoning by Overcoming Tree Search Exploration Pitfalls [83.89771461061903]
  検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 検証者による木探索アルゴリズムの最近の進歩は、大規模言語モデル(LLM)の推論能力を大幅に向上させた。 意味論的に等価なコンテンツを持つ冗長な状態による$textitover-Exploration$と、検証器のスコアリングにおける高いばらつきに起因する$textitunder-Exploration$である。 各種木探索アルゴリズムに適合するフレキシブルなプラグアンドプレイシステムであるFETCHを提案する。
  論文  参考訳（メタデータ） (2025-02-16T16:12:01Z)
• Loss Function Discovery for Object Detection via Convergence-Simulation Driven Search [101.73248560009124]
  本稿では,効率的な収束シミュレーションによる進化的探索アルゴリズムCSE-Autolossを提案する。 一般的な検出器上での損失関数探索の広範囲な評価を行い、探索された損失の優れた一般化能力を検証した。 実験の結果, 2段検出器と1段検出器のmAPでは, 最適損失関数の組み合わせが1.1%と0.8%を上回っていることがわかった。
  論文  参考訳（メタデータ） (2021-02-09T08:34:52Z)
• Meta-AAD: Active Anomaly Detection with Deep Reinforcement Learning [56.65934079419417]
  偽陽性率が高いことは、異常検出アルゴリズムの長年の課題である。 本稿では,クエリ選択のためのメタポリシーを学習する新しいフレームワーク,Meta-AAD(Active Anomaly Detection with Meta-Policy)を提案する。
  論文  参考訳（メタデータ） (2020-09-16T01:47:42Z)

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

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