多代理大型語言模型系統中併發異常的驗證檢測與預防
該研究針對多代理LLM系統共享狀態導致的併發異常，提出了形式化定義和驗證檢測方法。透過TLA+建模四種異常（陳舊生成、幻影工具、因果級聯、工具效應重排序），並構建了一個經機械驗證的一致性層級L0到L4。使用274個Verus驗證義務，證明了檢測器的正確性和完備性。在三個已部署的Rust執行時中實現了L0-L1級別，並對比了字節跳動deer-flow和LangGraph中的實際異常案例。
多代理大型語言模型（LLM）系統透過在記憶體儲存、向量索引和工具登錄檔之間共享狀態來協作，但這種共享可能導致併發異常，影響系統的一致性和可靠性。近期一篇發表於arXiv的論文（2606.17182）提出了一個形式化框架，用於檢測和預防這類併發異常，並提供了機械驗證的解決方案。
研究人員將多代理LLM系統中的狀態共享建模為長期執行的“讀-生成-寫”操作，並在確定性生成語義下（即持久執行引擎透過確定性重放強制執行的機制）使用TLA+形式化定義了四種併發異常：陳舊生成（stale-generation）、幻影工具（phantom-tool）、因果級聯（causal-cascade）和工具效應重排序（tool-effect reordering）。這些異常是經典隔離異常的結構化類比，每種異常都配有TLC反例。
該研究的核心貢獻是構建了一個機械驗證的一致性層級，標記為L0到L4，其中L0 ⊆ ... ⊆ L4。據作者所知，這是首個針對此類執行時系統進行機器檢查的一致性層級。透過274個Verus驗證義務（零假設、零接受，信任基礎僅為兩個結構公理和一個互斥對應關係），作者證明了檢測器相對於規格的正確性和完備性，以及每個執行時對其避免集的滿足性。
在實際部署方面，研究者提供了三個Rust執行時，分別實現L0至L1級別（悲觀鎖、可序列化快照隔離、預設SI），每個都經過陳舊生成異常驗證並精煉為其狀態機。L2至L4級別則透過執行模式驗證，並提供了無依賴的預防孿生實現（異常A3、A6、A2的檢測率分別為0/1000和1000/1000）。L2級別的實現在三個模型系列上進行了即時測試，所有120個重試會話均成功預防了A3異常。
此外，論文還重現了字節跳動deer-flow中一個靜默丟失更新的問題，並將其修復形式化為從L0到L1的精煉。同時，在LangGraph的ToolNode中展示了工具效應重排序現象，並透過L3提交順序排序器予以消除。研究者提供了完整的驗證工件，包括TLA+模型、Rust執行時、Python測試工具以及輔助附錄。
該工作的重要意義在於為多代理LLM系統的併發控制提供了形式化基礎和實用工具，有助於提升這類系統的可靠性和資料一致性。