論文の概要: EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2509.12603v1
• Date: Tue, 16 Sep 2025 03:00:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-17 17:50:52.851689
• Title: EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
• Title（参考訳）: EconProver: 自動定理証明のための経済的なテストタイムスケーリングを目指す
• Authors: Mukai Li, Linfeng Song, Zhenwen Liang, Jiahao Xu, Shansan Gong, Qi Liu, Haitao Mi, Dong Yu,
• Abstract要約: 大規模言語モデル(LLM)は、最近、自動定理証明(ATP)の分野を進歩させた。 ATPモデルに対する異なるテスト時間スケーリング戦略は、推論にかなりの計算オーバーヘッドをもたらすことを示す。 本稿では,統一EconRLパイプラインに統合可能な2つの補完手法を提案する。
• 参考スコア（独自算出の注目度）: 64.15371139980802
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) have recently advanced the field of Automated Theorem Proving (ATP), attaining substantial performance gains through widely adopted test-time scaling strategies, notably reflective Chain-of-Thought (CoT) reasoning and increased sampling passes. However, they both introduce significant computational overhead for inference. Moreover, existing cost analyses typically regulate only the number of sampling passes, while neglecting the substantial disparities in sampling costs introduced by different scaling strategies. In this paper, we systematically compare the efficiency of different test-time scaling strategies for ATP models and demonstrate the inefficiency of the current state-of-the-art (SOTA) open-source approaches. We then investigate approaches to significantly reduce token usage and sample passes while maintaining the original performance. Specifically, we propose two complementary methods that can be integrated into a unified EconRL pipeline for amplified benefits: (1) a dynamic Chain-of-Thought (CoT) switching mechanism designed to mitigate unnecessary token consumption, and (2) Diverse parallel-scaled reinforcement learning (RL) with trainable prefixes to enhance pass rates under constrained sampling passes. Experiments on miniF2F and ProofNet demonstrate that our EconProver achieves comparable performance to baseline methods with only 12% of the computational cost. This work provides actionable insights for deploying lightweight ATP models without sacrificing performance.
• Abstract（参考訳）: 大規模言語モデル (LLM) は、最近、ATP (Automated Theorem Proving) の分野を進歩させ、広く採用されているテスト時間スケーリング戦略、特に反射的チェーン・オブ・ソート (CoT) 推論とサンプリングパスの増加により、大幅なパフォーマンス向上を実現した。 しかし、どちらも推論にかなりの計算オーバーヘッドを導入している。 さらに、既存のコスト分析はサンプリングパスの数だけを規制するが、異なるスケーリング戦略によって導入されたサンプリングコストの相違は無視する。 本稿では、ATPモデルの異なるテストタイムスケーリング戦略の効率を体系的に比較し、現在のSOTA(State-of-the-art)オープンソースアプローチの非効率性を実証する。 次に、元の性能を維持しながらトークン使用率とサンプルパスを大幅に削減するアプローチについて検討する。 具体的には,(1)不必要なトークン消費を軽減するために設計された動的チェーン・オブ・ソート(CoT)切替機構,(2)トレーニング可能なプレフィックス付き並列スケール強化学習(RL)により,制約付きサンプリングパスのパスレートを向上する2つの補完的手法を提案する。 miniF2FとProofNetの実験では、EconProverは計算コストのわずか12%でベースライン手法に匹敵する性能を実現している。 この作業は、パフォーマンスを犠牲にすることなく、軽量ATPモデルをデプロイするための実用的な洞察を提供する。

関連論文リスト

• Quantum-Inspired DRL Approach with LSTM and OU Noise for Cut Order Planning Optimization [0.0]
  裁量計画(COP)は繊維産業において重要な課題であり、繊維の利用と製造コストに直接影響を及ぼす。 本稿では,Long Short-Term Memory NetworkとOrnstein-Uhlenbeckノイズを統合した量子インスパイアされたDeep Reinforcement Learningフレームワークを提案する。 比較分析の結果,提案手法は従来手法と比較して最大13%のコスト削減を実現していることがわかった。
  論文  参考訳（メタデータ） (2025-08-13T05:00:50Z)
