Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

Dit artikel introduceert een proceskalkulusformalisatie die de structurele bisimilariteit tussen Schema-Guided Dialogue en het Model Context Protocol aantoont, terwijl het ook de beperkte expressiviteit van MCP blootlegt en een uitgebreide variant (MCP+) presenteert die volledig equivalent is aan SGD om formele verificatie van agent-systemen mogelijk te maken.

De kern

Stel je voor dat je een zeer slimme, maar soms wat ongeduldige assistent hebt: een AI-agent. Deze assistent kan heel veel doen, zoals banktransacties regelen of vluchten boeken. Maar om dat te doen, moet hij praten met andere computersystemen (de "gereedschappen" of tools).

Het probleem is: hoe weet je zeker dat deze assistent de regels volgt? Dat hij eerst zijn saldo checkt voordat hij geld overmaakt? En dat hij niet per ongeluk een verkeerde knop indrukt?

Dit artikel, geschreven door Andreas Schlapbach, probeert dit probleem op te lossen door een wiskundig taal te gebruiken die we "proces-calculus" noemen. Laten we dit uitleggen met een paar simpele metaforen.

1. Twee talen voor één doel

Er zijn momenteel twee grote manieren om AI-assistenten te laten praten met computersystemen:

• SGD (Schema-Guided Dialogue): Dit is als een ouderwets, maar zeer gedetailleerd script voor een toneelstuk. Alles staat er precies in beschreven: welke woorden je mag zeggen, in welke volgorde, en wat er gebeurt als je een fout maakt. Het is heel veilig, maar soms wat star.
• MCP (Model Context Protocol): Dit is de nieuwe, flexibele standaard van de industrie. Het is als een moderne app-store voor AI. Je kunt nieuwe tools "downloaden" en direct gebruiken zonder de hele assistent opnieuw te leren. Het is flexibel, maar soms mist het de strenge veiligheidsregels van het oude script.

De vraag is: Zijn deze twee systemen eigenlijk hetzelfde? Kunnen we bewijzen dat ze precies hetzelfde doen?

2. De Wiskundige Vertaler (De "Φ"-functie)

De auteur heeft een wiskundige vertaler bedacht (noem hem Phi).

• Als je een oud script (SGD) aan Phi geeft, kan hij het omzetten naar een moderne app-omschrijving (MCP).
• Het goede nieuws: Dit werkt perfect! Als je een veilig script omzet, krijg je een veilige app-omschrijving. Ze zijn "bisimilar", wat in deze taal betekent dat ze zich precies hetzelfde gedragen.

3. Het Grootste Probleem: De "Verlies" bij het Terugvertalen

Maar hier komt de twist. Als je de moderne app-omschrijving (MCP) terug probeert te vertalen naar het oude script (SGD), gaat er informatie verloren.

Stel je voor dat je een recept (MCP) hebt dat zegt: "Kook de pasta."

• Het oude script (SGD) zou zeggen: "Kook de pasta, maar wacht eerst tot de waterkoker piept en check of je geen allergieën hebt."
• De moderne versie (MCP) zegt alleen: "Kook de pasta."

De vertaler (Phi) kan de instructie "Kook de pasta" wel omzetten, maar hij kan de geheime veiligheidsinstructies (wacht op piepen, check allergieën) niet terugvinden in de moderne tekst. Die informatie is "verloren" gegaan.

Dit betekent dat de moderne standaard (MCP) op zichzelf niet veilig genoeg is om complexe taken te regelen zonder dat je extra regels toevoegt.

4. De Oplossing: Vijf Nieuwe Regels (MCP+)

Om de moderne wereld (MCP) net zo veilig en betrouwbaar te maken als het oude script (SGD), stelt de auteur vijf nieuwe regels voor. Hij noemt dit MCP+.

Laten we deze regels vergelijken met het regelen van een groot bankfeest:

1. Betekenisvolle Beschrijvingen (Semantic Completeness):

   • Vroeger: "Voer hier een naam in."
   • Nu: "Voer hier de naam in van de gast, bijvoorbeeld 'Jan' of 'Maria', zodat we de uitnodiging kunnen sturen."
   • Metafoor: Geef niet alleen de vorm, maar vertel ook waarom je het nodig hebt.

2. Duidelijke Grenzen voor Acties (Explicit Action Boundaries):

   • Vroeger: De AI doet gewoon wat hij moet doen.
   • Nu: Als een actie gevaarlijk is (zoals geld overmaken of een bestand wissen), moet de AI eerst om toestemming vragen.
   • Metafoor: Je mag de sleutel van de kluis niet gebruiken zonder dat de directeur eerst "Ja" zegt.

