智能体工具协议的形式语义：一种进程演算方法

能够调用外部工具的大语言模型代理的出现，迫切需要对代理协议进行形式化验证。两个范式主导了这个领域：模式引导对话 (SGD)（零样本 API 泛化的研究框架）和模型上下文协议 (MCP)（代理工具集成的行业标准）。虽然两者都通过模式描述实现动态服务发现，但它们的正式关系仍未被探索。基于先前建立这些范式概念收敛的工作，我们提出了 SGD 和 MCP 的第一个过程微积分形式化，证明它们在明确定义的映射 Phi 下在结构上是相似的。然而，我们证明反向映射 Phi^{-1} 是部分且有损的，揭示了 MCP 表达能力的关键差距。通过双向分析，我们确定了五个原则——语义完整性、明确的操作边界、故障模式文档、渐进式披露兼容性和工具间关系声明——作为完全行为等效的必要和充分条件。我们将这些原则形式化为类型系统扩展 MCP+，证明 MCP+ 与 SGD 同构。我们的工作为经过验证的代理系统提供了第一个正式基础，并将模式质量建立为可证明的安全属性。