多智能体大语言模型系统中并发异常的验证检测与预防

# 多智能体大语言模型系统中并发异常的可验证检测与预防 来源: https://arxiv.org/html/2606.17182 Sajjad Khan（独立研究者，电子邮箱：sajjad [email protected]）。文中引用的在线附录（第A–F节及补充表S1–S6），以及验证与实验制品——TLA+源码、Verus 验证器 crateverus-detector、参考运行时 mac-consistency-runtime 和 Python 框架——均作为本 arXiv 投稿的附属文件提供。

###### 摘要

多智能体 LLM 系统通过内存存储、向量索引和工具注册表共享状态。我们将此类共享建模为在确定性生成语义（即持久化执行引擎通过确定性重放所强制的机制）下的长时间运行读-生成-写操作，并在 TLA+ 中形式化了四种并发异常：陈旧生成、幻象工具、因果级联和工具效果重排序——这些是经典隔离异常的结构性类比，每种异常均附有 TLC 反例。这些异常构成的排除格是平凡的；贡献在于机械验证了*格内一个最大链的可实现性与严格分离性*，即 L0 ⊊ ⋯ ⊊ L4——据我们所知，这是此类运行时首个经过机器检查的一致性层级。一个包含 274 个 Verus 义务（零 assume、零 admit；信任基：两个结构公理和一个互斥体对应关系）的开发过程，证明了检测器相对于规约是可靠且完备的，并且每个运行时都实现了其避免集合。三个已部署的 Rust 运行时实现了 L0–L1（悲观锁、可序列化快照隔离、默认-SI），每个都针对陈旧生成进行了验证，并精化为其状态机；L2–L4 通过执行模式验证，并附有依赖无关的预防孪生方案（A3、A6、A2：0/10000/1000 对比 1000/1000），且 L2 还在三个模型族上进行了实时运行（A3 在所有 120 个撤销会话中均被预防）；L3/L4 仍为执行验证状态。预防成本有界而非零：快照隔离在一个工作负载上增加约 8% 的 token，悲观锁增加 1.6–2.3 倍——并非通常假设的数量级惩罚。我们重现了字节跳动 deer-flow 中的隐藏丢失更新问题，将其修复形式化为经过验证的 L0→L1 精化，并在 LangGraph 的 ToolNode 上展示了未修改输出中的工具效果重排序，通过 L3 提交顺序序列器予以消除。验证后的检测器、精化及可实现性制品是贡献所在；现象与格则是经典内容。

###### 索引术语：多智能体系统，内存一致性，隔离级别，形式化方法，TLA+，Verus，大语言模型。

## 1 引言

### 1.1 在已记录模式下的构造性故障

