当AI特工们共享记忆时，谁来保证它们不会"记错账"？——独立研究者首次用机器验证的方式，为多智能体AI系统的并发安全问题建立了完整的理论防线

这项由独立研究者完成的研究以预印本形式发布于2026年6月，论文编号为arXiv:2606.17182，感兴趣的读者可通过该编号在arXiv平台查阅完整原文。

一、一个看起来没有问题、却悄悄出了问题的故事

在正式进入这项研究之前，先来看一个场景。你正在通过一个AI助手系统预订行程：一个AI负责订机票，另一个AI负责订酒店，第三个AI则是你本人在对话框里说"把出发日期改成21号"的那个接口。订机票的AI读到了"14号"这个出发日期，然后它开始"思考"——这个思考过程在大型语言模型里叫做"推理生成"，需要几秒钟甚至更长时间。就在它思考的时候，你通过第三个AI把日期改成了21号。订机票的AI思考完毕，提交了预订请求，但用的还是14号。

这个过程里没有任何系统报错，没有任何警告，也没有任何人意识到出了问题。机票订好了，日期却是错的。你去住酒店，发现机票日期与酒店日期不匹配。这不是网络故障，也不是程序漏洞，而是一种叫做"并发异常"的问题，类似于两个人同时在同一张白板上写字，结果字迹叠在一起、互相覆盖。

这项研究要解决的，正是这类发生在多个AI智能体共同工作时、因为时间差和共享数据而产生的"数据不一致"问题。更重要的是，这项研究不仅提出了理论框架，还用严格的数学工具验证了检测方法和防护机制的正确性——这在这个领域里是第一次。

二、多智能体系统的"共享记忆"到底是个什么问题

理解这项研究，需要先理解多智能体AI系统是如何运作的。把一个多智能体系统想象成一家有很多员工的公司，这些员工共用一块大白板来记录项目信息。每个员工在开始处理任务时，会先看一眼白板上的内容，然后去自己的办公桌上思考和起草方案，最后把结果写回白板。

问题在于，这个"思考和起草"的过程可能需要几秒甚至几分钟。在这段时间里，其他员工可能已经修改了白板上的内容。等第一个员工回来把方案写上去，他的方案是基于已经过时的信息写出来的，但白板上不会有任何迹象表明这个信息是过时的。

对于普通的数据库系统，这个问题早已有成熟的解决方案，叫做"事务隔离"。银行系统在你转账的时候会锁住相关账户，确保没有人在转账过程中同时修改余额。但AI推理生成这个"思考"过程和银行转账不同，它持续时间长、消耗资源大，如果在这段时间内锁住所有相关数据，代价会非常高昂。更麻烦的是，AI系统还有工具注册表这种数据库里根本没有的东西——某个AI在执行任务时调用了一个工具，但这个工具在它完成生成之前已经被管理员下线了。

数据库理论、硬件内存模型和分布式系统理论这三个领域在各自范围内都有成熟的并发控制框架，但没有一个直接适用于AI多智能体系统这种"长时间生成+外部不可撤销副作用"的场景。这正是这项研究填补的空白。

三、四种会悄悄捣乱的"幽灵"——异常类型的分类与定义

研究者把多智能体系统中会出现的并发异常整理成了一份"异常目录"，并用TLA+这门专门用于描述并发系统行为的数学语言，精确地写出了每种异常的触发条件，然后用TLC这个模型检查工具，在小规模的系统模型里自动找出了每种异常发生时的具体案例。

第一种异常叫做"陈旧生成"，也就是前面订机票例子里发生的那种情况。技术上的定义是：一个AI在时刻A读取了某个数据的值，另一个AI在时刻B对这个数据写入了新值（B在A之后），然后第一个AI在时刻C把基于旧值的结论提交了出去（C在B之后）。换句话说，这个AI的结论建立在它自己已经知道"可能已经过时"的信息上。模型检查工具在只有2个AI智能体、1个数据格和最多4次操作的小系统里，5步之内就找到了一个具体的反例。

第二种异常叫做"幽灵工具"。AI系统里的工具注册表记录着哪些工具可以被调用——类似一个工具箱的目录。一个AI在任务开始时查了工具箱目录，发现有个叫做"发邮件"的工具，于是计划用它。但在它思考方案的时候，系统管理员把这个工具下架了。等它提交方案时，它指定要调用的工具已经不存在了。这在数据库理论里没有对应的概念，因为数据库的字段是相对固定的，而AI系统里的工具注册表是动态变化的能力集合。