3. Plannen voor Fouten (Failure Mode Documentation):

   • Vroeger: Als het misgaat, crasht de AI.
   • Nu: De AI moet van tevoren zeggen: "Als de server uitvalt, probeer ik het 3 keer opnieuw. Als dat niet lukt, vraag ik de gebruiker om hulp."
   • Metafoor: Een brandverzekering. Wat doe je als het vuur uitbreekt?

4. Progressieve Ontsluiting (Progressive Disclosure):

   • Vroeger: De AI moet de hele handleiding lezen om één ding te doen.
   • Nu: De AI krijgt eerst een korte samenvatting ("Dit is een zoekfunctie"). Pas als hij die gaat gebruiken, krijgt hij de volledige, lange handleiding.
   • Metafoor: Een menukaart. Eerst zie je de hoofdgerechten, pas als je kiest, zie je de ingrediëntenlijst. Dit bespaart tijd en ruimte.

5. Relaties tussen Gereedschappen (Inter-Tool Relationship):

   • Vroeger: De AI weet niet welke knop hij eerst moet indrukken.
   • Nu: De AI weet: "Ik kan pas 'Betaling' doen als ik eerst 'Bestelling' heb gedaan."
   • Metafoor: Je kunt geen huis bouwen zonder eerst de fundering te leggen. De regels zeggen dit expliciet.

5. Het Eindresultaat: Veiligheid als Wiskunde

Door deze vijf regels toe te voegen aan de moderne standaard (MCP+), wordt het systeem wiskundig gelijkwaardig aan het oude, veilige script (SGD).

Wat betekent dit voor de gewone mens?

• Vertrouwen: We kunnen nu wiskundig bewijzen dat een AI-assistent geen fouten maakt in zijn volgorde van handelingen.
• Veiligheid: We kunnen garanderen dat een AI nooit geld overmaakt zonder toestemming, of nooit een bestand wist zonder check.
• Toekomst: Omdat AI's steeds meer taken overnemen (van ziekenhuizen tot treinen), is dit soort "wiskundige garantie" essentieel. Het zorgt ervoor dat we niet blindelings vertrouwen op een slimme computer, maar dat we kunnen verifiëren dat hij veilig werkt.

Kort samengevat:
De auteur heeft ontdekt dat de nieuwe, flexibele manier om AI's te laten werken (MCP) een paar belangrijke veiligheidsregels mist die de oude manier (SGD) wel had. Door vijf simpele, maar krachtige regels toe te voegen, kunnen we de nieuwe manier net zo veilig maken als de oude. Hierdoor kunnen we in de toekomst met een gerust hart AI's laten regelen wat er echt toe doet.

Technische samenvatting

Titel: Formele Semantiek voor Agentische Tool-protocollen: Een Procescalculus Benadering

1. Het Probleem

De snelle opkomst van Large Language Model (LLM) agents die externe tools kunnen aanroepen, heeft een kritieke kloof gecreëerd in de beveiliging en betrouwbaarheid van systemen. Hoewel deze agents complexe workflows kunnen orchestreren, ontbreken er formele methoden om hun correctheid, veiligheid en gedragskenmerken te verifiëren.

Twee dominante paradigma's voor de integratie van agents en tools zijn:

1. Schema-Guided Dialogue (SGD): Een onderzoeksframework dat dialogue-modellen in staat stelt om zero-shot generalisatie naar nieuwe API's te bereiken via natuurlijke taal-schema's.
2. Model Context Protocol (MCP): Een industriestandaard (geïntroduceerd door Anthropic) die N-naar-M integratie mogelijk maakt via gestandaardiseerde primitieven (Tools, Resources, Prompts).

Hoewel beide paradigma's conceptueel convergeren rondom schema-ontwerp, is hun formele relatie onbekend. Bestaande aanpakken vertrouwen op testen (onvolledige dekking), prompt-engineering (geen garanties) of menselijke review (niet schaalbaar). Er is behoefte aan een wiskundige basis om te bewijzen dat agents veilig opereren en dat protocollen equivalent zijn.

2. Methodologie

De auteur hanteert een procescalculus-benadering, specifiek gebaseerd op de $\pi$-calculus, om de semantiek van SGD en MCP te formaliseren.

• Formalisatie: Zowel SGD als MCP worden gemodelleerd als communicerende processen met gedefinieerde syntaxis, operationele semantiek en gelabelde transitiestelsels (LTS).
  • SGD-processen omvatten intenties, slot-collectie en uitvoering.
  • MCP-processen omvatten tool-definities, resources, prompts en initialisatie.
• Bisimulatie: De kern van de analyse ligt in het bewijzen van sterke bisimulatie ($\sim$). Dit is een gedragsvergelijkende relatie die waarborgt dat twee systemen ononderscheidbaar zijn voor een externe waarnemer.
• Mapping Functies:
  • $\Phi$: Een mapping van SGD naar MCP.
  • $\Phi^{-1}$: Een reverse mapping van MCP naar SGD.
