验证性检测与预防多智能体大型语言模型系统中的并发异常行为
Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
摘要
多智能体LLM系统通过内存存储、向量索引以及工具注册表来共享状态。我们将这种状态共享建模为一系列在确定性生成语义下的读取-生成-写入操作——而这类操作是由确定性重放机制所强制执行的。我们还形式化了四种并发异常情况：生成数据已过期、工具出现“幽灵”现象、因果关系出现级联效应，以及工具效果的顺序排列问题。这些情况可以视为传统隔离问题的结构化类比，而每一种情况都有对应的TLC反例。针对这些异常情况的排除格是简单的；我们的研究还证明了其中一种最大链的可实现性以及严格的分离性——据我们所知，这是首个针对此类运行时环境进行机器验证的一致性层次结构。我们提出了274条Verus约束条件（包括零假设、零接受条件；信任基础：两个结构公理以及一个互斥对应关系），这些约束条件证明了检测器对规范的描述是正确且完整的，并且每种运行时环境都有其对应的避免策略。三个部署在Rust语言中的运行时环境实现了L0-L1阶段的功能（悲观锁机制、可序列化的快照隔离、默认SI机制），这些运行环境都经过了针对生成数据过期的验证，并且其状态机也得到了完善。L2-L4阶段则通过无依赖关系的预防机制得到了验证（A3、A6、A2：0/1000对比1000/1000）；L2阶段则在不同模型框架下进行了实时运行测试（在所有120个会话中均避免了A3机制的触发）。我们再现了字节跳动公司开发的ByteDance项目中的“无声丢失更新”现象，并将其修正为经过验证的L0到L1阶段的改进措施。此外，我们还展示了LangGraph项目中ToolNode节点在未经修改的输出结果上出现的工具效果顺序排列问题，这一问题可以通过L3级别的提交顺序排序机制来解决。经过验证的检测器、改进措施以及可实现性成果才是我们研究的重点；而那些现象和排除格则属于经典的数学概念而已。
English 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.