摘要
大语言模型智能体调用外部工具的需求催生了对协议形式验证的迫切需求。本文针对模式引导对话（SGD）与模型上下文协议（MCP）两种主流范式，首次提出进程演算形式化描述，证明二者在特定映射下结构互模拟。研究揭示 MCP 反向映射存在信息丢失，指出其表达能力缺陷，并提炼出五项原则作为行为等价充要条件。通过扩展类型系统提出 MCP+，证明其与 SGD 同构，为可验证智能体系统奠定理论基础，确立模式质量为可证明的安全属性。
AI 推荐理由
论文聚焦智能体工具调用协议的语义形式化，直接定义工具交互规范与能力边界。
研究机构
SBB (Swiss Federal Railways), SBB IT, Bern, Switzerland
论文信息