TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
作者: Shuren Xia, Qiwei Li, Taqiya Ehsan, Jorge Ortiz
分类: cs.AI, cs.MA
发布日期: 2026-05-08
💡 一句话要点
提出TraceFix框架：利用TLA+模型检测与反例反馈实现多智能体协作协议的自动修复与验证
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 多智能体系统 形式化验证 TLA+ 大语言模型 协议合成 运行时监控 逻辑鲁棒性
📋 核心要点
- 现有LLM多智能体协作缺乏形式化验证，导致在复杂交互中极易出现死锁、活锁及逻辑错误，难以保证系统可靠性。
- TraceFix引入“验证优先”范式，通过TLA+模型检测器生成反例，驱动LLM迭代修复协调协议，确保逻辑的正确性与鲁棒性。
- 实验证明该方法在保证验证效率的同时，显著提升了任务完成率，并有效降低了复杂环境下的死锁与活锁发生概率。
📝 摘要（中文）
本文介绍了TraceFix，这是一个针对大语言模型（LLM）多智能体协作的验证优先流水线。该系统首先根据任务描述将协议拓扑合成为结构化中间表示（IR），随后生成PlusCal协调逻辑，并利用TLA+模型检测器（TLC）提供的反例进行迭代修复，直至协议通过验证。验证后的逻辑被编译为智能体系统提示词，并在运行时监控下执行，以拒绝违规操作。在涵盖16个场景系列的48项任务中，所有任务均实现了完全的TLC验证，且62.5%的任务一次性通过，修复迭代次数不超过四次。尽管状态空间跨越六个数量级，所有任务的验证时间均在60秒内。实验表明，拓扑监控执行在任务完成率上表现最优（平均89.4%），且在模型能力下降时，其性能衰减率仅为基线方法的一半。消融实验显示，TLC验证协议将死锁/活锁率从31.1%显著降低至14.1%。
🔬 方法详解
问题定义：论文旨在解决大语言模型在多智能体协作中协议逻辑不可靠的问题。现有方法依赖提示词工程，缺乏对协作协议的形式化约束，导致在面对复杂任务或故障注入时，智能体极易陷入死锁或活锁状态。
核心思路：引入形式化验证工具TLA+作为“外部监督者”。通过将LLM生成的协议逻辑转化为PlusCal代码，利用TLC模型检测器进行穷尽式状态空间搜索，并利用产生的反例（Counterexamples）反馈给LLM进行针对性修复，从而实现协议的“正确性构造”。
技术框架：系统包含三个核心阶段：1. 协议合成：LLM根据任务描述生成拓扑结构IR；2. 迭代验证：将IR转换为PlusCal，通过TLC检测并根据反例反馈迭代修复；3. 运行时监控：将验证后的逻辑编译为系统提示词，并部署运行时监控器，强制执行拓扑约束，拦截非法操作。
关键创新：将形式化验证与LLM生成式工作流深度集成，通过反例驱动的闭环反馈机制，解决了LLM在逻辑推理上的不确定性，实现了从“概率性生成”到“确定性验证”的跨越。
关键设计：采用PlusCal作为中间语言以降低TLA+的使用门槛；运行时监控器通过预定义的拓扑约束，确保智能体在执行过程中不会偏离已验证的协议路径，从而在模型能力受限时仍能维持系统稳定性。
🖼️ 关键图片
📊 实验亮点
TraceFix在48项任务中实现了100%的TLC验证通过率，验证过程均在60秒内完成。对比基线，其任务完成率达到89.4%，在故障注入场景下，死锁/活锁率从31.1%大幅下降至14.1%。此外，该方法在模型能力下降时表现出极强的鲁棒性，性能衰减速度仅为传统提示词方法的一半。
🎯 应用场景
该研究适用于对可靠性要求极高的多智能体系统，如自动化供应链管理、分布式机器人协作、复杂软件工程自动化及多智能体金融交易系统。其核心价值在于通过形式化方法为LLM赋能，使其能够胜任需要严格逻辑一致性的工业级任务，显著降低系统故障风险。
📄 摘要（原文）
We present TraceFix, a verification-first pipeline for Large Language Model (LLM) multi-agent coordination. An agent synthesizes a protocol topology as a structured intermediate representation (IR) from a task description, generates PlusCal coordination logic, and iteratively repairs the protocol using counterexamples from the TLA+ model checker (TLC) until verification succeeds. Verified process bodies are compiled into per-agent system prompts and executed under a runtime monitor that rejects out-of-topology coordination operations. On 48 tasks spanning 16 scenario families, all tasks reach full TLC verification; 62.5% pass on the first attempt and none requires more than four repair iterations. State spaces span six orders of magnitude yet verification completes in under 60 s for every task. A 3,456-run runtime comparison shows that topology-monitored execution achieves the highest task completion (89.4% average, 81.5% full) and that runtimes using the verified protocol degrade at roughly half the rate of prompt-only and chat-only baselines when model capability is reduced. A paired ablation under a fixed runtime shows that TLC-verified protocols cut deadlock/livelock (DL/LL) from 31.1% to 14.1%, with the largest separation under fault injection.