Autoformalization of Agent Instructions into Policy-as-Code

Technische Samenvatting: Autoformalizatie van Agentinstructies naar Policy-as-Code

Probleemstelling
De inzet van autonome Large Language Model (LLM) agents in domeinen met een hoog risico (bijv. de gezondheidszorg) brengt een kritieke beveiligingsafweging met zich mee: agents hebben verhoogde privileges nodig om complexe taken uit te voeren, maar deze privileges vergroten het aanvalsoppervlak voor adversariële technieken zoals prompt injection. De huidige industriële praktijken vertrouwen zwaar op probabilistische guardrails, zoals gefinetunede veiligheidsklassificaties (bijv. Llama Guard) of prompt-gebaseerde sturing. Hoewel deze methoden enige bruikbaarheid bieden, missen ze formele garanties en zijn ze vaak ontoereikend voor beveiligingskritische toepassingen waar deterministische handhaving vereist is. Daartegenover staat handmatig gecodeerde symbolische handhaving, die weliswaar formele garanties biedt, maar niet schaalbaar is naar de breedte en complexiteit van realistische beleidsspecificaties.

Methodologie
De auteurs stellen een autoformalisatie-pipeline voor die natuurlijke taal agentinstructies, Model Context Protocol (MCP) toolbeschrijvingen en beleidsdocumenten vertaalt naar formeel geverifieerde policies geschreven in de Cedar Policy Language. Deze pipeline werkt via een generator-critic loop gestructureerd als een "Verification Sandwich" met drie afzonderlijke lagen:

1. De Grounding Layer (Onderste laag): Deze laag legt de basis door entiteiten te extraheren, tool-schema's te identificeren (bijv. OpenAI JSON-schema's) en een principal-resource-action ontologie te definiëren. Het zorgt ervoor dat de agent opereert binnen een gestructureerde omgeving waar potentiële acties mappen naar real-world entiteiten en geldige systeem-identifiers. Cruciaal is dat deze laag programmatisch een Cedar-schema genereert vanuit MCP tool-definities om te dienen als een strikt type-control mechanisme.
2. De Model Layer (Middelste laag): Door gebruik te maken van state-of-the-art LLM's interpreteert deze laag instructies in natuurlijke taal en genereert het kandidaat-policy sets. Het maakt gebruik van parametrische kennis om policies voor te stellen die de beoogde agent-logica weerspiegelen.
3. De Safety Layer (Bovenste laag): Deze laag gebruikt een dual-critic mechanisme om kandidaten te valideren:
   • Hard Critic: Een deterministische, programmatische controle met behulp van de ingebouwde statische analyse-tools van Cedar. Het verifieert syntaxis, handhaaft schema-compliance en detecteert logische tegenstrijdigheden (bijv. vacuüm-policies of conflicterende regels).
   • Soft Critic: Een LLM-as-a-judge die kandidaten evalueert op basis van een semantische alignment met een vooraf gedefinieerde rubric. Het zorgt ervoor dat de formele logica nauwkeurig de geest van de oorspronkelijke instructies in natuurlijke taal en beleidsdocumenten weerspiegelt.

De loop iterreert door feedback van beide critics terug te voeren naar de generator totdat de policy set zowel de harde als de soft checks doorstaat. De resulterende policies worden tijdens runtime afgedwongen door een externe, deterministische policy engine, waardoor de veiligheidslogica wordt ontkoppeld van de redeneercontext van de LLM.

Belangrijkste Bijdragen

