多代理大型語言模型的並發異常驗證偵測與防護
為何重要
在高度並發且需維護狀態的多代理環境中，形式化驗證成為解決傳統軟體工程難以追蹤之並發邏輯錯誤的必要手段。
研究針對多代理大型語言模型系統，以形式化方法定義了四種並發異常（如 stale-generation、phantom-tool），並透過 TLA+ 與 Verus 進行機械驗證，證實了 $L_0$ 至 $L_4$ 一致性層級的可實現性。團隊在 Rust 執行時中實作了這些偵測器，成功修復了 ByteDance deer-flow 的靜默遺失更新問題，並在 LangGraph 的 ToolNode 上驗證了工具效果重排序。這為確保高複雜度代理系統的執行 正確性提供了關鍵的技術見解。