論文の概要: Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2503.09730v1
• Date: Wed, 12 Mar 2025 18:20:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-14 21:36:22.381979
• Title: Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
• Title（参考訳）: 自動定理証明のためのVerifier-in-the-Loopによる局所的ルックアヘッド誘導
• Authors: Sara Rajaee, Kumar Pratik, Gabriele Cesa, Arash Behboodi,
• Abstract要約: 自動定理証明タスクのための新しい検証器-イン・ザ・ループ設計を提案する。 実験により,ステップバイステップの局所的検証がモデルの推論精度と効率を大域的に向上させることを示す。
• 参考スコア（独自算出の注目度）: 17.289776394847063
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The most promising recent methods for AI reasoning require applying variants of reinforcement learning (RL) either on rolled out trajectories from the model, even for the step-wise rewards, or large quantities of human annotated trajectory data. The reliance on the rolled-out trajectory renders the compute cost and time prohibitively high. In particular, the correctness of a reasoning trajectory can typically only be judged at its completion, leading to sparse rewards in RL or requiring expensive synthetic data generation in expert iteration-like methods. In this work, we focus on the Automatic Theorem Proving (ATP) task and propose a novel verifier-in-the-loop design, which unlike existing approaches that leverage feedback on the entire reasoning trajectory, employs an automated verifier to give intermediate feedback at each step of the reasoning process. Using Lean as the verifier, we empirically show that the step-by-step local verification produces a global improvement in the model's reasoning accuracy and efficiency.
• Abstract（参考訳）: AI推論の最も有望な手法は、ステップワイドな報酬であっても、モデルから展開された軌道に強化学習(RL)の変種を適用するか、あるいは大量の人間の注釈付き軌道データを適用する必要がある。 ロールアウト軌道への依存は計算コストと時間を大幅に高める。 特に、推論軌跡の正しさは、通常、その完了時にのみ判断できるため、RLでの報酬は少なくなるか、専門家の反復的な手法で高価な合成データを生成する必要がある。 本研究は、ATP(Automatic Theorem Proving)タスクに焦点をあて、推論軌道全体のフィードバックを利用する既存のアプローチとは異なり、推論プロセスの各ステップで中間的なフィードバックを与える自動検証器を採用する。 検証としてリーンを用いることで、ステップバイステップのローカル検証がモデルの推論精度と効率を大幅に向上させることを示す。

関連論文リスト

• ProRAG: Process-Supervised Reinforcement Learning for Retrieval-Augmented Generation [54.071574153853994]
  ProRAGは、学習段階の監視をオンライン最適化ループに統合するために設計されたプロセス教師付き強化学習フレームワークである。 本フレームワークは,(1)構造化推論形式でモデルを初期化するための監視されたポリシーワームアップ,(2)中間推論品質を定量化するためのMCTSベースのプロセスリワードモデル(PRM)の構築,(3)細粒度プロセスの好みに合わせてポリシーを調整するためのPRM誘導推論リファインメント,(4)プロセススーパービジョン強化学習と2つのグラニュラリティー・アドバンテージ・メカニズムの4段階から構成される。
  論文  参考訳（メタデータ） (2026-01-29T16:04:59Z)
• InT: Self-Proposed Interventions Enable Credit Assignment in LLM Reasoning [32.274434679047395]
  アウトカム・リワード強化学習(RL)は,大規模言語モデル(LLM)の推論能力向上に有効であることが証明された。 標準RLは最終回答のレベルにのみクレジットを割り当て、結果が正しくない場合にすべての推論トレースを罰する。 Invention Training (InT) は、モデルが独自の推論トレースに基づいてきめ細かいクレジット割り当てを行う訓練パラダイムである。
  論文  参考訳（メタデータ） (2026-01-20T18:15:38Z)
• Formal that "Floats" High: Formal Verification of Floating Point Arithmetic [0.0]
  本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。 この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。 その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
  論文  参考訳（メタデータ） (2025-12-07T14:03:44Z)
• Arbitrage: Efficient Reasoning via Advantage-Aware Speculation [71.45710345765528]
  投機的復号化は、高速だが不正確なドラフトモデルを用いて推論を加速し、自動回帰的にトークンを提案する。 しかし、意味論的に等価なステップにおけるトークンミスマッチによる不要な拒絶のため、従来のトークンレベルの投機的デコーディングは、タスクの推論に苦労する。 提案するArbitrageは,ドラフトモデルとターゲットモデルとの相対的優位性に基づいて動的に生成をルーティングする,新しいステップレベルの投機生成フレームワークである。
  論文  参考訳（メタデータ） (2025-12-04T17:50:53Z)