• DynScaling: Efficient Verifier-free Inference Scaling via Dynamic and Integrated Sampling [20.605487145370752]
  推論時間スケーリングは、テスト時間計算の増大を通じて、大きな言語モデル(LLM)の性能向上に有効であることが証明されている。 しかし、実際的な応用は、外部検証への依存や、現実的な計算制約に対する最適化の欠如によってしばしば妨げられる。 我々はDynScalingを提案し、これらの制限を2つの主要なイノベーション、すなわち並列シーケンスサンプリング戦略と帯域幅に基づく動的予算配分フレームワークを通じて解決する。
  論文  参考訳（メタデータ） (2025-06-19T05:40:54Z)
• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [58.05959902776133]
  私たちはSingle-Passを紹介します。 Reference-Guided Evaluation (SPARE)は、効率的なステップごとのアノテーションを可能にする新しい構造化フレームワークである。 数学的推論(GSM8K, MATH)、マルチホップ質問応答(MuSiQue-Ans)、空間推論(SpaRP)にまたがる4つの多様なデータセットにおけるSPAREの有効性を実証する。 ProcessBenchでは、SPAREがデータ効率のよいアウト・オブ・ディストリビューションの一般化を実証し、トレーニングサンプルの$sim$16%しか使用していない。
  論文  参考訳（メタデータ） (2025-06-18T14:37:59Z)
• S$^4$C: Speculative Sampling with Syntactic and Semantic Coherence for Efficient Inference of Large Language Models [38.784951111677856]
  大規模言語モデル(LLM)は、様々な下流タスクにまたがる顕著な推論能力を示す。 その自己回帰的な性質は、相当なレイテンシ推論をもたらし、リアルタイムアプリケーションに課題を提起する。 マルチヘッドドラフトを利用して投機的サンプリングを拡張するSyntactic and Semantic Coherenceフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-06-17T03:38:19Z)
• Fractured Chain-of-Thought Reasoning [61.647243580650446]
  完全CoTと解のみのサンプリングを補間する統合推論時間戦略であるフラクチャードサンプリングを導入する。 フラクチャードサンプリングは、Pass@kとトークンの予算に対して、急激なログ線形スケーリングゲインをもたらすため、優れた精度とコストのトレードオフを一貫して達成できることを示す。
  論文  参考訳（メタデータ） (2025-05-19T11:30:41Z)
• SEVA: Leveraging Single-Step Ensemble of Vicinal Augmentations for Test-Time Adaptation [29.441669360316418]
  テスト時間適応(TTA)は、推論中の迅速なモデル適応を通じて、分散シフトに対するモデルロバスト性を高めることを目的としている。 拡張戦略は、信頼性のあるサンプルの可能性を効果的に解き放つことができるが、急速に増大する計算コストは、彼らのリアルタイムアプリケーションを妨げる。 本稿では, 計算負担を増大させることなく, データの増大を生かして, 新たなTTAアプローチであるSingle-step Ensemble of Vicinal Augmentations(SEVA)を提案する。
  論文  参考訳（メタデータ） (2025-05-07T02:58:37Z)
• FTP: A Fine-grained Token-wise Pruner for Large Language Models via Token Routing [17.01412432658081]
  大規模言語モデル(LLM)は、法則を拡張することによって、様々なタスクにおいて優れた性能を示す。 重要でないトークンを適応的に識別する学習可能なルータを提案する。 提案手法は,既存の刈り込み手法を超越して,最先端(SOTA)刈り込み結果を実現する。
  論文  参考訳（メタデータ） (2024-12-16T07:09:46Z)
• Bridging SFT and DPO for Diffusion Model Alignment with Self-Sampling Preference Optimization [67.8738082040299]
  自己サンプリング優先最適化(SSPO)は,訓練後強化学習のための新しいアライメント手法である。 SSPOは、SFTのトレーニング安定性を維持しながら、ペアデータと報酬モデルの必要性を排除する。 SSPOは、テキスト・ツー・イメージベンチマークにおける以前のアプローチを全て上回り、テキスト・ツー・ビデオベンチマークにおける優れたパフォーマンスを示している。
  論文  参考訳（メタデータ） (2024-10-07T17:56:53Z)
• PYRA: Parallel Yielding Re-Activation for Training-Inference Efficient Task Adaptation [61.57833648734164]
  本稿では, PYRA(Parallel Yielding Re-Activation)法を提案する。 PYRAは低圧縮率と高圧縮率の両方で競合する全ての手法より優れている。
  論文  参考訳（メタデータ） (2024-03-14T09:06:49Z)

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

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