Autoformalization of Agent Instructions into Policy-as-Code

Technisches Resümee: Autoformalisierung von Agenten-Instruktionen in Policy-as-Code

Problemstellung
Der Einsatz autonomer Large Language Model (LLM)-Agenten in hochsensiblen Bereichen (z. B. dem Gesundheitswesen) stellt einen kritischen Sicherheitskompromiss dar: Agenten benötigen erhöhte Privilegien, um komplexe Aufgaben auszuführen, doch diese Privilegien vergrößern die Angriffsfläche für adversarielle Techniken wie Prompt Injection. Die derzeitige Branchenpraxis stützt sich stark auf probabilistische Leitplanken (Guardrails), wie etwa feinabgestimmte Sicherheitsklassifikatoren (z. B. Llama Guard) oder promptbasierte Steuerung. Während diese Methoden einen gewissen Nutzen bieten, mangelt es ihnen an formalen Garantien und sie sind oft unzureichend für sicherheitskritische Anwendungen, bei denen eine deterministische Durchsetzung erforderlich ist. Umgekehrt bietet die handkodierte symbolische Durchsetzung zwar formale Garantien, kann jedoch nicht mit der Breite und Komplexität realer Richtlinienspezifikationen skalieren.

Methodik
Die Autoren schlagen eine Autoformalisierungs-Pipeline vor, die natürliche Sprachinstruktionen für Agenten, Model Context Protocol (MCP) Tool-Beschreibungen und Richtliniendokumente in formal verifizierte Richtlinien übersetzt, die in der Cedar Policy Language geschrieben sind. Diese Pipeline operiert über eine Generator-Critic-Schleife, die als „Verification Sandwich“ mit drei distinkten Schichten strukturiert ist:

1. Die Grounding-Schicht (Unten): Diese Schicht bildet das Fundament, indem sie Entitäten extrahiert, Tool-Schemata (z. B. OpenAI JSON-Schemas) identifiziert und eine Principal-Resource-Action-Ontologie definiert. Sie stellt sicher, dass der Agent innerhalb einer strukturierten Umgebung agiert, in der potenzielle Aktionen auf reale Entitäten und gültige System-Identifikatoren abgebildet werden. Entscheidend ist, dass sie programmatisch ein Cedar-Schema aus den MCP-Tool-Definitionen generiert, um als strenger Typprüfungsmechanismus zu dienen.
2. Die Modell-Schicht (Mitte): Unter Verwendung modernster LLMs interpretiert diese Schicht natürliche Sprachinstruktionen und generiert Kandidaten-Richtliniensätze. Sie nutzt parametrisches Wissen, um Richtlinien vorzuschlagen, die die beabsichtigte Agentenlogik widerspiegeln.
3. Die Sicherheits-Schicht (Oben): Diese Schicht verwendet einen dualen Critic-Mechanismus, um Kandidaten zu validieren:
   • Hard Critic: Eine deterministische, programmatische Prüfung mittels Cedars integrierter statischer Analyse-Tools. Sie verifiziert die Syntax, erzwingt die Einhaltung des Schemas und erkennt logische Widersprüche (z. B. vadose Richtlinien oder konfliktierende Regeln).
   • Soft Critic: Ein LLM-as-a-judge, der die semantische Übereinstimmung anhand einer vordefinierten Rubrik bewertet. Er stellt sicher, dass die formale Logik tatsächlich den Geist der ursprünglichen natürlichen Sprachinstruktionen und Richtliniendokumente widerspiegelt.

Die Schleife iteriert, indem sie Feedback von beiden Critics an den Generator zurückführt, bis der Richtliniensatz sowohl die Hard- als auch die Soft-Checks besteht. Die resultierenden Richtlinien werden zur Laufzeit durch eine externe, deterministische Policy-Engine durchgesetzt, wodurch die Sicherheitslogik vom Reasoning-Kontext des LLMs entkoppelt wird.

Wesentliche Beiträge

• Verification Sandwich Architektur: Ein neuartiger geschichteter Ansatz zur Autoformalisierung, der Grounding, generatives Reasoning und duale Verifizierung (Hard/Soft) kombiniert, um unstrukturierte Richtlinien in formalen Code zu übersetzen.
• Open-Source-Implementierung: Die Veröffentlichung eines Open-Source Policy Harness für Agent-Scaffolds, implementiert in Cedar, einschließlich benutzerdefinierter Python-Bindings.
• Skalierbare Autoformalisierung: Eine Pipeline, die Agent Cards (Instruktionen + Tool-Schemata) automatisch in verifizierte Autorisierungsrichtlinien konvertiert und damit die Skalierbarkeitsbeschränkungen manueller symbolischer Durchsetzung adressiert.
• Evaluations-Framework: Eine rigorose Evaluierung auf dem MedAgentBench Benchmark, die den autoformalisierten Ansatz mit bisherigen handkodierten symbolischen Guardrails vergleicht.