• LaSeR: Reinforcement Learning with Last-Token Self-Rewarding [54.72617309922891]
  RLVR(Reinforcement Learning with Verifiable Rewards)は、Large Language Models(LLM)の推論能力を高めるためのコアパラダイムとして登場した。 従来、LLMは2つの異なるプロンプトテンプレートを使用してソリューションと自己検証をシーケンシャルに生成し、効率を大幅に低下させる必要があった。 本稿では,従来のRLVR損失をMSE損失で増大させるアルゴリズムであるLaSeR(Reinforcement Learning with Last-Token Self-Rewarding)を提案する。
  論文  参考訳（メタデータ） (2025-10-16T17:55:11Z)
• Audited Reasoning Refinement: Fine-Tuning Language Models via LLM-Guided Step-Wise Evaluation and Correction [1.41282143488996]
  人間の直接監督や高品質なラベルが不足している場合、タスク固有の小さな推論モデルのトレーニングは困難である。 本稿では,Reason-Refine-then-Align (R2tA)を提案する。
  論文  参考訳（メタデータ） (2025-09-15T21:47:52Z)
• SSPO: Self-traced Step-wise Preference Optimization for Process Supervision and Reasoning Compression [15.87106741558898]
  後学習法は補助的なモデルや過度な考えのためにかなりの計算オーバーヘッドを発生させる。 本稿では,プラグインRLgableプロセス監視フレームワークであるSSPO(Self-traced Step-wise Preference Optimization)を提案する。 SSPOは、モデル自身が生成したステップワイズ優先信号を使用して、圧縮を推論するための最適化プロセスを導出する。
  論文  参考訳（メタデータ） (2025-08-18T04:02:15Z)
• CAPO: Towards Enhancing LLM Reasoning through Verifiable Generative Credit Assignment [39.965170904699974]
  RLVR(Reinforcement Learning with Verifiable Rewards)は、ルールベースのバイナリフィードバックを使用することで、LLM(Large Language Models)の推論能力を改善した。 現在のRLVRメソッドは、すべてのレスポンスを単一のアクションとして扱い、トークンに同じ報酬を割り当てる。 この粗い粒度のフィードバックは、正確なクレジット割り当てを妨げ、モデルがどの推論ステップが成功または失敗につながるかを特定するのが難しくなる。
  論文  参考訳（メタデータ） (2025-08-04T11:06:08Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  大規模言語モデル(LLM)は、最近、検証可能な報酬付き強化学習(RLVR)を通じて推論能力の顕著な進歩を示した。 本稿では,情報ボトルネック(IB)の原理に基づくLLM推論の理論的特徴について述べる。 IB対応推論最適化(IBRO)を提案する。
  論文  参考訳（メタデータ） (2025-07-24T13:14:25Z)
• AALC: Large Language Model Efficient Reasoning via Adaptive Accuracy-Length Control [18.273777938294327]
  大きな推論モデル(LRM)は、長いチェーン・オブ・シークレットを生成することで印象的な推論能力を達成する。 我々は、強化学習に組み込まれた軽量で精度の高い長さの報酬であるALCを紹介する。 提案手法は,元の精度を維持したり改善したりしながら,応答長を50%以上削減することを示す。
  論文  参考訳（メタデータ） (2025-06-25T06:29:18Z)
• Reinforcing General Reasoning without Verifiers [47.72684162518086]
  本稿では,応答検証を回避し,RLを用いて参照応答を生成する確率を直接最大化する検証自由手法(VeriFree)を提案する。 VeriFreeは、MMLU-Pro、GPQA、SuperGPQA、数学関連のベンチマークにまたがる広範囲な評価において、検証者ベースの手法に匹敵する。
  論文  参考訳（メタデータ） (2025-05-27T17:56:27Z)
• The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
  大規模言語モデルの推論効率を向上させるために,Unsupervised Prefix Fine-Tuning (UPFT)を導入した。 UPFTはラベル付きデータや徹底的なサンプリングの必要性を取り除く。 実験の結果,UPFTは教師付き手法の性能と一致していることがわかった。
  論文  参考訳（メタデータ） (2025-03-04T18:56:03Z)
• Optimizing Diffusion Models for Joint Trajectory Prediction and Controllable Generation [49.49868273653921]
  拡散モデルは、自律運転における共同軌道予測と制御可能な生成を約束する。 最適ガウス拡散(OGD)と推定クリーンマニフォールド(ECM)誘導を導入する。 提案手法は生成過程の合理化を図り,計算オーバーヘッドを低減した実用的な応用を実現する。
  論文  参考訳（メタデータ） (2024-08-01T17:59:59Z)
• Adaptive $Q$-Network: On-the-fly Target Selection for Deep Reinforcement Learning [18.579378919155864]
  我々は、追加のサンプルを必要としない最適化手順の非定常性を考慮するために、Adaptive $Q$Network (AdaQN)を提案する。 AdaQNは理論上は健全で、MuJoCo制御問題やAtari 2600のゲームで実証的に検証されている。
  論文  参考訳（メタデータ） (2024-05-25T11:57:43Z)
• REBEL: Reward Regularization-Based Approach for Robotic Reinforcement Learning from Human Feedback [61.54791065013767]
  報酬関数と人間の嗜好の相違は、現実世界で破滅的な結果をもたらす可能性がある。 近年の手法は、人間の嗜好から報酬関数を学習することで、不適応を緩和することを目的としている。 本稿では,ロボットRLHFフレームワークにおける報酬正規化の新たな概念を提案する。
  論文  参考訳（メタデータ） (2023-12-22T04:56:37Z)
• Let's reward step by step: Step-Level reward model as the Navigators for Reasoning [64.27898739929734]
  Process-Supervised Reward Model (PRM)は、トレーニングフェーズ中にステップバイステップのフィードバックをLLMに提供する。 LLMの探索経路を最適化するために,PRMからのステップレベルのフィードバックを応用した欲求探索アルゴリズムを提案する。 提案手法の汎用性を探るため,コーディングタスクのステップレベル報酬データセットを自動生成する手法を開発し,コード生成タスクにおける同様の性能向上を観察する。
  論文  参考訳（メタデータ） (2023-10-16T05:21:50Z)
• Provable Reward-Agnostic Preference-Based Reinforcement Learning [61.39541986848391]
  PbRL(Preference-based Reinforcement Learning)は、RLエージェントが、軌道上のペアワイドな嗜好に基づくフィードバックを用いてタスクを最適化することを学ぶパラダイムである。 本稿では,隠れた報酬関数の正確な学習を可能にする探索軌道を求める理論的報酬非依存PbRLフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-05-29T15:00:09Z)
