論文の概要: The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

• arxiv url: http://arxiv.org/abs/2512.02080v1
• Date: Sun, 30 Nov 2025 22:19:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-03 21:04:45.55842
• Title: The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
• Title（参考訳）: 4/$δ$境界:形式的手法保証のための予測可能なLCM検証システムの設計
• Authors: PIerre Dantas, Lucas Cordeiro, Youcheng Sun, Waldir Junior,
• Abstract要約: この研究は LLM-Verifier Convergence Theorem の開発によってギャップを埋める。 LLMと検証器の相互作用を離散時間マルコフ連鎖としてモデル化する。 われわれはこの予測を90,000件以上の治験を含む広範囲な実証キャンペーンでストレステストした。
• 参考スコア（独自算出の注目度）: 5.345468714252351
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The idea of using Formal Verification tools with large language models (LLMs) has enabled scaling software verification beyond manual workflows. However, current methods remain unreliable. Without a solid theoretical footing, the refinement process can wander; sometimes it settles, sometimes it loops back, and sometimes it breaks away from any stable trajectory. This work bridges this critical gap by developing an LLM-Verifier Convergence Theorem, providing the first formal framework with provable guarantees for termination and convergence. We model the interaction between the LLM and the verifier as a discrete-time Markov Chain, with state transitions determined by a key parameter: the error-reduction probability ($δ$). The procedure reaching the Verified state almost surely demonstrates that the program terminates for any $δ> 0$, with an expected iteration count bounded by $\mathbb{E}[n] \leq 4/δ$. We then stress-tested this prediction in an extensive empirical campaign comprising more than 90,000 trials. The empirical results match the theory with striking consistency. Every single run reached verification, and the convergence factor clustered tightly around $C_f\approx$ 1.0. Consequently, the bound mirrors the system's actual behavior. The evidence is sufficiently robust to support dividing the workflow into three distinct operating zones: marginal, practical, and high-performance. Consequently, we establish the design thresholds with absolute confidence. Together, the theoretical guarantee and the experimental evidence provide a clearer architectural foundation for LLM-assisted verification. Heuristic tuning no longer has to be carried out by the system. Engineers gain a framework that supports predictable resource planning and performance budgeting, precisely what is needed before deploying these pipelines into safety-critical software environments.
• Abstract（参考訳）: 大きな言語モデル(LLM)でFormal Verificationツールを使用するというアイデアは、手作業によるワークフローを越えて、ソフトウェア検証のスケーリングを可能にした。 しかし、現在の手法は信頼できないままである。 しっかりとした理論的な足場がなければ、精製プロセスはさまよることができ、時には落ち着き、時にはループバックし、時には安定な軌道から外れる。 この研究は LLM-Verifier Convergence Theorem を開発し、終端と収束の証明可能な保証を備えた最初の形式的なフレームワークを提供することによって、この重要なギャップを埋める。 LLMと検証器間の相互作用を離散時間マルコフ連鎖としてモデル化し、鍵パラメータによって決定される状態遷移(エラー低減確率(δ$))をモデル化する。 検証された状態に達する手順は、プログラムが任意の$δ> 0$に対して終了することをほぼ確実に示し、期待される反復数は$\mathbb{E}[n] \leq 4/δ$で制限される。 そして、90,000回以上の臨床試験を含む広範な実証キャンペーンで、この予測をストレステストした。 経験的な結果は、その理論と顕著な一貫性に一致する。 すべての実行が検証に到達し、収束係数は$C_f\approx$1.0前後で密集した。 その結果、境界はシステムの実際の振舞いを反映する。 この証拠はワークフローを3つの異なる運用ゾーン(限界、実用、ハイパフォーマンス)に分割するのを支援するのに十分堅牢である。 その結果,絶対的な信頼性で設計しきい値を確立することができた。 理論的な保証と実験的な証拠が組み合わさって、LCM支援検証のためのより明確なアーキテクチャ基盤を提供する。 ヒューリスティックチューニングはもはやシステムによって行われなくてもよい。 エンジニアは、これらのパイプラインを安全クリティカルなソフトウェア環境にデプロイする前に、正確に何が必要か、予測可能なリソース計画とパフォーマンス予算をサポートするフレームワークを手に入れる。

関連論文リスト

• Uncertainty-Guided Expert-AI Collaboration for Efficient Soil Horizon Annotation [0.13999481573773068]
  土壌プロファイルを記述するためのマルチモーダルマルチタスクモデルである$textitSoilNet$に共形予測を適用する。 我々は,モデルの不確実性が高い場合に,基本真理アノテーションを得るための限られた予算が利用できる,シミュレーションされたHILアノテーションパイプラインを設計する。 実験により、SoilNetの適合性は回帰タスクにおけるより効率的なアノテーションと分類タスクにおける同等のパフォーマンススコアをもたらすことが示された。
  論文  参考訳（メタデータ） (2025-09-29T14:54:23Z)
• A Fano-Style Accuracy Upper Bound for LLM Single-Pass Reasoning in Multi-Hop QA [65.38186593873313]
  MHQA(Multi-Hop Question Answering)は、ノイズ下でのシーケンシャルな推論を通じて、分散した相互依存的な証拠を統合する必要がある。 我々はMHQAのための概念実証マルチコールフレームワークをInfoQAで紹介する。 我々は、理論とフレームワークを検証するために、厳密で騒音に富んだベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-09-25T14:11:57Z)
• Tractable Asymmetric Verification for Large Language Models via Deterministic Replicability [0.6117371161379209]
  大規模言語モデル(LLM)の展望は、動的でマルチエージェントなシステムへと急速にシフトします。 本稿では, トラクタブルな非対称な作業を実現するための検証フレームワークを提案する。 対象検定は全再生の12倍以上の速さで行うことができる。
  論文  参考訳（メタデータ） (2025-09-14T03:30:06Z)
• LLMs are Bayesian, in Expectation, not in Realization [0.0]
  大きな言語モデルはパラメータを更新せずに新しいタスクに適応する。 最近の経験的発見は根本的な矛盾を示しており、変圧器はマルティンゲールの性質を体系的に侵害している。 この違反は、臨界応用における不確実性定量化の基礎となる理論的基礎に挑戦する。
  論文  参考訳（メタデータ） (2025-07-15T22:20:11Z)
• Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
  バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。 我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。 本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
  論文  参考訳（メタデータ） (2025-04-13T16:49:37Z)
• Supervised Optimism Correction: Be Confident When LLMs Are Sure [91.7459076316849]
  教師付き微調整とオフライン強化学習の間には,新たな理論的関係が確立されている。 広く使われているビームサーチ法は、許容できない過度な最適化に悩まされていることを示す。 本稿では,トークンレベル$Q$-value推定のための簡易かつ効果的な補助的損失を導入したSupervised Optimism Correctionを提案する。
  論文  参考訳（メタデータ） (2025-04-10T07:50:03Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Rethinking Uncertainty Estimation in Natural Language Generation [6.3398383724486544]
  大規模言語モデル(LLM)は、現実のアプリケーションにますます採用されている。 不確実性推定法は複数の出力シーケンスを生成し解析し、LCMの不確実性を決定する。 単一出力シーケンスのみを用いて得られる利点を持つG-NLLを提案する。
  論文  参考訳（メタデータ） (2024-12-19T18:51:06Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。 本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-06-05T16:35:30Z)

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

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