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

本文针对多智能体 LLM 系统通过共享存储、向量索引等机制共享状态时产生的并发异常问题展开研究。作者将此类共享建模为长周期的读 - 生成 - 写操作，并在 TLA+ 中形式化了四种并发异常。通过机械验证构建了最大一致性层级链，证明了检测器的完备性。研究在 Rust 运行时中实现了不同层级的隔离机制，成功复现并修复了现有框架中的静默更新丢失及工具效应重排序问题，为多智能体系统的记忆一致性提供了首个机器验证的保障。