• End-to-End Meta-Bayesian Optimisation with Transformer Neural Processes [52.818579746354665]
  本稿では,ニューラルネットワークを一般化し,トランスフォーマーアーキテクチャを用いて獲得関数を学習する,エンド・ツー・エンドの差別化可能な最初のメタBOフレームワークを提案する。 我々は、この強化学習(RL)によるエンドツーエンドのフレームワークを、ラベル付き取得データの欠如に対処できるようにします。
  論文  参考訳（メタデータ） (2023-05-25T10:58:46Z)
• Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
  我々は,Large Language Model (LLM) の推論プロセスのガイドと校正を行うための段階的自己評価機構を導入する。 本稿では,ビームサーチによる自己評価ガイダンスを統合した復号アルゴリズムを提案する。 我々のアプローチは、GSM8K、AQuA、StrategyQAにおいて、対応するCodexバックボンドベースラインをわずかに精度6.34%、9.56%、および5.46%で上回る。
  論文  参考訳（メタデータ） (2023-05-01T02:37:59Z)
• Efficient Learning of Accurate Surrogates for Simulations of Complex Systems [0.0]
  サンプリング駆動サンプリングによって強化されたオンライン学習手法を提案する。 モデル応答面上のすべての旋回点がトレーニングデータに含まれることを保証する。 本手法を核物質のシミュレーションに適用し,高精度なサロゲートを確実に自動生成できることを実証する。
  論文  参考訳（メタデータ） (2022-07-11T20:51:11Z)
• Leveraging Unlabeled Data to Predict Out-of-Distribution Performance [63.740181251997306]
  実世界の機械学習デプロイメントは、ソース(トレーニング)とターゲット(テスト)ディストリビューションのミスマッチによって特徴づけられる。 本研究では,ラベル付きソースデータとラベルなしターゲットデータのみを用いて,対象領域の精度を予測する手法を検討する。 本稿では,モデルの信頼度をしきい値として学習し,精度をラベルなし例のごく一部として予測する実践的手法である平均閾値保持信頼度(ATC)を提案する。
  論文  参考訳（メタデータ） (2022-01-11T23:01:12Z)
• Ordering-Based Causal Discovery with Reinforcement Learning [31.358145789333825]
  本論文では, RL を順序付けに基づくパラダイムに組み込むことにより, RL に基づく因果的発見手法を提案する。 提案手法の一貫性と計算複雑性を分析し,事前学習モデルを用いて学習を高速化できることを実証的に示す。
  論文  参考訳（メタデータ） (2021-05-14T03:49:59Z)
• Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
  事前学習されたトランスモデルの微調整は、一般的なNLPタスクを解決するための標準的なアプローチとなっている。 そこで本研究では,可視性ランキングタスクをフルテキスト形式でキャストする新たなスコアリング手法を提案する。 提案手法は, ランダム再起動にまたがって, より安定した学習段階を提供することを示す。
  論文  参考訳（メタデータ） (2020-04-29T10:54:40Z)

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

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