为多智能体大模型系统设计了可验证的并发异常检测与预防机制。
Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
- 基于TLA+形式化建模共享状态的并发操作，定义四类异常。
- 实现从L0到L4共五级一致性保证，其中L2-L4经验证可防止关键错误。
- 已在真实系统中部署，适用于高可靠性大模型应用开发。
多智能体大语言模型系统通过内存存储、向量索引和工具注册表共享状态。我们将其建模为在确定性生成语义下的长时读-生成-写操作——即持久执行引擎通过确定性重放所强制的模式，并在TLA+中形式化定义了四种并发异常：过期生成、幻影工具、因果级联和工具效应重排序，它们是经典隔离异常的结构对应物，每种都有TLC反例。这些异常的排除格是平凡的；本研究的贡献在于机械验证了其可实现性，并严格分离出其中一条最大链 $L_0 \subsetneq \cdots \subsetneq L_4$，据我们所知，这是首个针对此类运行时的机器检查一致性层级。开发过程中共建立274个Verus义务（零假设、零容许；信任基础：两个结构性公理和一个互斥对应），证明检测器对规范的完备性和正确性，以及各运行时对其避免集的正确性。三个已部署的Rust运行时实现了L0-L1（悲观锁、可序列化快照隔离、默认快照隔离），均通过过期生成检测并精化至状态机；L2-L4通过执行模式验证，配备无依赖的预防孪生机制（如A3、A6、A2：0/1000 vs 1000/1000），L2已在三个模型族上实际运行，成功防止所有120次回滚会话中的过期生成。我们复现了字节跳动deer-flow中的沉默丢失更新，并形式化其修复为从L0到L1的已验证精化；还展示了LangGraph的ToolNode在未修改输出下存在工具效应重排序，由一个L3提交顺序调度器移除。验证的检测器、精化关系及可实现性构件是核心贡献；异常现象与格结构则属经典范畴。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。