論文の概要: Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
- arxiv url: http://arxiv.org/abs/2606.17182v1
- Date: Mon, 15 Jun 2026 18:19:34 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-17 17:15:32.095697
- Title: Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
- Title（参考訳）: マルチエージェント大規模言語モデルシステムにおける並行異常の検証と防止
- Authors: Sajjad Khan,
- Abstract要約: マルチエージェント LLM システムは、メモリストア、ベクトルインデックス、ツールレジストリを経由する。
我々は、決定論的意味論の下で、長期にわたるリード・ジェネレーション・ライト操作などの共有をモデル化する。
われわれはTLA+の4つの異常を定式化した: 老化, ファントムツール, 因果カスケード, ツール・エフェクト・リオーダー。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Multi-agent LLM systems share state through memory stores, vector indices, and tool registries. We model such sharing as long-running read-generate-write operations under deterministic-generation semantics -- the regime durable-execution engines enforce by deterministic replay -- and formalize four concurrency anomalies in TLA+: stale-generation, phantom-tool, causal-cascade, and tool-effect reordering, structural analogues of classical isolation anomalies, each with a TLC counter-example. The exclusion lattice over these anomalies is trivial; the contribution is the mechanically verified realizability and strict separation of one maximal chain within it, $L_0 \subsetneq \cdots \subsetneq L_4$, to our knowledge the first machine-checked consistency hierarchy for such runtimes. A development of 274 Verus obligations (zero assume, zero admit; trust base: two structural axioms and a mutex correspondence) proves the detectors sound and complete against the specifications and each runtime its avoidance set. Three deployed Rust runtimes realize L0-L1 (pessimistic locking, serializable snapshot isolation, default-SI), each verified against stale-generation and refined to its state machine; L2-L4 are exec-mode-verified with dependency-free prevention twins (A3, A6, A2: 0/1000 versus 1000/1000), and L2 is run live across three model families (A3 prevented in all 120 retracted sessions). We reproduce a silent lost update in ByteDance's deer-flow, formalizing its fix as a verified $L_0 \to L_1$ refinement, and exhibit tool-effect reordering in LangGraph's ToolNode on unmodified output, removed by an L3 commit-order sequencer. The verified detector, refinements, and realizability artifacts are the contribution; the phenomena and lattice are classical.
- Abstract（参考訳）: マルチエージェントLLMシステムは、メモリストア、ベクトルインデックス、ツールレジストリを通じて状態を共有する。
決定論的セマンティクス(deterministic-generation semantics, 決定論的リプレイ(deterministic replay, 決定論的リプレイ(deterministic replay, 決定論的リプレイ(deterministic replay, 決定論的リプレイ(deterministic replay, 決定論的リプレイ(deterministic replay))によって強制される)による、長期にわたるリード・ジェネレーション・ライト操作の共有や、TLA+における4つの同時並行異常(stale-generation, phantom-tool, causal-cascade, ツール・エフェクト・リオーダー)、古典的アイソレーション異常の構造的類似、それぞれTLC反例)の形式化をモデル化する。
これらの異常に対する排除格子は自明なものであり、その寄与は機械的に証明された実現可能性と、その内の1つの最大鎖の厳密な分離($L_0 \subsetneq \cdots \subsetneq L_4$)である。
274Verusの義務(ゼロ仮定、ゼロ許容、信頼ベース:2つの構造公理とミューテックス対応)の開発は、検出器が仕様と各ランタイムの回避セットに対して健全で完備であることを証明している。
3つのデプロイされたRustランタイムはL0-L1(悲観的ロック、シリアライズ可能なスナップショット分離、デフォルト-SI)を認識し、それぞれが古い世代に対して検証され、ステートマシンに洗練されている。
我々はByteDanceのdeer-flowでサイレントな失われた更新を再現し、その修正を検証済みの$L_0 \to L_1$ refinementとして定式化し、L3コミット順序シーケンサによって削除された未修正出力上のLangGraphのToolNodeでツール効果の並べ替えを示す。
確認された検出器、精細化および実現可能性アーティファクトは貢献であり、現象と格子は古典的である。
関連論文リスト
- PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
PRIMAは、複数時間にわたる協調型マルチエージェント研究システムとして運用されている。
主なコントリビューションは、生存可能な障害モードのための3つの運用パターンである。
グラフ同型ケーススタディは、生成されたアーティファクトのアーキテクチャ的クレームを根拠にしている。
論文 参考訳（メタデータ） (2026-05-23T23:27:46Z) - CasualSynth: Generating Structurally Sound Synthetic Data [44.80087038178069]
大言語モデル(LLM)は、現実的な合成データを生成するが、その出力がターゲットドメインを管理する因果的メカニズムを尊重することを保証しない。
本稿では,意味的実現から因果構造の生成を分離するフレームワークCausal Synthを紹介し,因果的妥当性と言語学的にリッチな合成データを生成する。
論文 参考訳（メタデータ） (2026-05-17T16:21:01Z) - Logic-Regularized Verifier Elicits Reasoning from LLMs [63.65875399266337]
論理規則で正規化された教師なしの検証器であるLOVERを提案する。
ローバーは、定理を二項潜在変数として扱い、内部の活性化を活用し、3つの論理的制約を課す。
ローバーは教師なしのベースラインを大幅に上回る。
論文 参考訳（メタデータ） (2026-05-07T09:03:49Z) - Pairwise matrices for sparse autoencoders: single-feature inspection mislabels causal axes [2.741152471987327]
標準スパースオートエンコーダプロトコルは、各機能をトップアクティベーションコンテキストからラベル付けし、単一機能ステアリングによって検証する。
本稿では,Qwen3-1.7B-Instruct上での標準ワンコーナプロトコルミスをGemma-2-2B-itで再現した,ペアワイズ行列プロトコルと共変ステアリング係数を提案する。
これら3つの所見はGemmaでモデル特異的な損傷シグネチャを再現し,一致した形状制御はCIを10倍に分離する。
論文 参考訳（メタデータ） (2026-05-04T21:11:21Z) - OrgForge-IT: A Verifiable Synthetic Benchmark for LLM-Based Insider Threat Detection [0.0]
本稿では,決定論的シミュレーションエンジンが基底真理を維持し,言語モデルが表面の散文のみを生成する検証可能な合成ベンチマークを提案する。
コーパスは51日の模擬日、2,904回のテレメトリ記録を96.4%のノイズレートで記録し、単面と単日のトリアージ戦略を破るために設計された4つの検出シナリオをカバーしている。
論文 参考訳（メタデータ） (2026-03-23T19:03:53Z) - Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。
テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。
そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
論文 参考訳（メタデータ） (2026-02-02T09:14:51Z) - Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
オープンソースのDeepSeek、Llama、Qwenのエコシステムから、705の現実世界の失敗に関する大規模な実証的研究を行った。
ホワイトボックスオーケストレーションは、モデルアルゴリズムの欠陥からデプロイメントスタックのシステム的脆弱性へと、信頼性のボトルネックを移動させます。
論文 参考訳（メタデータ） (2026-01-20T06:42:56Z) - The Trojan in the Vocabulary: Stealthy Sabotage of LLM Composition [31.827344197678126]
トケナイザー移植はサプライチェーンの脆弱性を導入する。
係数再利用の幾何学を利用して、我々の攻撃は非対称的な実現可能性ギャップを生み出す。
実験的に、攻撃は訓練なしで、スペクトルの模倣を達成し、異常検出を回避する。
論文 参考訳（メタデータ） (2025-12-31T19:00:03Z) - Higher-order Linear Attention [59.92962330635185]
スケールされたドット積の注意の二次コストは、自己回帰言語モデルを長いコンテキストにスケールするための中心的な障害である。
本稿では,高次線形注意(Higher-order Linear Attention, HLA)を提案する。
論文 参考訳（メタデータ） (2025-10-31T07:54:37Z) - Beyond 'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models [86.88657425848547]
大型推論モデル(LRMs)はすでに長い連鎖推論のための潜在能力を持っている。
我々は、自動生成の自己検証タスクを使用して、モデルに推論、帰納、誘拐の3つのメタ能力を持たせることを明確にした。
我々の3つのステージ・パイプラインの個別アライメント、パラメータ空間のマージ、ドメイン固有の強化学習は、命令調整ベースラインと比較して10%以上のパフォーマンス向上を実現します。
論文 参考訳（メタデータ） (2025-05-15T17:58:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。