エージェント型ツールプロトコルのための形式意味論：プロセス計算アプローチ

概要: 外部ツールを呼び出すことができる大規模言語モデルエージェントの登場により、エージェントプロトコルの形式的検証に対する緊急の必要が生じました。この領域では、支配的な2つのパラダイムがあります。ゼロショットAPI汎化のための研究フレームワークである「Schema-Guided Dialogue（SGD）」と、エージェントとツールの統合のための産業標準である「Model Context Protocol（MCP）」です。両者はいずれもスキーマ記述による動的なサービス発見を可能にしますが、その形式的な関係性は未検討のままです。これらのパラダイムが概念的に収束することを示した先行研究に基づき、本論文ではSGDとMCPの初めてのプロセス計算による形式化を提示し、定義された写像Phiの下でそれらが構造的に双模倣（structurally bisimilar）であることを証明します。しかし、逆写像Phi^{-1}は部分的で情報を失う（lossy）ことを示し、それによりMCPの表現力における重大なギャップを明らかにします。双方向の解析によって、完全な振る舞いの同値性のための必要十分条件として、5つの原則――意味的完全性、明示的な作用境界、失敗モードの文書化、段階的開示（progressive disclosure）との互換性、ツール間関係の宣言――を特定します。これらの原則を型システム拡張として形式化し、MCP+がSGDと同型（isomorphic）であることを証明します。本研究は、検証済みのエージェントシステムのための最初の形式的基盤を提供し、スキーマ品質を証明可能な安全性（safety）の性質として確立します。