# 多智能体LLM系统中并发异常的验证检测与预防

- 来源：HuggingFace Daily Papers（社区热门论文）
- 发布时间：2026-06-15 08:00
- AIHOT 分数：53
- AIHOT 链接：https://aihot.virxact.com/items/cmqiaujmx0779slf05iavabo1
- 原文链接：https://arxiv.org/abs/2606.17182

## AI 摘要

本文将多智能体LLM系统的共享状态建模为确定性生成语义下的读-生成-写操作，并在TLA+中形式化四种并发异常。通过274个Verus义务（零assume，零admit）证明检测器对规范的正确性和完备性，实现三个Rust运行时（L0-L1悲观锁、可序列化快照隔离、默认SI）。L2-L4通过执行模式验证实现无依赖预防。再现了字节跳动deer-flow中的静默丢失更新和LangGraph的ToolNode中的tool-effect reordering，并给出形式化修复。

## 正文

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.