第三种异常叫做"因果级联"。这发生在使用"补偿事务"（一种出了问题就反向撤销操作的机制）的系统里。假设AI-甲写入了一条数据，AI-乙读取了这条数据并在此基础上写入了自己的结论，然后AI-甲的操作因为某种原因被撤销了。那么AI-乙的结论是建立在一条已经被撤销的数据之上的，属于悬空的引用。如果AI-乙的结论已经触发了外部动作——比如发送了一封邮件——这个邮件不可能被撤回，因果的混乱就此扩散开去。

第四种异常叫做"工具效果乱序"。当一个AI在一次操作里依次发出了多个工具调用，比如"先创建数据库，再运行迁移脚本，再填入初始数据"，但底层系统因为异步执行导致这些调用实际完成的顺序颠倒了——比如先填了初始数据，再创建数据库——结果自然是灾难性的。在数据库系统里，两阶段提交协议会保证操作的原子性，但AI工具调用的外部副作用往往无法撤销，更无法事后重排序。

研究者还识别出了第五种异常"分裂视图"——在多个副本之间，两个AI同时读到了同一个数据格的不同值——但这种异常超出了单一存储模型的范畴，用不同的方式单独处理了，具体做法放到后文再说。

四、一把"一致性阶梯"——从混乱到有序的五个台阶

有了四种形式化定义的异常，研究者就可以构建一个分类体系了。这个体系的逻辑是：一个系统能防止哪几种异常，就站在哪个台阶上。四种异常可以组合出16种不同的"只防止其中某几种"的系统，形成一个数学上叫做"布尔格"的结构——你可以把它想象成一张从"啥都不管"到"全部防住"的层级地图。

研究者在这张地图上挑出了5个有实际意义的点，形成一条从低到高的阶梯。最底层L0代表什么保护都没有的系统，任何异常都可能发生。往上一台阶是L1，防止了"陈旧生成"，保证每个AI的结论至少是基于读取时那一刻的正确数据。再上一台阶是L2，在L1的基础上还防止了"因果级联"，确保被撤销操作的所有下游依赖都会被一并撤销。L3在L2基础上再防止"工具效果乱序"，保证工具调用按照AI设想的顺序对外界产生影响。最顶层L4则额外防止了"幽灵工具"，确保AI调用的工具在整个操作周期内始终有效。

这把阶梯的核心价值不是它的层级结构——任何人都可以画一把阶梯——而是研究者为每个台阶都提供了严格的机器验证证明，表明每个台阶确实能防住它声称能防住的异常，而且不同台阶之间确实存在严格的区分（更高台阶能防住低台阶无法防住的情况）。

还有一个值得单独说的观察：光有"读取时的快照"是不够的。你可能以为，如果一个AI在开始操作时记录下当时所有相关数据的值，之后的生成只用这份记录，就不会有问题了。但研究者发现事实并非如此。快照只能保证"读取时的值是当时正确的"，却不能保证"基于这个值的结论提交时仍然是有意义的"——因为从读取到提交之间，其他AI可能已经修改了这个数据，使得原本合理的结论变得无效。这个观察被TLC工具用一个具体的5步反例验证了。这跟数据库领域一个叫做"写偏斜"的经典问题非常相似，只是发生在AI推理的时间尺度上。

五、机器证明：不是"我觉得没问题"，而是"证明了没问题"

研究中最重量级的贡献，是用Verus这门专门用于验证Rust程序正确性的工具，对检测器和防护机制进行了机器证明。

先解释一下什么是机器证明。普通的软件测试是"在很多情况下试了试，没发现问题"；机器证明是"在逻辑上穷举了所有可能的情况，证明了任何情况下都没问题"。后者要强得多，也要难得多。Verus要求你不仅写出程序代码，还要写出数学命题，然后由计算机自动验证这些命题对所有可能的输入都成立。

研究中写出的检测器（用来判断一段操作历史是否存在某种异常的程序）被验证了"健全性"和"完备性"：健全性意味着检测器报告的每一个异常都是真实的异常（不会误报）；完备性意味着真实存在的异常检测器一定会报告（不会漏报）。这两者合在一起，等于说检测器的判断和理论定义是完全等价的。

