論文の概要: ProofCompass: Enhancing Specialized Provers with LLM Guidance

• arxiv url: http://arxiv.org/abs/2507.14335v1
• Date: Fri, 18 Jul 2025 19:28:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-22 20:51:31.84561
• Title: ProofCompass: Enhancing Specialized Provers with LLM Guidance
• Title（参考訳）: ProofCompass: LLMガイダンスによる特化プロバーの強化
• Authors: Nicolas Wischermann, Claudio Mayrink Verdun, Gabriel Poesia, Francesco Noseda,
• Abstract要約: 本稿では,計算効率を向上する新しいハイブリッド手法であるProofを紹介する。 DeepSeek-Prover-v1.5-RL (DSP-v1.5) のような既存の特殊な証明手法をLLM (Large Language Model) で戦略的にガイドする。 miniF2F ベンチマークでは、Proof は DSP-v1.5 (54.9% rightarrow 55.3%$) を上回っ、25 個の試行 (3200 rightarrow 128$) を使用する。
• 参考スコア（独自算出の注目度）: 6.757964026033364
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Language models have become increasingly powerful tools for formal mathematical reasoning. However, most existing approaches rely exclusively on either large general-purpose models or smaller specialized models, each with distinct limitations, while training specialized large models still requires significant computational resources. This paper introduces ProofCompass, a novel hybrid methodology that achieves remarkable computational efficiency by strategically guiding existing specialized prover methods, such as DeepSeek-Prover-v1.5-RL (DSP-v1.5) with a Large Language Model (LLM) without requiring additional model training. The LLM provides natural language proof strategies and analyzes failed attempts to select intermediate lemmas, enabling effective problem decomposition. On the miniF2F benchmark, ProofCompass demonstrates substantial resource efficiency: it outperforms DSP-v1.5 ($54.9\% \rightarrow 55.3\%$) while using 25x fewer attempts ($3200 \rightarrow 128$). Our synergistic approach paves the way for simultaneously improving computational efficiency and accuracy in formal theorem proving.
• Abstract（参考訳）: 言語モデルは、形式的な数学的推論のための強力なツールになりつつある。 しかし、既存のほとんどのアプローチは、大きな汎用モデルまたはより小さな専門モデルにのみ依存しており、それぞれに異なる制限がある。 本稿では,DeepSeek-Prover-v1.5-RL (DSP-v1.5) やLarge Language Model (LLM) など,既存の特殊証明手法をモデルトレーニングを必要とせずに戦略的に導くことによって,計算効率を向上する新しいハイブリッド手法であるProofCompassを紹介する。 LLMは自然言語の証明戦略を提供し、中間補題の選択に失敗した試行を分析し、効果的な問題分解を可能にする。 miniF2F ベンチマークでは、ProofCompass は DSP-v1.5 (54.9\% \rightarrow 55.3\%$) を上回り、25倍の試行(3200 \rightarrow 128$)を使用する。 我々の相乗的アプローチは、形式的定理証明における計算効率と精度を同時に改善する方法を舗装する。

関連論文リスト

