論文の概要: 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 15:55:19.166846
• 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:
• 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)タスクに焦点をあて、推論軌道全体のフィードバックを利用する既存のアプローチとは異なり、推論プロセスの各ステップで中間的なフィードバックを与える自動検証器を採用する。 検証としてリーンを用いることで、ステップバイステップのローカル検証がモデルの推論精度と効率を大幅に向上させることを示す。

関連論文リスト

• Towards General-Purpose Model-Free Reinforcement Learning [40.973429772093155]
  強化学習(RL)は、ほぼ普遍的な問題解決のためのフレームワークを約束する。 実際には、RLアルゴリズムは特定のベンチマークに合わせて調整されることが多い。 そこで本研究では,ドメインと問題設定の多様なクラスに対処可能なモデルフリーの深部RLアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2025-01-27T15:36:37Z)
• 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)
• 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)

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

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