我们在用于激励 SagaLLM [1 (https://arxiv.org/html/2606.17182#bib.bib1)] 架构的旅行预订工作流中构造了一个场景：一个多智能体系统中，一个智能体预订航班，另一个智能体预订酒店，两者都查询并更新共享的旅行状态记录。假设航班预订智能体从共享状态中读取“旅行日期==6月14日”，然后进入持续数秒的生成阶段，在此期间起草预订请求。在此期间，用户（通过第三个智能体）将旅行日期更新为6月21日。当航班智能体提交时，它提交了原始日期，从而产生了与系统当前状态相矛盾的预订。运行时任何层均未发生故障。然而，系统产生了当前状态所无法证明的外部效果。SagaLLM 的补偿事务架构是对此故障模式的一种可能回应；Atomix 的进展门控工具调用 [2 (https://arxiv.org/html/2606.17182#bib.bib2)] 则是另一种。两者均未命名该现象，未将其置于分层的一致性保证设计空间中定位，也未正式证明运行时在何种条件下能够预防它。上述场景是对已发表工作中所记录架构模式的一个构造性实例，而非来自已部署生产系统的踪迹；定位由并发引起的不一致的生产踪迹本身便是一个研究问题，我们将在第6.2节 (https://arxiv.org/html/2606.17182#S6.SS2) 中进一步探讨。相比之下，一个已部署实例中较低层次的丢失更新异常（该异常构成了格的基）并非构造的：第6.5节 (https://arxiv.org/html/2606.17182#S6.SS5) 重现了字节跳动 deer-flow（一个广泛使用的智能体应用）开放问题中的一个实时隐藏丢失更新，该更新来自项目自身的回归测试，并将其修复形式化为一个经过验证的 L0→L1 精化。然而，该模式只是我们在第3节 (https://arxiv.org/html/2606.17182#S3) 中编录的五种并发异常之一，所有这些异常都特定于我们所提出的操作机制，并且现有的一致性理论均未涉及。

### 1.2 为什么现有理论不直接操作化这些现象

三种一致性理论传统涉及此问题，但没有一种直接适用。硬件模型（顺序一致性 [3 (https://arxiv.org/html/2606.17182#bib.bib3)]、全存储顺序、释放一致性 [4 (https://arxiv.org/html/2606.17182#bib.bib4)]、ARMv8 [5 (https://arxiv.org/html/2606.17182#bib.bib5)]、线性一致性 [6 (https://arxiv.org/html/2606.17182#bib.bib6)]）预设了有界操作延迟和静态确定的读集；长时间运行的智能体操作两者都不具备。数据库隔离理论 [7 (https://arxiv.org/html/2606.17182#bib.bib7),8 (https://arxiv.org/html/2606.17182#bib.bib8),9 (https://arxiv.org/html/2606.17182#bib.bib9)] 采用了我们在此遵循的逐异常特征化方法，但假设读集在事务的生命周期内通过锁或快照持有。分布式系统一致性 [10 (https://arxiv.org/html/2606.17182#bib.bib10),11 (https://arxiv.org/html/2606.17182#bib.bib11),12 (https://arxiv.org/html/2606.17182#bib.bib12),13 (https://arxiv.org/html/2606.17182#bib.bib13),14 (https://arxiv.org/html/2606.17182#bib.bib14)] 处理复制状态和消息传递参与者 [15 (https://arxiv.org/html/2606.17182#bib.bib15)]，但将操作视为具有可概括签名的离散事件，而非长时间运行、非确定性的过程。PACELC 公式 [16 (https://arxiv.org/html/2606.17182#bib.bib16)] 用延迟/一致性权衡精化了 CAP，这在概念上邻近我们的格，但并未将长生成阶段视为一级对象。非事务性一致性模型的经典分类法 [17 (https://arxiv.org/html/2606.17182#bib.bib17)] 提供了最接近的现有框架，我们的格必须相对于其进行定位；其级别是为网络传播下的复制存储定义的，并不直接适用于我们所研究的操作机制。第7节 (https://arxiv.org/html/2606.17182#S7) 将详细阐述这些比较。

三个近期的运行时解决了智能体部署中的并发问题。Atomix [2 (https://arxiv.org/html/2606.17182#bib.bib2)] 为工具调用提供了进展感知的事务语义；SagaLLM [1 (https://arxiv.org/html/2606.17182#bib.bib1)] 使用 Saga 风格的补偿；CodeCRDT [18 (https://arxiv.org/html/2606.17182#bib.bib18)] 在并行代码生成中使用 CRDT 实现强最终一致性。每个都命名了一个一致性点并展示了如何实现它；但都没有将其保证置于一个分层设计空间中。我们将在第6.4节 (https://arxiv.org/html/2606.17182#S6.SS4) 中非正式地提供这些放置。

### 1.3 差距与贡献

现有的多智能体 LLM 故障特征描述，包括最近的 NeurIPS 分类法 [19 (https://arxiv.org/html/2606.17182#bib.bib19)]，记录了一个不同的故障类别：认知和协调失败，如步骤重复、推理-行动不匹配以及智能体间失调。我们描述的并发故障在很大程度上缺席于此类分类法，因为当前一代的智能体基准测试并未在争用下对智能体间共享状态进行压力测试。经典的隔离层级——ANSI/SQL 隔离 [7 (https://arxiv.org/html/2606.17182#bib.bib7)]、Adya 的广义模型 [8 (https://arxiv.org/html/2606.17182#bib.bib8)]、Bailis/Hellerstein 对弱一致性的调查 [20 (https://arxiv.org/html/2606.17182#bib.bib20)]，以及可序列化快照隔离 [21 (https://arxiv.org/html/2606.17182#bib.bib21)]——描述了数据库事务的一个紧密相关的设计空间，但并未直接处理区分多智能体 LLM 机制的长时间推理阶段。我们并不声称提出了一个根本性的新理论，而是将这些经典特征描述移植到新的操作机制中，并附有机械验证的检测器、安全性和精化制品来支持这一移植。本文提供了这一移植；其相对于经典原作的权重如何，由读者自行判断。

该操作机制的三个特征超出了经典异常层级的建模假设，正是这些特征——而非孤立的异常——要求移植必须适应。首先，生成阶段具有*无界延迟*：数据库隔离理论假设事务在锁或快照下持有其读集，时间窗口有界，而智能体操作的读-提交间隔是一个持续数秒到数分钟的神经推理阶段，在此期间读集既未被锁定，也不能廉价地重新验证。其次，*工具注册表*是一级可变状态，在关系模型中没有对应物：A2（幻象工具）是对能力集的一致性失败，经典隔离根本不对此建模。第三，外部工具效果是*不可逆的*：数据库恢复的级联中止和原子提交机制假设效果可以撤销，而这正是 A3 和 A6 在已提交效果是外发电子邮件或支付时所失败的原因。各个异常是已知异常的结构性类比，我们不声称新的并发理论；贡献在于，这种*机制特征的组合*在经典分类法中是不可表达的，并且我们为此提供了机械验证的检测器、安全性和精化制品。

### 1.4 贡献

本文做出五项贡献。由四种形式化异常诱导出的布尔格 L = ⟨2^{A1,A2,A3,A6}, ⊆⟩ 作为组织性词汇服务于随后的实质性贡献；该格本身并非一项理论结果。本文的重点在于机械化及已部署的制品，即贡献 (4a)–(4c) 和 (5)–(5b)，而非目录或格。我们声称的新颖之处在于*组合*：针对形式化异常规约被证明*同时*是可靠*且*完备的 Verus 验证检测器；沿着整条链验证并部署在真实 LLM 智能体下实时运行的 L0–L1 一致性规程；以及针对已部署框架实际通道语义（LangGraph 的 reducer 和 AutoGen 的 ETag 持久化层）验证的精化——其中一项精化关闭了已发布应用（字节跳动 deer-flow）中一个重现的、实时的隐藏丢失更新。目录 (1)、组织性格 (2) 和快照不足的观察 (3) 是验证制品所挂靠的脚手架；现象是经典的。据我们所知，没有先前的工作机械验证了多智能体 LLM 运行时沿着整条链的一致性层级，或将其精化建立在已部署智能体框架实际提供的并发原语之上。这个差距——而非格——才是贡献所在。

(1) **异常目录** (第3节 (https://arxiv.org/html/2606.17182#S3))。我们识别出在提议的操作模型中出现的五种并发异常。其中四种——陈旧生成、幻象工具、因果级联、工具效果重排序——被形式化为 TLA+ 中操作历史之上的谓词，每种都通过一个显式的 TLC 反例踪迹在小的有限参数（|A|=2, |Cells|≤2, MaxOps≤4）下验证。第五种，分裂视图，超出了单存储操作模型（它需要复制），并单独在 Verus 模型层面形式化为一个单调主节点无分裂定理（第4.12节 (https://arxiv.org/html/2606.17182#S4.SS12)）。

(2) **作为组织框架的一致性格** (第4节 (https://arxiv.org/html/2606.17182#S4))。布尔格 L 有十六个点；我们沿着一条选定的最大链命名了五个显著点 L0,...,L4——这是 L 的二十四个线性扩展之一，基于操作理由而非数学优先性选择。该构造将 Berenson 等人 [7 (https://arxiv.org/html/2606.17182#bib.bib7)] 和 Adya [8 (https://arxiv.org/html/2606.17182#bib.bib8)] 的方法论扩展到了多智能体 LLM 机制中。

(3) **快照不足：新操作设置中的经典模式** (第4.5节 (https://arxiv.org/html/2606.17182#S4.SS5))。我们观察到，结构定义的生成快照不足以预防陈旧生成，并且该级别必须用显式的读集稳定性来增强。这呼应了快照隔离下的写偏斜模式 [7 (https://arxiv.org/html/2606.17182#bib.bib7),21 (https://arxiv.org/html/2606.17182#bib.bib21),22 (https://arxiv.org/html/2606.17182#bib.bib22)]，该模式在数据库文献中众所周知。我们的贡献在于将该模式形式化于第2节 (https://arxiv.org/html/2606.17182#S2) 的操作模型中，其中在中止时被丢弃的工作是 LLM 推理而非关系型更新。

(4a) **机械验证的检测器流水线** (第4.7节 (https://arxiv.org/html/2606.17182#S4.SS7))。我们在 Verus [23 (https://arxiv.org/html/2606.17182#bib.bib23)] 中机械验证了，对于四种形式化异常的 Rust 检测器函数相对于其 TLA+ 规约既是可靠*且*完备的，包括 A1 的值不匹配组件。该链在不使用 assume 或额外公理的情况下完成了二十四项义务。

(4b) **机械验证的运行时安全性（仅针对 A1）**。我们还在 Verus 中验证了，第6.6节 (https://arxiv.org/html/2606.17182#S6.SS6) 的所有三种运行时策略在其各自的抽象状态机上满足 ¬A1：悲观锁运行时（23项义务，无条件）、SSI 运行时（8项义务，无条件，validate_no_write=true 模式）以及默认-SI 运行时（9项义务，条件性于全写入者工作负载假设）。默认-SI 的结果是一个条件性工作负载特征描述，而非无条件保证：该运行时通过设计中的只读无写入旁路承认 A1（测量的静默残余：对分类工作负载为 3%，见第5.13节 (https://arxiv.org/html/2606.17182#S5.SS13)）——这一负面结果推动了将无条件 SSI 作为推荐的 L1 机制。在所有三个运行时中：安全定理证明体内部零 assume、零 external_body、零添加公理，共计四十项义务。三个已部署的运行时仅实现了 L0→L1 步骤；更高级别由专用的运行时模型（因果追踪带级联中止，第4.11节 (https://arxiv.org/html/2606.17182#S4.SS11)；Saga 补偿，第4.15节 (https)）验证。