• SPaRFT: Self-Paced Reinforcement Fine-Tuning for Large Language Models [51.74498855100541]
  大規模言語モデル(LLM)は、強化学習(RL)による微調整時に強い推論能力を示す。 トレーニング対象のモデルの性能に基づいて,効率的な学習を可能にする自己評価学習フレームワークである textbfSPaRFT を提案する。
  論文  参考訳（メタデータ） (2025-08-07T03:50:48Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• LLaDA 1.5: Variance-Reduced Preference Optimization for Large Language Diffusion Models [76.8317443926908]
  Masked Diffusion Models (MDM) は言語モデリングにおいて有望なパラダイムである。 この課題は、優先最適化に必要なエビデンス・ロウアー・バウンド(ELBO)に基づく推定値の高分散から生じる。 本稿では,ELBO推定器の偏差を公式に解析し,優先最適化勾配の偏差と偏差を導出するフレームワークであるVRPOを提案する。
  論文  参考訳（メタデータ） (2025-05-25T16:36:20Z)
• Can 1B LLM Surpass 405B LLM? Rethinking Compute-Optimal Test-Time Scaling [69.57918638435491]
  テスト時間スケーリングは、大規模言語モデルの性能を向上させる重要な方法である。 異なるポリシーモデル、PRM、問題の難易度にまたがってテスト時間計算をスケールするための最適なアプローチは何か? 計算-最適TS戦略により、非常に小さなポリシーモデルがより大きなモデルより優れていることを示す。
  論文  参考訳（メタデータ） (2025-02-10T17:30:23Z)
• Do NOT Think That Much for 2+3=? On the Overthinking of o1-Like LLMs [76.43407125275202]
  o1のようなモデルは、推論中に人間のような長時間の思考をエミュレートすることができる。 本論文は,これらのモデルにおける過度な考察の課題に関する,最初の包括的研究である。 精度を損なうことなく、過剰思考を緩和し、推論プロセスを合理化するための戦略を提案する。
  論文  参考訳（メタデータ） (2024-12-30T18:55:12Z)
• A Convex-optimization-based Layer-wise Post-training Pruner for Large Language Models [24.185245582500876]
  本稿では,凸最適化モデルとアルゴリズムに基づく最初のポストトレーニングプルーナであるFISTAPrunerを紹介する。 FISTAPrunerは層内累積誤差補正機構を搭載し、並列プルーニングをサポートする。 OPT, LLaMA, LLaMA-2, LLaMA-3 などのモデルにおける FISTAPruner の評価を行った。
  論文  参考訳（メタデータ） (2024-08-07T12:33:46Z)
• Inference Scaling Laws: An Empirical Analysis of Compute-Optimal Inference for Problem-Solving with Language Models [46.959380978972206]
  我々は、推論スケーリング法則(いわゆるテスト時間スケーリング法則)と計算最適推論について研究する。 計算最適推論手法の理解と設計に向けた第一歩として,推論戦略のコストパフォーマンストレードオフについて検討した。 この結果から,モデルパラメータのスケーリングよりも,推論戦略による推論計算のスケーリングの方が効率的であることが示唆された。
  論文  参考訳（メタデータ） (2024-08-01T17:16:04Z)
• Pruning Large Language Models with Semi-Structural Adaptive Sparse Training [17.381160429641316]
  Adaptive Sparse Trainer (AST)は、半構造化スパースモデルに適した、新規で効率的なリトレーニングフレームワークである。 ASTは、密度と2:4の半構造化スパースモデルのパープレキシティとゼロショット精度のギャップをそれぞれ0.6と1.16%に削減する。
  論文  参考訳（メタデータ） (2024-07-30T06:33:44Z)
• Towards Efficient Pareto Set Approximation via Mixture of Experts Based Model Fusion [53.33473557562837]
  大規模深層ニューラルネットワークに対する多目的最適化問題を解くことは、損失ランドスケープの複雑さと高価な計算コストのために難しい課題である。 本稿では,専門家(MoE)をベースとしたモデル融合を用いて,この問題を実用的でスケーラブルに解決する手法を提案する。 特殊な単一タスクモデルの重みをまとめることで、MoEモジュールは複数の目的間のトレードオフを効果的に捉えることができる。
  論文  参考訳（メタデータ） (2024-06-14T07:16:18Z)
• When Parameter-efficient Tuning Meets General-purpose Vision-language Models [65.19127815275307]
  PETALは、一意のモード近似技術によって達成される全パラメータの0.5%しか必要とせず、トレーニングプロセスに革命をもたらす。 実験の結果,PETALは現状の手法をほとんどのシナリオで上回るだけでなく,完全な微調整モデルよりも優れていることがわかった。
  論文  参考訳（メタデータ） (2023-12-16T17:13:08Z)

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

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