論文の概要: Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models

• arxiv url: http://arxiv.org/abs/2602.10538v1
• Date: Wed, 11 Feb 2026 05:22:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-12 21:44:01.483923
• Title: Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
• Title（参考訳）: エージェント理論が機能する理由:数学的推論モデルの統計的確率論
• Authors: Sho Sonoda, Shunta Akiyama, Yuya Uezato,
• Abstract要約: エージェント定理プロバーは、数学的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証とを結合したパイプラインである。 分布的視点を提案し、**統計的証明性*を導入し、証明された証明に到達する有限水平成功確率として定義する。 我々は,緩やかな規則性の下での最適政策の存在を証明し,サブ/スーパーソリューションの不等式による検証可能性証明を導出し,スコア誘導計画のパフォーマンスギャップを限定する。
• 参考スコア（独自算出の注目度）: 8.948475969696075
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Agentic theorem provers -- pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier -- have recently achieved striking empirical success, yet it remains unclear which components drive performance and why such systems work at all despite classical hardness of proof search. We propose a distributional viewpoint and introduce **statistical provability**, defined as the finite-horizon success probability of reaching a verified proof, averaged over an instance distribution, and formalize modern theorem-proving pipelines as time-bounded MDPs. Exploiting Bellman structure, we prove existence of optimal policies under mild regularity, derive provability certificates via sub-/super-solution inequalities, and bound the performance gap of score-guided planning (greedy/top-\(k\)/beam/rollouts) in terms of approximation error, sequential statistical complexity, representation geometry (metric entropy/doubling structure), and action-gap margin tails. Together, our theory provides a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions, while clarifying limitations in worst-case or adversarial regimes.
• Abstract（参考訳）: エージェント定理プロバー -- 論理的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証を組み合わせたパイプライン -- は、最近、顕著な実証的な成功を収めた。 本稿では, 検証された証明に到達する有限水平成功確率として定義される**統計的証明性**を導入し, 現代の定理証明パイプラインを時間有界なMDPとして定式化する。 ベルマン構造をエクスプロイトすることにより, 近似誤差, 逐次統計複雑性, 表現幾何学(メトリックエントロピー/ダブルブリング構造), アクションギャップ・テールといった点において, スコア誘導計画(greedy/top-\(k\)/beam/rollouts)のパフォーマンスギャップを埋める。 我々の理論は、最悪の場合や敵の体制における制限を明確にしつつ、いつ、なぜエージェント定理が実世界の問題分布に成功するのかを原則的かつコンポーネントに敏感な説明を提供する。

関連論文リスト

• Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
  学習後のカリキュラムは指数関数的複雑性のボトルネックを回避していることを示す。 結果のみの報酬信号の下では、強化学習の微調整は、サンプルの複雑さを高い精度で達成する。 カリキュラムを意識したクエリにより、報奨託書の呼び出しとサンプリングコストの両方を指数関数的に削減するテストタイムスケーリングの保証を確立する。
  論文  参考訳（メタデータ） (2025-11-10T18:29:54Z)
• Non-asymptotic error bounds for probability flow ODEs under weak log-concavity [6.661419982187023]
  この研究は、確率フローODEの一般クラスに対して、2-ワッサーシュタイン距離における非漸近収束境界を確立する。 この結果は収束理論を、より現実的なデータ分布と実用的なODEソルバに拡張する。
  論文  参考訳（メタデータ） (2025-10-20T14:54:38Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  チェーン・オブ・シント(CoT)推論は、大規模な言語モデルで複雑な問題を解釈可能な中間ステップに分解することを可能にする。 我々は,遅延状態遷移を伴うマルコフ決定プロセス(MDP)としてCoT推論を定式化するフレームワークであるgroundingSを紹介する。 我々は、ベンチマーク推論タスクにおける推論精度、多様性、探索効率の改善を示す。
  論文  参考訳（メタデータ） (2025-07-10T21:32:18Z)
• From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
  我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。 我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。 この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
  論文  参考訳（メタデータ） (2025-06-08T10:09:54Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Identifiable Latent Neural Causal Models [82.14087963690561]
  因果表現学習は、低レベルの観測データから潜伏した高レベルの因果表現を明らかにすることを目指している。 因果表現の識別可能性に寄与する分布シフトのタイプを決定する。 本稿では,本研究の成果を実用的なアルゴリズムに翻訳し,信頼性の高い潜在因果表現の取得を可能にする。
  論文  参考訳（メタデータ） (2024-03-23T04:13:55Z)
• Advancing Counterfactual Inference through Nonlinear Quantile Regression [77.28323341329461]
  ニューラルネットワークで実装された効率的かつ効果的な対実的推論のためのフレームワークを提案する。 提案手法は、推定された反事実結果から見つからないデータまでを一般化する能力を高める。 複数のデータセットで実施した実証実験の結果は、我々の理論的な主張に対する説得力のある支持を提供する。
  論文  参考訳（メタデータ） (2023-06-09T08:30:51Z)
• A Topological Perspective on Causal Inference [10.965065178451104]
  仮定のない因果推論は、構造因果モデルの単なる集合においてのみ可能であることを示す。 以上の結果から,有効な因果推論を行うのに十分な帰納的仮定は,原理上は統計的に検証できないことが示唆された。 我々のトポロジカルアプローチのさらなる利点は、無限に多くの変数を持つSCMに容易に対応できることである。
  論文  参考訳（メタデータ） (2021-07-18T23:09:03Z)

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

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