整个验证工作共产生了274条独立的验证义务（你可以把每条想象成一个需要被证明的数学命题），全部通过，没有一个是通过"我相信这是对的"或"跳过这个不证了"这样的方式绕过的。研究者特别强调，整个证明链只依赖两条基础公理：一条是说字符串标识符的编码是单射的（不同的标识符不会映射到同一个数字），另一条是说程序里用"NULL"这个字符串代表空值而规范里用数字0代表空值、两者是对应的。除此之外没有任何未经证明的假设。

对于L0和L1这两个最低的台阶，研究者还实际部署了三个用Rust语言写成的运行时系统，分别对应"悲观锁"、"可序列化快照隔离"和"默认快照隔离"三种策略，并验证了这三个真实运行的系统满足各自的保证。悲观锁的做法是：一个AI开始操作某个数据格时，先把它锁住，不让其他AI同时操作同一个格子，直到操作完成才解锁。这种方式完全消除了陈旧生成，代价是操作只能串行进行。可序列化快照隔离的做法是：在提交时检查从读取到提交这段时间内有没有其他AI修改了相同的数据，如果有就中止当前操作。这种方式允许更多并行操作，代价是可能出现中止和重试。

六、超快照的防护：L2到L4是如何工作的

对于更高的台阶L2、L3和L4，研究者分别构建了专门的运行时模型，并同样进行了机器验证。

防止"因果级联"（L2）的机制是让每个操作都记录自己的"因果前驱集"——也就是这个操作在读取时依赖了哪些其他操作的结果。当某个操作被撤销时，系统会顺着这条因果链把所有还没被撤销、却依赖了被撤销操作的"幸存者"也一并撤销。关键在于，这个因果链被记录成了一个"闭包"（数学上的概念，大概意思是"包含了所有间接依赖"），所以不需要迭代查找、只需要一轮就能找到所有需要撤销的操作。研究者在Verus里证明了这个单轮撤销确实足够，而且对所有可达的系统状态都成立。

研究者还把L2的验证推进到了可运行代码的层面。他们写了一个可以实际执行的Rust程序，并在Verus里证明了这个程序完全精确地对应了理论模型，因此理论保证直接适用于运行中的程序。在实验中，他们生成了1000个会触发因果级联的场景，在有L2防护的运行时里全部通过（0次异常），在没有防护的基线运行时里全部出现异常（1000次异常）。

防止"工具效果乱序"（L3）的机制基于一个"提交顺序序列器"的概念：系统等到一批工具调用全部完成后，才按照它们被发出的原始顺序依次对外界产生效果，而不是按照它们完成的顺序。研究者证明了这个序列器的对外效果时间戳相对于发出顺序是单调递增的——这意味着序列器永远不会把后发出的工具调用排在先发出的调用之前对外产生效果。

防止"幽灵工具"（L4）的机制是让每个操作在开始时锁定它打算调用的工具的签名，提交时检查这个工具是否仍然以相同的签名存在，否则中止操作。这类似于你在网上购物时"锁定价格"，如果商品在你下单之前涨价了，系统会提示你确认新价格而不是悄悄扣更多的钱。

七、"分裂视图"的特殊处理：多副本场景下的保证

第五种异常"分裂视图"因为需要多个存储副本才能发生，无法在单一存储模型里直接形式化，所以用了单独的方式处理。研究者在Verus里建立了一个追加式单调日志的模型，代表主副本的行为，并证明了一个叫做"单调主副本无分裂"的定理：两次从主副本读取同一个版本号的操作，一定会读到相同的值。也就是说，只要读操作总是从主副本进行，就不会出现分裂视图。当然，从落后的副本读取时仍然可能出现分裂视图，这正是"读主副本"这个约束消除的问题，而不是一个逻辑漏洞。

整个证明只依赖于追加式单调日志的结构性质，而不是简单地说"因为只有一个副本所以两次读到的值一定相同"——后者是一个空洞的同义反复，前者才是有实质内容的定理。

八、现实世界里的测试：问题到底有多真实？

理论和机器证明之外，研究者还做了大量实验，用真实的AI模型来测试检测器和防护机制在实际条件下的表现。