• Type-systemen: De analyse leidt tot de introductie van een uitgebreid type-systeem (MCP+) om gaten in expressiviteit op te vullen.

3. Belangrijkste Bijdragen

1. Eerste Formele Semantiek: Definities van de syntaxis en operationele semantiek voor zowel SGD als MCP binnen de $\pi$-calculus.
2. Bisimulatiebewijs (SGD $\sim$ MCP): Bewijs dat SGD en MCP structureel en gedragsmatig equivalent zijn onder een goed gedefinieerde mapping $\Phi$.
3. Gatenanalyse (Reverse Mapping): Het aantonen dat de reverse mapping $\Phi^{-1}$ partiëel en verliesrijk is. MCP mist essentiële metadata die in SGD aanwezig is, zoals transactievlaggen en expliciete foutbehandeling.
4. De Vijf Principes: Identificatie van vijf noodzakelijke en toereikende voorwaarden voor volledige gedrags-equivalentie:
   1. Semantische volledigheid: Beschrijvingen moeten uitleggen waarom parameters bestaan, niet alleen hun type.
   2. Expliciete actie-grenzen: Tools moeten signaleren of ze bijwerkingen (side-effects) hebben en goedkeuring vereisen.
   3. Documentatie van faalmodi: Expliciete enumeratie van foutcondities en herstelstrategieën.
   4. Compatibiliteit met progressieve onthulling: Ondersteuning voor samenvattingen om token-kosten te verlagen.
   5. Verklaring van inter-tool relaties: Expliciete declaratie van afhankelijkheden tussen tools.
5. MCP+ en Volledige Equivalentie: De introductie van MCP+, een uitgebreide calculus die de vijf principes integreert als type-systeem extensies. Hiermee wordt bewezen dat MCP+ $\cong$ SGD (volledige bijectie).
6. Veiligheidseigenschappen: Formele bewijzen voor proces-invarianten zoals capability confinement (toegang beperken), voorkomen van tool-vergiftiging (prompt injection) en correcte volgorde van goedkeuringen en afhankelijkheden.

4. Resultaten

• Structurale Equivalentie: Het is bewezen dat een SGD-intentie en een MCP-tool onder $\Phi$ dezelfde transities doorlopen (invoke $\approx$ call, execute $\approx$ execute, etc.).
• Expressiviteitskloof: De analyse toont aan dat standaard MCP strikt minder expressief is dan SGD omdat het geen machine-leesbare vlaggen heeft voor transacties (is_transactional) en geen primitieven voor passieve context (Resources) of workflow-sjablonen (Prompts) kent die direct naar SGD-intenties kunnen worden gemapt zonder informatieverlies.
• Oplossing via MCP+: Door de vijf principes toe te passen, wordt MCP+ gecreëerd. In dit systeem is de mapping $\Phi^+$ een volledige bijectie, wat betekent dat er geen informatie verloren gaat bij het converteren tussen de twee protocollen.
• Veiligheidsgaranties:
  • Capability Confinement: Kanalen voor credentials blijven binnen hun scope.
  • Tool Poisoning: Door type-systemen wordt voorkomen dat beschrijvingen als uitvoerbare code worden behandeld.
  • Volgorde: Het systeem garandeert dat goedkeuringen plaatsvinden vóór uitvoering van schrijvende acties en dat afhankelijkheden (bijv. "bestelling maken" vóór "betalen") correct worden gevolgd.

5. Betekenis en Impact

Dit werk legt de wiskundige fundamenten voor verifieerbare agent-systemen. Het transformeert agent-protocollen van ad-hoc conventies naar systemen met bewezen veiligheidseigenschappen.

• Schaalbaarheid en Veiligheid: Voor kritieke toepassingen zoals financiële transacties, gezondheidszorg en infrastructuurmanagement is het niet langer voldoende om te vertrouwen op testen; formele verificatie is noodzakelijk.
• Software 3.0: De convergentie van SGD en MCP, ondersteund door deze formele semantiek, markeert de opkomst van "Software 3.0", waar autonome agents dynamisch capaciteiten ontdekken en orchestreren via gestandaardiseerde, machine-leesbare interfaces.
• Toekomstige Richtingen: De paper schetst paden voor geautomatiseerde bewijzen (met tools zoals Isabelle/HOL), probabilistische bisimulatie voor LLM-stochasticiteit, en model-checking voor temporele veiligheid.

Kortom, het artikel biedt een theoretisch raamwerk om de veiligheid en betrouwbaarheid van de volgende generatie AI-agents te garanderen door schema-kwaliteit om te zetten in een bewijsbaar type-systeem.