論文の概要: Don't Eliminate Cut: Exponential Separations in LLM-Based Theorem Proving

• arxiv url: http://arxiv.org/abs/2602.10512v1
• Date: Wed, 11 Feb 2026 04:24:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-12 21:44:01.46261
• Title: Don't Eliminate Cut: Exponential Separations in LLM-Based Theorem Proving
• Title（参考訳）: カットを排除しない: LLMに基づく定理証明における指数分離
• Authors: Sho Sonoda, Shunta Akiyama, Yuya Uezato,
• Abstract要約: 対話型証明アシスタント(リーンなど)で証明されるLLM誘導形式定理の理論解析を開発する。 現代の表現学習を捉えるために、状態空間と作用空間を一般コンパクトな計量空間として扱い、リプシッツのポリシーを仮定する。 我々の主分離結果は、切断除去が深さ$D$のDAGをサイズ$(D)$のカットフリーツリーに拡張する一方、カットアウェア階層プロセスはサイズ$O(D)$ with $ll$を持つ場合、フラットラーナは、カットアウェア階層学習者よりも指数関数的に多くのデータを必要とすることを示す。
• 参考スコア（独自算出の注目度）: 8.948475969696075
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We develop a theoretical analysis of LLM-guided formal theorem proving in interactive proof assistants (e.g., Lean) by modeling tactic proposal as a stochastic policy in a finite-horizon deterministic MDP. To capture modern representation learning, we treat the state and action spaces as general compact metric spaces and assume Lipschitz policies. To explain the gap between worst-case hardness and empirical success, we introduce problem distributions generated by a reference policy $q$, including a latent-variable model in which proofs exhibit reusable cut/lemma/sketch structure represented by a proof DAG. Under a top-$k$ search protocol and Tsybakov-type margin conditions, we derive lower bounds on finite-horizon success probability that decompose into search and learning terms, with learning controlled by sequential Rademacher/covering complexity. Our main separation result shows that when cut elimination expands a DAG of depth $D$ into a cut-free tree of size $Ω(Λ^D)$ while the cut-aware hierarchical process has size $O(λ^D)$ with $λ\llΛ$, a flat (cut-free) learner provably requires exponentially more data than a cut-aware hierarchical learner. This provides a principled justification for subgoal decomposition in recent agentic theorem provers.
• Abstract（参考訳）: 我々は,有限水平決定性MDPにおける確率的ポリシとして戦術的提案をモデル化することにより,対話型証明アシスタント(例えばリーン)で証明されるLLM誘導形式定理の理論解析を開発する。 現代の表現学習を捉えるために、状態空間と作用空間を一般コンパクトな計量空間として扱い、リプシッツのポリシーを仮定する。 最悪の場合の硬さと経験的成功のギャップを説明するために、証明DAGで表される再利用可能なカット/レムマ/スケッチ構造を示す潜在変数モデルを含む、参照ポリシー$q$で生成された問題分布を導入する。 上位$kの検索プロトコルとツィバコフ型マージン条件の下では、連続ラデマチャー/探索複雑性によって制御される学習により、探索と学習の用語に分解される有限水平成功確率の低い境界を導出する。 我々の主分離結果は,カット・エミッションが深さ$D$のDAGを,カット・アウェアの階層的プロセスのサイズが$O(λ^D)$であるのに対して,カット・アウェアの階層的学習者よりも、フラット(カット・フリー)な学習者が指数関数的に多くのデータを必要とすることを示す。 このことは、最近のエージェント定理の証明器における部分分解の原理的な正当化を与える。

関連論文リスト

• Near-Optimal Sample Complexity Bounds for Constrained Average-Reward MDPs [6.237808815887583]
  制約付き平均回帰MDPにおける$epsilon$-optimal Policyを生成モデルで学習する際のサンプル複雑性について検討した。 本結果は,制約付き平均回帰MDPの複雑性の理解における理論的ギャップを埋めるものである。
  論文  参考訳（メタデータ） (2025-09-20T09:19:42Z)
• Reinforcement Learning in MDPs with Information-Ordered Policies [7.881781003954483]
  無限水平平均コストマルコフ決定過程に対するエポック型強化学習アルゴリズムを提案する。 我々は,このアルゴリズムが,部分順序の幅を$w$とする$O(sqrtw log(|Theta|) T)$の残差を達成していることを示す。 本稿では、在庫管理やキューシステムなど、オペレーション研究におけるこれらの部分的な注文の適用性について説明する。
  論文  参考訳（メタデータ） (2025-08-05T20:43:23Z)
• Projection by Convolution: Optimal Sample Complexity for Reinforcement Learning in Continuous-Space MDPs [56.237917407785545]
  本稿では,円滑なベルマン作用素を持つ連続空間マルコフ決定過程(MDP)の一般クラスにおいて,$varepsilon$-optimal Policyを学習する問題を考察する。 我々のソリューションの鍵となるのは、調和解析のアイデアに基づく新しい射影技術である。 我々の結果は、連続空間 MDP における2つの人気と矛盾する視点のギャップを埋めるものである。
  論文  参考訳（メタデータ） (2024-05-10T09:58:47Z)
• Demonstration-Regularized RL [39.96273388393764]
  専門的な実証から,次数$widetildeO(mathrmPoly(S,A,H)/(varepsilon2 NmathrmE)$および$widetildeO(mathrmPoly(d,H)/(varepsilon2 NmathrmE)$の線形マルコフ決定過程における最適ポリシを同定した。 実演規則化手法が人間のフィードバックからの強化学習に有効であることを示す。
  論文  参考訳（メタデータ） (2023-10-26T10:54:47Z)
• Horizon-Free and Variance-Dependent Reinforcement Learning for Latent Markov Decision Processes [62.90204655228324]
  我々は,後期マルコフ決定過程(LMDP)における強化学習(RL)の文脈を考慮した後悔の最小化について検討した。 我々は,モデル最適化と値最適化の両手法でインスタンス化できる,新しいモデルベースアルゴリズムフレームワークを設計する。
  論文  参考訳（メタデータ） (2022-10-20T21:32:01Z)
• Settling the Sample Complexity of Model-Based Offline Reinforcement Learning [50.5790774201146]
  オフライン強化学習(RL)は、事前収集されたデータを用いて、さらなる探索を行わずに学習する。 事前のアルゴリズムや分析は、最適なサンプルの複雑さに悩まされるか、サンプルの最適性に到達するために高いバーンインコストがかかるかのいずれかである。 モデルベース(あるいは"プラグイン")アプローチは,バーンインコストを伴わずに,最小限のサンプル複雑性を実現することを実証する。
  論文  参考訳（メタデータ） (2022-04-11T17:26:19Z)
• Kernel-Based Reinforcement Learning: A Finite-Time Analysis [53.47210316424326]
  モデルに基づく楽観的アルゴリズムであるKernel-UCBVIを導入する。 スパース報酬を伴う連続MDPにおける我々のアプローチを実証的に検証する。
  論文  参考訳（メタデータ） (2020-04-12T12:23:46Z)
• Upper Confidence Primal-Dual Reinforcement Learning for CMDP with Adversarial Loss [145.54544979467872]
  マルコフ決定過程(CMDP)に対するオンライン学習の検討 本稿では,遷移モデルから標本化した軌跡のみを必要とする,新しいEmphupper confidence primal-dualアルゴリズムを提案する。 我々の分析では、ラグランジュ乗算過程の新たな高確率ドリフト解析を、高信頼強化学習の記念後悔解析に組み入れている。
  論文  参考訳（メタデータ） (2020-03-02T05:02:23Z)

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

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