• Verification Sandwich Architectuur: Een innovatieve gelaagde aanpak voor autoformalizatie die grounding, generatieve redenering en dual-mode verificatie (hard/soft) combineert om ongestructureerd beleid naar formele code te vertalen.
• Open-Source Implementatie: De release van een open-source policy harness voor agent scaffolds geïmplementeerd in Cedar, inclusief aangepaste Python bindings.
• Schaalbare Autoformalizatie: Een pipeline die automatisch agent cards (instructies + tool-schema's) omzet in geverifieerde autorisatie-policies, waarmee de schaalbaarheidsbeperkingen van handmatige symbolische handhaving worden aangepakt.
• Evaluatieframework: Een rigoureuze evaluatie op de MedAgentBench benchmark, waarbij de autoformaliseerde aanpak wordt vergeleken met eerdere hand-gecodeerde symbolische guardrails.

Resultaten
Het systeem werd geëvalueerd op MedAgentBench, een benchmark voor tool-gebruikende elektronische medische dossier (EMR) agents. De studie vergeleek drie condities: Raw HTTP tools, een Baseline met getypeerde MCP tools, en een Guardrail conditie die gebruik maakt van de door de auteurs ontwikkelde Cedar policies versus de hand-gecodeerde symbolische guardrails van Hong et al.

• Dekking: De autoformalisatie-pipeline dekte substantieel meer van de bron 88-regel natuurlijke taal specificatie dan de hand-gecodeerde aanpak, die slechts 23 regels implementeerde.
• Blokkeringspercentages: In de "Guardrail" conditie blokkeerde de Cedar policy engine een significant hoger percentage beleidsschendingen vergeleken met de hand-gecodeerde baseline, met name in adversariële scenario's.
  • Op de Original dataset blokkeerde Cedar 55,7% van de trajecten (167/300), terwijl de hand-gecodeerde guardrails 0% blokkeerden (door constructie, aangezien zij slechts een subset van de regels dekten).
  • Op de Adversarial dataset blokkeerde Cedar 85,7% van de trajecten (42/49).
• Analyse van Schrijfpogingen: Wanneer er gefilterd werd op trajecten die daadwerkelijke schrijfacties (POST requests) bevatten, benaderde de Cedar blokkeer-rate 100% (bijv. 100,0% in de Adversarial Guardrail conditie), wat aantoont dat het systeem ongeautoriseerde datamodificaties effectief voorkomt wanneer deze plaatsvinden.
• Robuustheid: Het systeem voorkwam succesvol "jailbreaking" en indirecte prompt injection door regels af te dwingen buiten de context window van de LLM.

Significantie en Claims
Het artikel claimt dat deze aanpak sterke formele garanties biedt over het gedrag van de agent, een capaciteit die ontbreekt bij probabilistische guardrails. Door de handhaving van beleid te ontkoppelen van de redeneercontext van de LLM, mitigeert de architectuur het risico dat een aanvaller de beveiligingslaag ervan overtuigt de regels te negeren. Het gebruik van Cedar zorgt ervoor dat policies menselijk leesbaar, auditeerbaar en formeel geverifieerd zijn, waardoor de kloof tussen de flexibiliteit van natuurlijke taal en de strengheid van symbolische logica wordt overbrugd.

De auteurs erkennen een "friction-utility trade-off", waarbij zij opmerken dat overly restrictieve policies de nuttigheid van de agent kunnen verminderen. Zij stellen dat de Generator-Critic Loop, in het bijzonder de inclusie van een soft critic, essentieel is voor het bereiken van een "Goldilocks zone" waar agents voldoende beperkt zijn maar toch functioneel blijven. Het werk demonstreert dat autoformalizatie de mogelijkheid biedt om beleidshandhaving te schalen naar complexe, real-world specificaties zonder de formele garanties op te offeren die vereist zijn voor domeinen met een hoog risico.

Beperkingen en Toekomstig Werk
De auteurs merken op dat Cedar per ontwerp stateless is, wat de mogelijkheid beperkt om multi-turn workflows te hanteren die afhankelijk zijn van de volgorde van acties of persistente context. Toekomstig werk beoogt dit aan te pakken door temporele logica te integreren voor prerequisite sequenties en door het ontwikkelen van memory-aware policies die de engine in staat stellen de historie van een agent-traject te refereren.