实验分几个层次展开。首先，研究者设计了三种工作负载：编辑-审核（两个AI同时读取同一个文档格，然后提交不同的修改）、计划-执行（一个AI写计划，另一个AI读计划后写结果，严格串行）、分诊（三个AI形成流水线，中间环节的读操作可能与上下游产生重叠）。在编辑-审核场景下，由于两个AI都被要求在第一轮就读取文档格，陈旧生成的发生率是100%——这不是随机发现，而是由工作负载结构决定的，主要用于验证检测器能正确识别出问题。在计划-执行场景下，发生率是1%（源于某次意外的重复读取）。在分诊场景下，发生率是35%，这是三种工作负载里唯一一个有实际测量意义的数字。

研究者还把这个检测器用于分析公开的多智能体失败案例数据集MAST-Data，这个数据集包含7个框架、1242个带标注的执行轨迹。在成功解析的600个轨迹里，陈旧生成的发生率是0。结合"共享可变状态"这个陈旧生成发生的结构性前提条件，研究者解释道：MAST数据集里大多数框架主要使用消息传递而非共享可变状态，因此这个前提条件本身就很少满足，这才是0发生率的根本原因，而不是说陈旧生成在实践中不重要。

在使用LangGraph框架的StateGraph模式（这是一种确实使用共享可变状态的模式）下，90%的会话出现了陈旧生成的证据，其中89%涉及跨智能体的数据陈旧。研究者检查了具体的触发案例：执行AI在时刻9读取了任务格的值"计划并执行数字文件存储系统的整理"，而计划AI随后在时刻14把同一个格的值改成了"继续执行……的整理"，读取在写入之前，值不同，智能体不同，完全符合陈旧生成的定义。

九、防护的代价到底有多大？

一个很自然的担心是：加了这些保护机制，AI系统会不会变得非常慢或者非常贵？研究者做了详细的成本测量，结果出乎很多人的预料。

在使用GPT-4o模型的实验里，可序列化快照隔离（L1的推荐实现方式）在大多数工作负载下与无防护的基线在每次会话的token消耗上看不出区别——置信区间完全重叠。只有在一种特定工作负载（计划-执行）下，通过配对设计才能分辨出约8%的token开销，这个数字在其他工作负载下统计上等同于零。研究者特别指出，"统计上与零无法区分"不等于"确实是零"，实际开销是"在低争用到中等争用场景下有界且可预测"。

悲观锁的代价更高，在多阶段流水线（分诊场景）下约为基线的1.62倍（GPT-4o）到2.3倍（Claude Sonnet 4.5），在低争用场景下与基线几乎无差异。这个数字比"中止一次AI推理等于浪费一大笔钱"的直觉要低得多，原因在于被中止的推理有很大一部分token是被缓存处理的，实际计算代价远低于从头生成一次的代价。

研究者还测量了在更高争用条件下的成本规律：token开销与实际发生的中止率呈线性关系，截距与零无显著差异，斜率约为108%——也就是说，每发生一次中止，大约消耗相当于原操作一倍的额外token。只要中止率低于约14%，总开销就能控制在15%以内。

十、在真实框架里发现并修复真实的问题

除了理论和实验，研究者还做了两件很有说服力的事：重现了一个真实的线上bug，并且用验证过的理论把修复方案表达成了一个精确的数学命题。

ByteDance（字节跳动）的deer-flow项目（一个广泛使用的AI代理应用）在2026年5月报告了一个用户可见的bug：待办事项列表在流式传输时是可见的，但运行完成后就消失了。项目自己的回归测试把原因归结为下游节点以一个"todos=None"的更新覆盖了已经积累好的待办事项，这正是LangGraph默认"最后写入者获胜"通道的一个典型后果。研究者在未修改的LangGraph运行时上重现了这个bug，然后用Verus写出并验证了一个证明：使用带有合并函数的通道（把所有写入合并而不是只保留最后一个），可以保证每个写入的贡献都被保留。这把"加个合并函数就好了"从一个经验性补丁变成了一个有数学保证的修复方案。

