論文の概要: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
- arxiv url: http://arxiv.org/abs/2605.07935v1
- Date: Fri, 08 May 2026 16:05:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-11 19:43:39.186838
- Title: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
- Title（参考訳）: TraceFix: TLA+ 対策によるエージェントコーディネートプロトコルの修復
- Authors: Shuren Xia, Qiwei Li, Taqiya Ehsan, Jorge Ortiz,
- Abstract要約: TraceFixは、LLM(Large Language Model)マルチエージェント調整のための検証ファーストパイプラインである。
エージェントは、タスク記述から構造化中間表現(IR)としてプロトコルトポロジを合成する。
さらに,TLA+モデルチェッカー(TLC)の逆例を用いて,検証が成功するまでプロトコルを反復的に修復する。
- 参考スコア（独自算出の注目度）: 3.8706622179041745
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present TraceFix, a verification-first pipeline for Large Language Model (LLM) multi-agent coordination. An agent synthesizes a protocol topology as a structured intermediate representation (IR) from a task description, generates PlusCal coordination logic, and iteratively repairs the protocol using counterexamples from the TLA+ model checker (TLC) until verification succeeds. Verified process bodies are compiled into per-agent system prompts and executed under a runtime monitor that rejects out-of-topology coordination operations. On 48 tasks spanning 16 scenario families, all tasks reach full TLC verification; 62.5% pass on the first attempt and none requires more than four repair iterations. State spaces span six orders of magnitude yet verification completes in under 60 s for every task. A 3,456-run runtime comparison shows that topology-monitored execution achieves the highest task completion (89.4% average, 81.5% full) and that runtimes using the verified protocol degrade at roughly half the rate of prompt-only and chat-only baselines when model capability is reduced. A paired ablation under a fixed runtime shows that TLC-verified protocols cut deadlock/livelock (DL/LL) from 31.1% to 14.1%, with the largest separation under fault injection.
- Abstract（参考訳）: 本稿では,Large Language Model (LLM)マルチエージェント協調のための検証ファーストパイプラインであるTraceFixを提案する。
エージェントは、タスク記述から構造化中間表現(IR)としてプロトコルトポロジを合成し、プラスCal調整ロジックを生成し、検証が成功するまでTLA+モデルチェッカー(TLC)から逆例を用いてプロトコルを反復的に修復する。
検証されたプロセスボディはエージェントごとのシステムプロンプトにコンパイルされ、実行時に実行され、トポロジー外の調整操作を拒否する。
16のシナリオファミリーにまたがる48のタスクでは、全てのタスクが完全なTLC検証に到達し、62.5%が最初の試行に合格し、4回以上の修理を繰り返した。
状態空間は6桁だが、各タスクに対して60秒以下で検証が完了する。
3,456ランのランタイム比較では、トポロジ監視による実行がタスクの完了率が最も高く(平均89.4%、フル81.5%)、検証済みプロトコルを使用するランタイムは、モデル能力が低下すると、プロンプトのみのベースラインとチャットのみのベースラインの約半分の速度で低下する。
固定されたランタイムの下でペア化されたアブレーションは、TLCが検証したプロトコルがデッドロック/リベロック(DL/LL)を31.1%から14.1%に削減したことを示している。
関連論文リスト
- Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳（メタデータ） (2026-04-20T13:25:40Z) - Token Coherence: Adapting MESI Cache Protocols to Minimize Synchronization Overhead in Multi-Agent LLM Systems [0.0]
マルチエージェントLLMオーケストレーションは、エージェント、ステップ、アーティファクトサイズにおいて、単純なブロードキャストの下でO(n x S x |D|)としてスケールする。
この病理は完全状態再放送の構造的残余であり、マルチエージェント協調の固有の性質ではないと私は主張する。
私はArtifact Coherence System(ACS)を構築し、Token Coherence Theoremを証明します。
論文 参考訳（メタデータ） (2026-03-16T12:20:06Z) - Semantic Consensus: Process-Aware Conflict Detection and Resolution for Enterprise Multi-Agent LLM Systems [0.0]
エンタープライズAI自動化の主要なアーキテクチャとして,マルチエージェント大規模言語モデル(LLM)システムが急速に普及している。
生産は41%から86.7%の失敗率を示しており、その約79%は仕様や調整の問題に起因する失敗である。
6つのコンポーネントからなるプロセス認識フレームワークSemantic Consensus Framework(SCF)を提案する。
論文 参考訳（メタデータ） (2026-03-13T14:55:38Z) - GraphCue for SDN Configuration Code Synthesis [0.09558392439655013]
自動構成のためのトポロジグラウンド検索とエージェント・イン・ザ・ループ・フレームワークであるGraphCueを提案する。
628のバリデーションケースでは、GraphCueは20イテレーションで88.2%のパスレートを獲得し、9秒で95%のバリデーションループを完了している。
論文 参考訳（メタデータ） (2025-12-19T09:13:51Z) - Towards a Science of Scaling Agent Systems [79.64446272302287]
エージェント評価の定義を定式化し,エージェント量,コーディネーション構造,モデル,タスク特性の相互作用として,スケーリング法則を特徴付ける。
協調指標を用いて予測モデルを導出し,R2=0をクロスバリデーションし,未知のタスク領域の予測を可能にする。
ツールコーディネーショントレードオフ: 固定的な計算予算の下では, ツールヘビータスクはマルチエージェントのオーバーヘッドから不均衡に悩まされ, 2) 能力飽和: 調整が減少または負のリターンを, 単一エージェントのベースラインが45%を超えると達成できる。
論文 参考訳（メタデータ） (2025-12-09T06:52:21Z) - Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
大規模言語モデルに基づくマルチエージェントシステムは、協調的な問題解決において優れているが、エラーのカスケードには脆弱である。
我々は,MASにリアルタイム,教師なし,ステップレベルの誤り検出と自己補正を付与するメタ認知フレームワークMASCを提案する。
論文 参考訳（メタデータ） (2025-10-16T05:35:37Z) - SLEAN: Simple Lightweight Ensemble Analysis Network for Multi-Provider LLM Coordination: Design, Implementation, and Vibe Coding Bug Investigation Case Study [0.0]
SLEANは、.txtテンプレートを使用してLLM間の単純なプロンプトブリッジとして機能し、デプロイに深い技術知識を必要としない。
独立した分析、相互批判、仲裁によって形成される3フェーズプロトコルは、有害なAI生成コード提案をフィルタリングする。
ファイル駆動でプロバイダに依存しないアーキテクチャは、特別なコーディング専門知識のないデプロイメントを可能にします。
論文 参考訳（メタデータ） (2025-10-11T04:24:04Z) - Model Context Protocol for Vision Systems: Audit, Security, and Protocol Extensions [0.4779196219827507]
Model Context Protocol (MCP) は、エージェントとツールのインタラクションのためのスキーマ境界実行モデルを定義する。
これは、ビジョンシステムにおけるMPPのデプロイメントスケール監査である、最初のプロトコルレベルである。
我々は,9次元の合成忠実度にアノテートされた91個の視覚中心型MPPサーバを解析した。
論文 参考訳（メタデータ） (2025-09-26T18:20:08Z) - Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。
Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。
SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
論文 参考訳（メタデータ） (2025-09-25T14:05:55Z) - SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
SOPBenchは、各サービス固有のSOPコードプログラムを実行可能な関数の有向グラフに変換する評価パイプラインである。
提案手法では,各サービス固有のSOPコードプログラムを実行可能関数の有向グラフに変換し,自然言語SOP記述に基づいてこれらの関数を呼び出しなければならない。
我々は18の先行モデルを評価し、上位モデルでさえタスクが困難であることを示す。
論文 参考訳（メタデータ） (2025-03-11T17:53:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。