Autoformalization of Agent Instructions into Policy-as-Code

Sintesi Tecnica: Autoformalizzazione delle Istruzioni degli Agenti in Policy-as-Code

Problematica
L'impiego di agenti autonomi basati su Large Language Model (LLM) in domini ad alto rischio (ad es. l'assistenza sanitaria) presenta un critico compromesso di sicurezza: gli agenti richiedono privilegi elevati per eseguire compiti complessi, ma tali privilegi espandono la superficie di attacco per tecniche avversarie come il prompt injection. Le attuali pratiche industriali si affidano pesantemente a guardrail probabilistici, come classificatori di sicurezza sottoposti a fine-tuning (ad es. Llama Guard) o steering basato su prompt. Sebbene questi metodi offrano una certa utilità, mancano di garanzie formali e sono spesso inadeguati per applicazioni critiche per la sicurezza dove è richiesto un enforcement deterministico. Al contrario, l'enforcement simbolico codificato manualmente offre garanzie formali, ma non riesce a scalare rispetto alla portata e alla complessità delle specifiche di policy del mondo reale.

Metodologia
Gli autori propongono una pipeline di autoformalizzazione che traduce le istruzioni in linguaggio naturale degli agenti, le descrizioni degli strumenti del Model Context Protocol (MCP) e i documenti di policy in policy formalmente verificate scritte nel linguaggio di policy Cedar. Questa pipeline opera tramite un ciclo generatore-critico strutturato come un "Verification Sandwich" composto da tre distinti livelli:

1. Il Livello di Grounding (Base): Questo livello stabilisce le fondamenta estraendo entità, identificando gli schemi degli strumenti (ad es. schemi JSON di OpenAI) e definendo un'ontologia principale-risorsa-azione. Garantisce che l'agente operi all'interno di un ambiente strutturato in cui le potenziali azioni mappano su entità del mondo reale e identificatori di sistema validi. Fondamentalmente, genera programmaticamente uno schema Cedar dalle definizioni degli strumenti MCP per servire come meccanismo rigoroso di controllo dei tipi (type-checking).
2. Il Livello del Modello (Intermedio): Utilizzando LLM allo stato dell'arte, questo livello interpreta le istruzioni in linguaggio naturale e genera set di policy candidati. Sfrutta la conoscenza parametrica per proporre policy che riflettano la logica intenzionale dell'agente.
3. Il Livello di Sicurezza (Superiore): Questo livello impiega un meccanismo a doppio critico per validare i candidati:
   • Hard Critic: Un controllo deterministico e programmatico utilizzando gli strumenti di analisi statica integrati in Cedar. Verifica la sintassi, impone la conformità dello schema e rileva contraddizioni logiche (ad es. policy vacue o regole conflittuali).
   • Soft Critic: Un LLM-as-a-judge che valuta l'allineamento semantico rispetto a una rubrica predefinita. Assicura che la logica formale rifletta accuratamente lo spirito delle istruzioni in linguaggio naturale e dei documenti di policy originali.

Il ciclo itera, fornendo feedback dai due critici al generatore finché il set di policy non supera sia i controlli hard che quelli soft. Le policy risultanti sono applicate a runtime da un motore di policy esterno e deterministico, disaccoppiando la logica di sicurezza dal contesto di ragionamento dell'LLM.

Contributi Chiave

• Architettura Verification Sandwich: Un approccio stratificato innovativo all'autoformalizzazione che combina grounding, ragionamento generativo e verifica a doppia modalità (hard/soft) per tradurre la policy non strutturata in codice formale.
• Implementazione Open-Source: Il rilascio di un harness di policy open-source per scaffold di agenti implementato in Cedar, inclusi binding Python personalizzati.
• Autoformalizzazione Scalabile: Una pipeline che converte automaticamente le "agent cards" (istruzioni + schemi degli strumenti) in policy di autorizzazione verificate, affrontando i limiti di scalabilità dell'enforcement simbolico manuale.
• Framework di Valutazione: Una valutazione rigorosa sul benchmark MedAgentBench, che confronta l'approccio autoformalizzato con i precedenti guardrail simbolici codificati a mano.

Risultati
Il sistema è stato valutato su MedAgentBench, un benchmark per agenti che utilizzano strumenti per cartelle clinhe elettroniche (EMR). Lo studio ha confrontato tre condizioni: strumenti HTTP grezzi, una Baseline con strumenti MCP tipizzati e una condizione di Guardrail utilizzando le policy Cedar degli autori rispetto ai guardrail simbolici codificati a mano di Hong et al.

• Copertura: La pipeline di autoformalizzazione ha coperto sostanzialmente più della specifica in linguaggio naturale originale di 88 regole rispetto all'approccio codificato a mano, che ha implementato solo 23 regole.
• Tassi di Blocco: Nella condizione "Guardrail", il motore di policy Cedar ha bloccato una percentuale significativamente più alta di violazioni di policy rispetto alla baseline codificata a mano, particolarmente negli scenari avversari.
  • Sul dataset Originale, Cedar ha bloccato il 55,7% delle traiettorie (167/300), mentre i guardrail codificati a mano hanno bloccato lo 0% (per costruzione, poiché coprivano solo un sottoinsieme di regole).
  • Sul dataset Adversarial, Cedar ha bloccato l'85,7% delle traiettorie (42/49).
• Analisi dei Tentativi di Scrittura: Quando filtrando per traiettorie contenenti effettivi tentativi di scrittura (richieste POST), il tasso di blocco di Cedar si è avvicinato al 100% (ad es. 100,0% nella condizione Adversarial Guardrail), dimostrando che il sistema impedisce efficacemente modifiche non autorizzate ai dati quando queste avvengono.
• Robustezza: Il sistema ha impedito con successo "jailbreaking" e prompt injection indiretti imponendo le regole al di fuori della finestra di contesto dell'LLM.

Significatività e Rivendicazioni
Il documento sostiene che questo approccio fornisce forti garanzie formali sul comportamento dell'agente, una capacità assente nei guardrail probabilistici. Disaccoppiando l'enforcement della policy dal contesto di ragionamento dell'LLM, l'architettura mitiga il rischio che un attaccante convinca lo strato di sicurezza a ignorare le proprie regole. L'uso di Cedar assicura che le policy siano leggibili dall'uomo, verificabili e formalmente validate, colmando il divario tra la flessibilità del linguaggio naturale e il rigore della logica simbolica.

Gli autori riconoscono un "compromesso tra frizione e utilità", notando che le policy eccessivamente restrittive possono degradare l'utilità dell'agente. Essi postulano che il Ciclo Generatore-Critico, in particolare l'inclusione di un soft critic, è essenziale per raggiungere una "zona Goldilocks" in cui gli agenti siano sufficientemente vincolati ma rimangano funzionali. Il lavoro dimostra che l'autoformalizzazione può scalare l'enforcement delle policy a specifiche complesse del mondo reale senza sacrificare le garanzie formali richieste in domini ad alto rischio.

Limitazioni e Lavoro Futuro
Gli autori osservano che Cedar è progettato per essere stateless, il che limita la sua capacità di gestire workflow multi-turno dipendenti dall'ordine delle azioni o dal contesto persistente. Il lavoro futuro mira ad affrontare questo aspetto integrando la logica temporale per sequenze di prerequisiti e sviluppando policy consapevoli della memoria che permettano al motore di fare riferimento alla cronologia della traiettoria dell'agente.