論文の概要: VERDICT: Multi-Agent Parallel Modular Verification
- arxiv url: http://arxiv.org/abs/2610.29147v1
- Date: Wed, 21 Oct 2026 03:33:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-23 00:40:06.191793
- Title: VERDICT: Multi-Agent Parallel Modular Verification
- Title（参考訳）: VERDICT:マルチエージェント並列モジュール検証
- Abstract要約: 帰納的検証(deductive validation)は,個々の機能の振る舞いを形式的な契約で要約するモジュール推論を通じて,大規模なソフトウェアシステムにスケールする。
大規模言語モデル(LLM)の最近の進歩により、前例のない規模で自動仕様合成が可能になった。
本稿では,大規模プログラムのモジュラーデダクティブ検証を並列化するフレームワークであるVERDICTを提案する。
- 参考スコア（独自算出の注目度）: 25.46830791373988
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification. Its central bottleneck is specification synthesis: constructing the contracts required for modular verification. Recent advances in large language models (LLMs) have enabled automated specification synthesis at unprecedented scale. However, existing approaches remain fundamentally bottom-up, requiring callees to be verified before their callers. This dependency limits parallelism and provides no principled mechanism for resolving interprocedural inconsistencies that propagate across call chains. We present VERDICT, a multi-agent framework for parallelizing modular deductive verification of large-scale programs. VERDICT is built on two key principles. First, assumption-based parallel specification synthesis assigns an agent to each function and allows it to proceed immediately using assumed contracts for its callees, enabling verification to proceed in parallel across the program. Second, bidirectional interprocedural conflict reconciliation resolves the inconsistencies introduced by these assumptions: when a synthesized contract contradicts an assumption, agents propagate the necessary revisions both up and down the call graph until the contracts converge. Experimental results on real-world C programs show that VERDICT synthesizes higher-quality specifications than existing approaches while substantially reducing verification time. In particular, VERDICT is the first approach that scales to the complete 20,000-line X.509 parser, ruling out nearly all the potential runtime errors within hours, whereas prior tools like PREGUSS fall far short even after days of execution.
- Abstract（参考訳）: 帰納的検証はモジュラー推論を通じて大規模ソフトウェアシステムにスケールし、形式的な契約は個々の機能の振る舞いを要約し、独立した検証を可能にする。
その中心となるボトルネックは仕様合成であり、モジュラー検証に必要な契約を構築することである。
大規模言語モデル(LLM)の最近の進歩により、前例のない規模で自動仕様合成が可能になった。
しかし、既存のアプローチは基本的にボトムアップのままであり、呼び出し前に呼び出し元を検証する必要がある。
この依存関係は並列性を制限し、コールチェーンをまたぐ相互不整合を解決するための原則的なメカニズムを提供しない。
本稿では,大規模プログラムのモジュラー・デダクティブ・検証を並列化するマルチエージェント・フレームワークであるVERDICTを提案する。
VERDICTは2つの重要な原則に基づいている。
まず、仮定ベースの並列仕様合成は、各関数にエージェントを割り当て、その呼び出し元に対する仮定されたコントラクトを即座に使用し、検証をプログラム間で並列に進めることを可能にする。
第二に、双方向の相互競合の和合はこれらの前提によってもたらされる矛盾を解消する: 合成された契約が仮定に矛盾すると、エージェントは契約が収束するまで、呼び出しグラフの上下の両方で必要な修正を伝達する。
実世界のCプログラムの実験結果から,VERDICTは既存の手法よりも高品質な仕様を合成し,検証時間を著しく短縮することを示した。
特にVERDICTは、完全な2万行のX.509パーサにスケールする最初のアプローチであり、数時間以内にほぼすべての実行時エラーを排除している。
関連論文リスト
- TELLER: Non-intrusive Cross-Layer Root-Cause Analysis for LLM Inference [47.62941623025392]
本稿では,非侵入的でログ対応なLLM推論フレームワークであるTELLERについて紹介する。
TELLERはモデルバイナリを変更することなく、NVTX/CUPTIトレースとサービスログを収集する。
リクエスト毎のコールチェーンツリーを再構築し、ログ行と対応する実行ステップをアライメントする。
これらの表現に加えて、TELLERは数値的候補のローカライゼーションとマルチモーダルな根起因モデルを組み合わせる。
論文 参考訳（メタデータ） (2026-08-03T09:39:11Z) - Heaviside Continuity of Rolling Coefficients for Eliminating Epistemic Entropy in Large Language Models [0.0]
Heaviside Continuity of Rolling Coefficients (HCRC) は検証ファーストな実行フレームワークである。
これは、ヘビサイドゲートが支配する述語による状態遷移として推論を再構成する。
HCRCは、モデルの信頼性と並列ワーカーアーキテクチャからの独立した検証信号を組み合わせることで、正しい予測が満たされた場合にのみ実行を前進させることができる。
論文 参考訳（メタデータ） (2026-07-06T00:29:34Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
PRIMAは、複数時間にわたる協調型マルチエージェント研究システムとして運用されている。
主なコントリビューションは、生存可能な障害モードのための3つの運用パターンである。
グラフ同型ケーススタディは、生成されたアーティファクトのアーキテクチャ的クレームを根拠にしている。
論文 参考訳（メタデータ） (2026-05-23T23:27:46Z) - From I/O to Code with Discovery Agent [103.88427301265669]
IO2Codeの発見エージェントであるDIO-Agentを提案する。
本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。
大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
論文 参考訳（メタデータ） (2026-05-14T18:57:32Z) - FeedbackLLM: Metadata driven Multi-Agentic Language Agnostic Test Case Generator with Evolving prompt and Coverage Feedback [0.0]
テストケース生成に対する従来のアプローチは、しばしば手作業と計算オーバーヘッドの増大を伴う。
We propose FeedbackLLM, a novel language-agnostic test case generation framework based on tightly coupled two-stage approach。
提案アーキテクチャの性能は,CプログラムとPythonプログラムに関連する標準ベンチマークプログラムで評価される。
論文 参考訳（メタデータ） (2026-05-02T05:43:29Z) - IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
既存のパイプラインは不透明でエンドツーエンドの出力を生成し、検査の中間状態は公開しない。
IMPACT-Cycleは,マルチモーダル反復クレームレベルのメンテナンスとして,長時間ビデオ理解を再構築するマルチエージェントシステムである。
論文 参考訳（メタデータ） (2026-04-22T03:03:33Z) - Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。
動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。
我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
論文 参考訳（メタデータ） (2026-04-17T14:56:45Z) - UniT: Unified Multimodal Chain-of-Thought Test-time Scaling [85.590774707406]
統一モデルは単一のアーキテクチャ内でマルチモーダル理解と生成の両方を扱うことができるが、通常は出力を反復的に書き換えることなく単一のパスで操作する。
マルチモーダルなテストタイムスケーリングのためのフレームワークであるUniTを導入し、単一の統一モデルで複数のラウンドをまたいだ推論、検証、精査を可能にします。
論文 参考訳（メタデータ） (2026-02-12T18:59:49Z) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
大規模言語モデルに基づくマルチエージェントシステムは、協調的な問題解決において優れているが、エラーのカスケードには脆弱である。
我々は,MASにリアルタイム,教師なし,ステップレベルの誤り検出と自己補正を付与するメタ認知フレームワークMASCを提案する。
論文 参考訳（メタデータ） (2025-10-16T05:35:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。