論文の概要: Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach
- arxiv url: http://arxiv.org/abs/2603.24747v1
- Date: Wed, 25 Mar 2026 19:18:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-27 20:52:47.955757
- Title: Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach
- Title（参考訳）: エージェントツールプロトコルのための形式的意味論:プロセス計算的アプローチ
- Authors: Andreas Schlapbach,
- Abstract要約: ガイドダイアログ(SGD)とモデルコンテキストプロトコル(MCP)の2つのパラダイムがこの分野を支配している。
我々は、SGD と MCP の第一過程の定式化を行い、それらがよく定義された写像 Phi の下で構造的に両相似であることを証明した。
セマンティック完全性、明示的なアクション境界、障害モードの文書化、プログレッシブな開示互換性、およびツール間の関係宣言という5つの原則を、完全な振る舞い等価性のための必要十分条件として定義します。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: The emergence of large language model agents capable of invoking external tools has created urgent need for formal verification of agent protocols. Two paradigms dominate this space: Schema-Guided Dialogue (SGD), a research framework for zero-shot API generalization, and the Model Context Protocol (MCP), an industry standard for agent-tool integration. While both enable dynamic service discovery through schema descriptions, their formal relationship remains unexplored. Building on prior work establishing the conceptual convergence of these paradigms, we present the first process calculus formalization of SGD and MCP, proving they are structurally bisimilar under a well-defined mapping Phi. However, we demonstrate that the reverse mapping Phi^{-1} is partial and lossy, revealing critical gaps in MCP's expressivity. Through bidirectional analysis, we identify five principles -- semantic completeness, explicit action boundaries, failure mode documentation, progressive disclosure compatibility, and inter-tool relationship declaration -- as necessary and sufficient conditions for full behavioral equivalence. We formalize these principles as type-system extensions MCP+, proving MCP+ is isomorphic to SGD. Our work provides the first formal foundation for verified agent systems and establishes schema quality as a provable safety property.
- Abstract（参考訳）: 外部ツールを起動できる大規模言語モデルエージェントの出現は、エージェントプロトコルの形式的検証を緊急に必要としてきた。
ゼロショットAPIの一般化のための研究フレームワークであるSchema-Guided Dialogue(SGD)と、エージェントツール統合の業界標準であるModel Context Protocol(MCP)である。
どちらもスキーマ記述を通じて動的サービスディスカバリを可能にするが、正式な関係は未解明のままである。
これらのパラダイムの概念収束を確立する先行研究に基づいて、SGD と MCP の形式化を初めて行い、よく定義された写像 Phi の下で構造的に両相似であることを証明した。
しかし, 逆写像 Phi^{-1} は部分的かつ損失的であり, MCP の表現性に重要なギャップがあることが示される。
双方向分析を通じて、動作の完全性、明示的な動作境界、障害モードの文書化、プログレッシブな開示互換性、およびツール間の関係宣言という5つの原則を、完全な振る舞い等価性に必要な十分な条件として識別する。
我々はこれらの原理をタイプシステム拡張 MCP+ として定式化し、 MCP+ が SGD に同型であることを証明する。
我々の研究は、検証されたエージェントシステムのための最初の公式な基盤を提供し、証明可能な安全特性としてスキーマ品質を確立する。
関連論文リスト
- The Auton Agentic AI Framework [5.410458076724158]
人工知能の分野では、ジェネレーティブAIからエージェントAIへの移行が進行中である。
大規模言語モデル(LLM)は構造化されていない出力を生成するが、それらが制御しなければならないバックエンドインフラストラクチャは決定論的でスキーマに適合する入力を必要とする。
本稿では,自律エージェントの作成,作成,管理を行うための原則アーキテクチャであるAuton Agentic AI Frameworkについて述べる。
論文 参考訳（メタデータ） (2026-02-27T06:42:08Z) - The Convergence of Schema-Guided Dialogue Systems and the Model Context Protocol [0.0]
本稿では、互換性誘導対話(SGD)とモデルコンテキストプロトコル(MCP)の基本的な収束性を確立する。
SGD と MCP は、決定論的で監査可能な LLM-エージェント相互作用のための統一パラダイムの2つの現れを表す。
論文 参考訳（メタデータ） (2026-02-21T09:02:35Z) - Ontology-to-tools compilation for executable semantic constraint enforcement in LLM agents [0.0]
本稿では,大規模言語モデル(LLM)と形式的ドメイン知識意味論を結合する原理実証機構を提案する。
オントロジー仕様は、LLMベースのエージェントが知識グラフインスタンスの作成と修正に使用する実行可能なツールツールにコンパイルされる。
本稿では, LLM インタフェースの有効性, マニュアルスキーマの削減, エンジニアリングの促進, フォーマルな知識を生成システムに組み込むための一般的なパラダイムの確立について述べる。
論文 参考訳（メタデータ） (2026-02-03T12:03:26Z) - Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
汎用エージェントをドメインエキスパートに変換するフレームワークであるALITA-Gを提案する。
このフレームワークでは、ジェネラリストエージェントが対象ドメインタスクのキュレートされたスイートを実行する。
計算コストを削減しながら、大きな利益を得ることができます。
論文 参考訳（メタデータ） (2025-10-27T17:59:14Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。
これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
論文 参考訳（メタデータ） (2025-09-28T06:32:14Z) - ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMs [54.154593699263074]
ProtoReasoningは、大規模推論モデルの推論能力を高めるフレームワークである。
ProtoReasoningは問題を対応するプロトタイプ表現に変換する。
ProtoReasoningは論理的推論に基づくベースラインモデルよりも4.7%改善されている。
論文 参考訳（メタデータ） (2025-06-18T07:44:09Z) - Guiding the PLMs with Semantic Anchors as Intermediate Supervision:
Towards Interpretable Semantic Parsing [57.11806632758607]
本稿では,既存の事前学習言語モデルを階層型デコーダネットワークに組み込むことを提案する。
第一原理構造をセマンティックアンカーとすることで、2つの新しい中間管理タスクを提案する。
いくつかのセマンティック解析ベンチマークで集中的な実験を行い、我々のアプローチがベースラインを一貫して上回ることを示す。
論文 参考訳（メタデータ） (2022-10-04T07:27:29Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。