論文の概要: VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools
- arxiv url: http://arxiv.org/abs/2606.20740v1
- Date: Wed, 17 Jun 2026 19:05:38 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-06-23 11:20:17.56275
- Title: VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools
- Title（参考訳）: VeriBound:形式検証ツールを用いたプロセスリワードモデルのPAC-Bayesian一般化境界
- Authors: Amirul Rahman, Mohammed Sabih Alsharari,
- Abstract要約: 本稿では,形式的検証ツールを用いて訓練されたPRMに対して,PAC-Bayesianの一般化境界を提供する理論的枠組みを提案する。
i) PAC-Bayesian generalization bound on formal-verification-annotated training data and the expected error on unseen reasoning tasks, with the bound on the formal accuracy accuracy and the divergence between training and test task distributions; (ii) a sample complexity results shows that $O(d log(d/) / 2)$ formal-verification-annotated examples suffice to achieve generalization error。
- 参考スコア（独自算出の注目度）: 0.0
- License:
- Abstract: Process Reward Models (PRMs) provide step-level verification for Large Language Model (LLM) reasoning, yet their training data acquisition remains a bottleneck: human annotation is costly and Monte Carlo roll-out estimates are noisy. A recent approach, FOVER, trains PRMs on step-level error labels automatically annotated by formal verification tools such as Z3 and Isabelle, and empirically observes cross-task generalization from symbolic tasks to diverse reasoning benchmarks. However, this generalization phenomenon lacks any theoretical explanation, and no formal bounds exist on the generalization error, sample complexity, convergence rate, or downstream Best-of-K performance of such PRMs. We propose VeriBound, a theoretical framework that provides PAC-Bayesian generalization bounds for PRMs trained with formal verification tools. We establish four main results: (i) a PAC-Bayesian generalization bound that relates the empirical verification error on formal-verification-annotated training data to the expected error on unseen reasoning tasks, with the bound depending on the formal verification accuracy and the divergence between training and test task distributions; (ii) a sample complexity result showing that $O(d \log(d/δ) / ε^2)$ formal-verification-annotated examples suffice to achieve generalization error $ε$ with probability $1-δ$, where $d$ is the complexity of the PRM hypothesis class; (iii) a convergence analysis proving that PRM training with formal verification labels converges at a linear rate under $L$-smoothness and bounded variance conditions; and (iv) an error propagation bound that relates step-level verification error to Best-of-K performance degradation.
- Abstract（参考訳）: Process Reward Models (PRM)は、Large Language Model (LLM)推論のためのステップレベルの検証を提供するが、トレーニングデータ取得はボトルネックのままである。
最近のアプローチであるFOVERは、Z3やIsabelleのような形式的な検証ツールによって自動的に注釈付けされたステップレベルのエラーラベルでPRMを訓練し、象徴的なタスクから多様な推論ベンチマークへのクロスタスクの一般化を実証的に観察している。
しかし、この一般化現象には理論的な説明はなく、一般化誤差、サンプルの複雑さ、収束率、下流のPRMの性能に公式な境界は存在しない。
本稿では,形式的検証ツールで訓練されたPRMに対して,PAC-Bayesianの一般化境界を提供する理論フレームワークであるVeriBoundを提案する。
主な成果は4つある。
一 形式的検証付訓練データの実証的検証誤差を、形式的検証精度及び試験課題分布のばらつきによつて、見知らぬ推論タスクの予測誤差に関連付けたPAC-ベイズ一般化
(ii)$O(d \log(d/δ) / ε^2)$ formal-verification-annotated examplesuffice to achieve generalization error $ε$ with probability $1-δ$, where $d$ is complexity of the PRM hypothesis class。
3 形式的検証ラベルを用いたPRMトレーニングが$L$-smoothness及び有界分散条件の下で線形レートで収束することを証明する収束解析
(4)ステップレベルの検証エラーとBest-of-Kパフォーマンス劣化を関連付けたエラー伝搬境界。
関連論文リスト
- The Paradox of Outcome Optimization: A Causal Information-Theoretic Bound on Reasoning Shortcuts in LLMs [5.802098323678549]
結果に基づく強化学習(RL)を通じて整列された大規模言語モデル(LLM)は、しばしば重大な障害モードを示す。
我々は,このパラドックスを説明するために,構造因果モデル(SCM)と情報ボトルネック(IB)の原理をブリッジする理論的枠組みを確立する。
論文 参考訳（メタデータ） (2026-05-30T11:06:13Z) - VerifyMAS: Hypothesis Verification for Failure Attribution in LLM Multi-Agent Systems [79.51005192758262]
大規模言語モデル駆動型マルチエージェントシステムは複雑なタスクで優れている。
しかし、信頼性の低いエージェントは、システムレベルの信頼性にとって重要なボトルネックである。
本稿では,エージェント故障の帰属に関する仮説検証フレームワークを提案する。
論文 参考訳（メタデータ） (2026-05-17T14:09:35Z) - Controllable and Verifiable Process Data Synthesis for Process Reward Models [0.0]
プロセス報酬モデル(PRM)のためのプロセス監視データを合成するための制御可能で検証可能なフレームワークを提案する。
筆者らのフレームワークはまず,まず正しいシンボリック推論チェーンを構築し,テンプレート認識エラーを中間ステップに注入し,その後のステップを劣化状態下で再計算し,インジェクトされたステップがそのプレフィックスから導出できないことを確認する。
実験により、合成されたデータは、論理的推論ベンチマークと数理的推論への変換に基づいて、最高の8倍の精度を向上することが示された。
論文 参考訳（メタデータ） (2026-05-04T09:36:57Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Information Fidelity in Tool-Using LLM Agents: A Martingale Analysis of the Model Context Protocol [69.11739400975445]
モデルコンテキストプロトコル(MCP)エージェントにおけるエラー蓄積を解析するための最初の理論的枠組みを紹介する。
累積歪みが線形成長と高確率偏差を$O(sqrtT)$で表すことを示す。
主な発見は、意味重み付けは歪みを80%減らし、周期的再接地は、エラー制御の約9ステップごとに十分である。
論文 参考訳（メタデータ） (2026-02-10T21:08:53Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - 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) - Reward Model Generalization for Compute-Aware Test-Time Reasoning [21.05692631562457]
外部テスト時推論は、生成と選択を分離することで、大きな言語モデル(LLM)を強化する。
この設定における中心的な課題は、テスト時間計算の最適性(TCO)、すなわち、固定された推論予算の下で答えの正確さを最大化する方法である。
PRMの一般化誤差が計算効率と推論性能に与える影響を解析する。
そこで本研究では,探索動作を動的に制御するアクター・クリティカルなフレームワークであるCompute-Aware Tree Search (CATS)を提案する。
論文 参考訳（メタデータ） (2025-05-23T16:12:12Z) - Generalizable Process Reward Models via Formally Verified Training Data [13.781401358802462]
FoVerは、正式な検証ツールによって自動的に注釈付けされた正確なステップレベルのエラーラベルでPRMトレーニングデータを合成するアプローチである。
実験により、FoVerでトレーニングされたPRMはクロスタスクの一般化を示し、単一のPRMが様々な推論タスクの検証を効果的に行えることを示した。
論文 参考訳（メタデータ） (2025-05-21T19:23:45Z) - Unveiling the Statistical Foundations of Chain-of-Thought Prompting Methods [59.779795063072655]
CoT(Chain-of-Thought)の促進とその変種は、多段階推論問題を解決する効果的な方法として人気を集めている。
統計的推定の観点からCoTのプロンプトを解析し,その複雑さを包括的に評価する。
論文 参考訳（メタデータ） (2024-08-25T04:07:18Z) - From Chaos to Clarity: Claim Normalization to Empower Fact-Checking [57.024192702939736]
Claim Normalization(別名 ClaimNorm)は、複雑でノイズの多いソーシャルメディア投稿を、より単純で分かりやすい形式に分解することを目的としている。
本稿では,チェーン・オブ・ソートとクレーム・チェック・バシネス推定を利用した先駆的アプローチであるCACNを提案する。
実験により, CACNは様々な評価尺度において, いくつかの基準値を上回る性能を示した。
論文 参考訳（メタデータ） (2023-10-22T16:07:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。