用TLA+验证修复大模型多智能体协作协议，确保高效可靠执行。
TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
- 基于任务描述生成协议结构，通过TLA+反例迭代修复。
- 48个任务全部通过验证，平均62.5%首轮成功，最多四次修复迭代。
- 显著降低死锁活锁率，适合对可靠性要求高的复杂协作场景。
我们提出TraceFix，一种面向大语言模型多智能体协调的验证优先流水线。智能体从任务描述中合成协议拓扑作为结构化中间表示（IR），生成PlusCal协调逻辑，并利用TLA+模型检查器（TLC）的反例进行迭代修复，直至验证通过。通过运行时监控拒绝非拓扑协调操作，已验证的进程体被编译为各智能体系统提示。在涵盖16种场景家族的48个任务上，所有任务均实现完整TLC验证；62.5%的任务首次即通过，无任务超过四次修复迭代。状态空间跨度达六数量级，但每个任务验证时间均低于60秒。3,456次运行对比显示，拓扑监控执行平均任务完成率达89.4%（全完成率81.5%），当模型能力下降时，使用已验证协议的运行时性能衰减仅为仅提示和仅对话基线的一半。固定运行时间内配对消融实验表明，TLC验证协议将死锁/活锁率从31.1%降至14.1%，故障注入下差异最显著。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。