論文の概要: Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
- arxiv url: http://arxiv.org/abs/2604.18587v1
- Date: Fri, 13 Mar 2026 01:33:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-04 02:32:14.029269
- Title: Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
- Title（参考訳）: コンプレックスへのコンパイル:コンパイラ出力による形式的定理証明の強化
- Abstract要約: 大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
- 参考スコア（独自算出の注目度）: 48.390500145598544
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute via massive roll-outs or extended context windows. In this work, we address this scalability bottleneck by exploiting an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts to a compact set of structured failure modes. We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration. We perform tree search that corrects errors locally conditioned on explicit verifier feedback, thereby circumventing the costs associated with accumulating a long history of proof attempts. Extensive evaluations show that our method consistently amplifies the reasoning capabilities of base provers across varying scales. Notably, our approach achieves state-of-the-art performance on PutnamBench among publicly reported $\sim$8B and $\sim$32B parameter models under comparable test-time budgets, offering a scalable paradigm for next-generation verifier-guided reasoning.
- Abstract（参考訳）: 大規模言語モデル (LLMs) は形式的定理の証明において有意義な可能性を証明しているが、最先端のパフォーマンスでは大規模なロールアウトや拡張コンテキストウインドウによる禁止的なテスト時間計算を必要とすることが多い。
本研究では,このスケーラビリティのボトルネックを,形式的検証において情報的構造を利用することによって解決する: コンパイラが多種多様な証明の試みを,構造化された障害モードのコンパクトなセットにマップする観察。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
我々は,明示的な検証者フィードバックに基づいて局所的に条件付けられた誤りを補正する木探索を行い,証明の試みの長い歴史を蓄積するコストを回避する。
広範囲な評価の結果,提案手法は様々なスケールでのベース・プローサの推論能力を一貫して増幅することがわかった。
特に,PutnamBenchでは,テスト時間予算に匹敵する$\sim$8Bおよび$\sim$32Bパラメータモデルを用いて,次世代検証者誘導推論のためのスケーラブルなパラダイムを提供する。
関連論文リスト
- Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization [20.22828310618122]
ToMapは、Decomposer-Formalizer-Proverパイプラインとして自動形式化の証明を構築するフレームワークである。
ToMapは,構文的正当性と意味的忠実性の両方で評価すると,最善前の手法よりも19.0%向上することを示す。
論文 参考訳（メタデータ） (2026-07-13T09:21:15Z) - PLUME: Latent Reasoning Based Universal Multimodal Embedding [52.35354073629127]
ユニバーサルマルチモーダル埋め込み(UME)は、異種入力を単一のモデルで共有検索空間にマッピングする。
最近のアプローチでは、埋め込みを抽出する前に明確なチェーン・オブ・シント(CoT)論理を生成することにより、UMEを改善している。
PLUMEは,言語化されたCoTを連続的潜伏状態の短時間の自己回帰ロールアウトに置き換えることで,UMEを進化させる潜在的推論フレームワークである。
論文 参考訳（メタデータ） (2026-04-02T14:04:53Z) - Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
エージェント定理プロバーは、数学的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証とを結合したパイプラインである。
本稿では, 検証された証明に到達する有限水平成功確率として定義される分布的視点を提案し, 証明可能性を導入する。
本稿では,エージェント定理の証明者が実世界の偏りのある問題分布にいつ,なぜ成功するのかを,原理的かつコンポーネントに敏感に説明する。
論文 参考訳（メタデータ） (2026-02-11T05:22:24Z) - Advancing Mathematical Research via Human-AI Interactive Theorem Proving [16.40852561664514]
LLMを用いた対話型定理証明と発見のためのヒューマン・イン・ザ・ループ・ワークフローを提案する。
人間の専門家は問題定式化と許容可能な仮定の制御を維持し、モデルは証明や矛盾を探索する。
このワークフローを、多様体最適化とグロバーの量子探索アルゴリズムの接続に関するケーススタディでインスタンス化する。
論文 参考訳（メタデータ） (2025-12-10T09:16:27Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。
本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。
我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
論文 参考訳（メタデータ） (2025-10-01T16:06:40Z) - Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。
最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。
本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文 参考訳（メタデータ） (2025-09-02T14:16:02Z) - 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) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Compact Proofs of Model Performance via Mechanistic Interpretability [1.4197963050877802]
本稿では,モデル性能に関する形式的保証を導出し,コンパクトに証明するために,機械的解釈可能性を用いることを提案する。
提案手法は, 最大K$タスクで訓練した151個の小型変圧器の精度について, 下限を正式に証明して試作する。
論文 参考訳（メタデータ） (2024-06-17T17:34:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。