Ergebnisse
Das System wurde auf MedAgentBench evaluiert, einem Benchmark für tool-nutzende Electronic Medical Record (EMR) Agenten. Die Studie verglich drei Bedingungen: Raw HTTP Tools, eine Baseline mit typisierten MCP-Tools sowie eine Guardrail-Bedingung unter Verwendung der von den Autoren entwickelten Cedar-Richtlinien gegenüber den handkodierten symbolischen Guardrails von Hong et al.

• Abdeckung (Coverage): Die autoformalisierte Pipeline deckte einen wesentlich größeren Teil der ursprünglichen 88-Regel-Naturlsprachspezifikation ab als der handkodierte Ansatz, welcher lediglich 23 Regeln implementierte.
• Blockierraten (Blocking Rates): In der „Guardrail“-Bedingung blockierte die Cedar Policy Engine einen signifikant höheren Prozentsatz an Richtlinienverstößen im Vergleich zur handkodierten Baseline, insbesondere in adversariellen Szenarien.
  • Auf dem Original-Datensatz blockierte Cedar 55,7 % der Trajektorien (167/300), während die handkodierten Guardrails 0 % blockierten (konstruktionsbedingt, da sie nur eine Teilmenge der Regeln abdeckten).
  • Auf dem Adversarial-Datensatz blockierte Cedar 85,7 % der Trajektorien (42/49).
• Analyse der Schreibversuche (Write-Attempt Analysis): Bei Filterung der Trajektorien auf tatsächliche Schreibversuche (POST-Requests) näherte sich die Cedar-Blockrate 100 % (z. B. 100,0 % in der Adversarial Guardrail Bedingung), was zeigt, dass das System unbefugte Datenänderungen effektiv verhindert, wenn diese auftreten.
• Robustheit: Das System verhinderte erfolgreich „Jailbreaking“ und indirekte Prompt Injection, indem es Regeln außerhalb des Kontextfensters des LLMs durchsetzte.

Bedeutung und Ansprüche
Das Paper behauptet, dass dieser Ansatz starke formale Garantien über das Verhalten von Agenten bietet – eine Fähigkeit, die probabilistischen Guardrails fehlt. Durch die Entkopplung der Richtliniendurchsetzung vom Reasoning-Kontext des LLM minimiert die Architektur das Risiko, dass ein Angreifer die Sicherheitsschicht davon überzeugt, ihre Regeln zu ignorieren. Die Verwendung von Cedar stellt sicher, dass Richtlinien menschenlesbar, auditierbar und formal verifiziert sind, wodurch die Lücke zwischen der Flexibilität natürlicher Sprache und der Strenge symbolischer Logik geschlossen wird.

Die Autoren räumen einen „Friction-Utility Trade-off“ ein und merken an, dass zu restriktive Richtlinien den Nutzen des Agenten mindern können. Sie postulieren, dass die Generator-Critic-Schleife, insbesondere die Einbeziehung eines Soft Critics, essenziell ist, um die „Goldilocks-Zone“ zu erreichen, in der Agenten ausreichend eingeschränkt, aber dennoch funktionsfähig bleiben. Die Arbeit demonstriert, dass Autoformalisierung die Durchsetzung von Richtlinien auf komplexe, reale Spezifikationen skalieren kann, ohne die für Hochrisikodomänen erforderlichen formalen Garantien aufzugeben.

Limitierungen und zukünftige Arbeit
Die Autoren stellen fest, dass Cedar per Design zustandslos (stateless) ist, was die Fähigkeit einschränkt, Multi-Turn-Workflows zu handhaben, die von der Abfolge von Aktionen oder persistenter Kontext abhängen. Zukünftige Arbeiten zielen darauf ab, dies durch die Integration von temporaler Logik für Voraussetzungs-Sequenzen und die Entwicklung von gedächtnisbewussten Richtlinien (memory-aware policies) zu adressieren, die es der Engine ermöglichen, auf die Historie der Trajektorie eines Agenten zuzugreifen.