LangGraph的ToolNode（标准工具调用节点）使用asyncio.gather并发执行一个AI轮次发出的所有工具调用。gather会把结果按照输入顺序返回，但各个工具调用对外界产生副作用的顺序是按照它们完成的顺序，而不是按照AI发出的顺序。研究者在发布的ToolNode版本上重现了这个问题：一个需要按序执行的五步流程（创建数据库→运行迁移→填入数据→建立索引→开启流量），在GPT-4o-mini把全部步骤打包在一个轮次发出时，22次出现了乱序执行（在18次完整流程里全部出现乱序）。更让人担心的是，在AI返回的对话记录里，工具调用结果是按输入顺序排列的，看起来完全正常——只有外部系统的状态是乱的，而外部状态正是一般人不会去检查的地方。用研究者的L3提交顺序序列器替换默认的ToolNode后，在所有产生乱序的33次多工具轮次里，乱序发生次数降为0。

十一、这套理论的边界在哪里

研究者对自己工作的局限性做了相当诚实的陈述。AI推理生成被假定为确定性的（给定相同输入总是产生相同输出），但真实的AI模型是随机的。这个假设主要影响"陈旧生成"检测器里的值比较这个环节：如果一个AI读到了过时的值，它有可能碰巧还是生成了和读到最新值一样的输出，这时检测器就不会报告异常，尽管陈旧读取确实发生了。研究者在实验里测量了这个"操作上不一致的概率"，发现它高度依赖于AI在工作流中的角色：纯产出型AI（只管生成内容，不评估内容）的不一致率是0%，纯评估型AI（需要对读取到的值做出判断）的不一致率高达100%。换句话说，检测器报告的异常里有一部分对纯产出型AI来说不会造成实际影响，而对评估型AI来说几乎每一次异常都是有实际影响的。

验证结果也有范围限制。L0和L1两个台阶有真实部署的Rust运行时，并做了机器验证的spec-runtime细化证明，表明真实运行的代码对应理论模型。L2的防护也有可执行的Rust代码并验证了精确对应关系，还在真实AI模型上做了活的实验。L3和L4有机器验证的模型，也有依赖自由的基准对比实验，但还没有在真实AI代理循环下运行的记录。并发行为的验证（多个线程同时运行时的正确性）部分依赖于标准库的互斥锁是正确实现的这个假设，而这个假设本身还没有被完全形式化地证明。

说到底，这项研究做的事情有点像给一栋建筑物做结构安全审查。它没有重建整栋建筑，也不能保证建筑物里永远不发生任何事故，但它提供了一套系统化的方法来识别哪些地方有可能出问题、问题的严重程度如何、以及有哪些有保证的加固方案。归根结底，当AI系统越来越多地被用于需要多个AI协同工作的复杂任务时，这种"理论上有保证、代码上有验证"的安全框架，比"跑了很多测试觉得没问题"要可靠得多。

有兴趣深入了解的读者，可以通过arXiv:2606.17182找到完整的论文和所有附属的验证工件、代码和实验数据。

Q&A

Q1：多智能体AI系统中的并发异常和普通软件bug有什么区别？

A：并发异常的特别之处在于它不是代码写错了，而是多个AI在合理地各自工作时，因为时间差和共享数据互相干扰而产生的问题。普通bug在任何环境下都能重现，而并发异常只在特定的执行时序下才出现，而且通常不报错——系统认为一切正常，只是输出结果不对。这使它比普通bug更难发现，也更难修复。

Q2：L0到L4这个一致性阶梯，现实中哪些框架处于哪个台阶？

A：研究者提供了几个非正式的定位。LangGraph的默认设置基本处于L0（什么都不保证）。SagaLLM通过补偿事务机制达到了类似防止因果级联的效果，大约在L1和L2之间。Atomix在最严格配置下接近L3。CodeCRDT使用CRDT合并机制，这个方向与这条阶梯是不同的轴，所以在这个分类里被放在L0，但这不代表它质量差，只是它保证的东西是另一类。没有任何框架达到了L4。

Q3：可序列化快照隔离的8%额外成本是指每次AI调用都会多花8%吗？

A：不完全是。8%这个数字是在特定工作负载（计划-执行场景）下通过配对实验才能统计上识别出来的token开销，在其他工作负载和粗粒度的session级别比较里与零无统计差异。更准确的描述是：在低争用场景下几乎察觉不到额外成本，在高争用场景下成本与中止率线性相关，中止率低于约14%时总开销在15%以内。