論文の概要: Structured Hints for Sample-Efficient Lean Theorem Proving

• arxiv url: http://arxiv.org/abs/2601.16172v1
• Date: Thu, 22 Jan 2026 18:16:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-23 21:37:20.689013
• Title: Structured Hints for Sample-Efficient Lean Theorem Proving
• Title（参考訳）: サンプル効率のよいリーン理論証明のための構造化ヒント
• Authors: Zachary Burton,
• Abstract要約: 私たちは、miniF2Fベンチマークで、軽量な介入 -- 15の一般的な戦術スケルトンに対する固定されたプロンプトスケジュール -- を評価します。 この単純なアプローチは21.7%のpass@16を、同じモデルからの標準サンプリングの15.2%と比較する。 以上の結果から,RL訓練プロバーでさえ,戦術言語で利用可能な構造的先行性を弱めていることが示唆された。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: State-of-the-art neural theorem provers like DeepSeek-Prover-V1.5 combine large language models with reinforcement learning, achieving impressive results through sophisticated training. We ask: do these highly-trained models still benefit from simple structural guidance at inference time? We evaluate a lightweight intervention -- a fixed prompt schedule over 15 common tactic skeletons -- on the miniF2F benchmark. This simple approach yields 21.7% pass@16 compared to 15.2% for standard sampling from the same model, a 43% relative improvement using the same number of samples (k=16) and same maximum generation length (1024 tokens). Our results suggest that even capable RL-trained provers underutilize structural priors available in the tactic language, and that simple inference-time guidance remains a cheap, complementary boost.
• Abstract（参考訳）: DeepSeek-Prover-V1.5のような最先端のニューラル定理の証明者は、大規模な言語モデルと強化学習を組み合わせることで、高度なトレーニングを通じて印象的な結果を達成する。 これらの高度に訓練されたモデルは、推論時に単純な構造的ガイダンスの恩恵を受けていますか? 私たちは、miniF2Fベンチマークで、軽量な介入 -- 15の一般的な戦術スケルトンに対する固定されたプロンプトスケジュール -- を評価します。 この単純なアプローチでは、同じモデルからの標準サンプリングの15.2%に対して21.7%のpass@16が得られ、同じサンプル数(k=16)と同じ最大生成長(1024トークン)を使用した相対的な改善が43%である。 以上の結果から,RL訓練プロバーでも戦術言語で利用できる構造的先行性は弱く,単純な推論時ガイダンスが安価で補足的な効果を保っていることが示唆された。

関連論文リスト

• Teaching Language Models to Reason with Tools [73.21700643314917]
  emphHint-Engineeringは、推論経路内の最適点に様々なヒントを戦略的に注入する新しいデータ合成戦略である。 CoRTは効率を大幅に向上させ、32Bモデルのトークン使用量を約30%削減し、1.5Bモデルのトークン使用量を50%削減した。
  論文  参考訳（メタデータ） (2025-10-23T08:41:44Z)
• MobileLLM-R1: Exploring the Limits of Sub-Billion Language Model Reasoners with Open Training Recipes [60.57770396565211]
  強い推論能力は、はるかに少ないデータで実現可能であることを示す。 MobileLLM-R50MのAIMEスコアは15.5であり、OLMo-2-1.48Bは0.6、SmolLM-2-1.7Bは0.3である。
  論文  参考訳（メタデータ） (2025-09-29T15:43:59Z)
• ProofCompass: Enhancing Specialized Provers with LLM Guidance [6.757964026033364]
  本稿では,計算効率を向上する新しいハイブリッド手法である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$) を使用する。
  論文  参考訳（メタデータ） (2025-07-18T19:28:01Z)
• Logit Arithmetic Elicits Long Reasoning Capabilities Without Training [14.015546463427732]
  大きな推論モデル(LRM)は、バックトラックや自己補正といった認知戦略を含む長いチェーン・オブ・シント(CoT)を介して複雑な推論を行うことができる。 最近の研究は、いくつかのモデルは本質的にこれらの長い推論能力を持ち、余分な訓練によって解錠される可能性があることを示唆している。 本稿では,より小さなモデルをガイドとして,目標とする大規模LMを長時間の推論のために調整するための復号時間アプローチであるThinkLogitを提案する。
  論文  参考訳（メタデータ） (2025-07-17T03:31:36Z)
• SARI: Structured Audio Reasoning via Curriculum-Guided Reinforcement Learning [21.36638095182274]
  強化学習は、大きな言語モデル(LLM)の推論能力を「答える前に考える」よう促すことによって、強化することができる。 明示的で構造化された推論とカリキュラム学習は、音声言語理解を大幅に強化することを示す。
  論文  参考訳（メタデータ） (2025-04-22T13:41:26Z)
• T1: Advancing Language Model Reasoning through Reinforcement Learning and Inference Scaling [52.34735382627312]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な能力を示した。 既存のアプローチは主に、効果的なテストタイムスケーリングを達成するために、模倣学習と苦労に依存しています。 我々は、探索を奨励し、推論スケーリングを理解することで、強化学習をスケールするためにT1を提案する。
  論文  参考訳（メタデータ） (2025-01-20T18:33:33Z)
• Pre-trained Model Guided Fine-Tuning for Zero-Shot Adversarial Robustness [52.9493817508055]
  我々は,モデルがゼロショットの逆方向のロバスト性を高めるために,事前訓練されたモデル誘導逆方向の微調整(PMG-AFT)を提案する。 私たちのアプローチは、平均8.72%のクリーンな精度を継続的に改善します。
  論文  参考訳（メタデータ） (2024-01-09T04:33:03Z)
• ProBoost: a Boosting Method for Probabilistic Classifiers [55.970609838687864]
  ProBoostは確率的分類器のための新しいブースティングアルゴリズムである。 各トレーニングサンプルの不確実性を使用して、最も困難で不確実なものを決定する。 これは、最も不確実性が高いと判明したサンプルに徐々に焦点をあてる配列を生成する。
  論文  参考訳（メタデータ） (2022-09-04T12:49:20Z)

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

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