論文の概要: 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（参考訳）: コンプレックスへのコンパイル:コンパイラ出力による形式的定理証明の強化
• Authors: Guchan Li, Rui Tian, Hongning Wang,
• 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パラメータモデルを用いて,次世代検証者誘導推論のためのスケーラブルなパラダイムを提供する。

関連論文リスト

• 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)

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

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