Riepilogo Tecnico: Applicazione Formale delle Politiche per Sistemi Agentici Reali

Enunciato del Problema

I sistemi agentici contemporanei, che integrano Modelli Linguistici di Grande Dimensione (LLM) con strumenti esterni per eseguire compiti come l'invio di email, l'esecuzione di codice e l'interrogazione di database, mancano di meccanismi robusti per l'applicazione di politiche di sicurezza e organizzative. Gli approcci attuali fanno prevalentemente affidamento sull'incorporazione di politiche in linguaggio naturale all'interno del prompt di sistema di un agente, delegando la conformità alle capacità di ragionamento dell'agente. Questa metodologia soffre di tre limitazioni critiche:

1. Mancanza di Garanzie Formali: La conformità è euristica e contingente alla capacità del modello di seguire le istruzioni, offrendo nessuna applicazione deterministica.
2. Incapacità di Esprimere la Storia Causale: I prompt in linguaggio naturale faticano ad applicare politiche dipendenti dalla storia causale di un'esecuzione (ad esempio, "consentire l'azione X solo se l'approvazione Y è stata ottenuta in un passaggio precedente").
3. Scalabilità nei Sistemi Multi-Agente: Gli approcci esistenti sono inadatti per ambienti multi-agente dove l'applicazione deve ragionare attraverso i confini degli agenti e ordinamenti parziali di eventi, piuttosto che su tracce lineari.

Queste lacune lasciano i sistemi agentici vulnerabili all'iniezione di prompt, all'uso non autorizzato di strumenti e alla riformulazione avversaria, limitandone il dispiegamento sicuro in scenari reali.

Metodologia

Gli autori propongono FORGE (FOrmal Runtime Guarantee Enforcement), un framework che tratta l'applicazione delle politiche come una preoccupazione trasversale, fondata sulla Programmazione Orientata agli Aspetti (AOP). Il framework disaccoppia la logica delle politiche dal ragionamento dell'agente, applicando regole in ogni punto decisionale rilevante per la politica senza modificare gli agenti sottostanti.

Architettura Principale

1. Formulazione Orientata agli Aspetti:

   • Punti di Unione (Join Points): Definiti come azioni candidate (ad esempio, invocazioni di strumenti) in attesa di autorizzazione.
   • Pointcut: Funzioni booleane sullo stato di esecuzione che determinano a quali azioni si applica una regola.
   • Consiglio (Advice): Il calcolo di applicazione eseguito da un Monitor di Riferimento, che valuta la politica e restituisce un verdetto Consenti o Nega.
   • Tessitore (Weaver): Un livello di strumentazione che intercetta le chiamate agli strumenti, sospende l'esecuzione, consulta il monitor e procede solo dopo l'approvazione.

2. Linguaggio delle Politiche (Datalog):

   • Le politiche sono specificate in Datalog con negazione stratificata ed estensioni a funzioni esterne.
   • Espressività: Supporta la specifica dichiarativa delle regole e la ricorsione, consentendo la definizione di relazioni transitve (ad esempio, catene di supervisione) e controllo degli accessi basato sulle relazioni (ReBAC).
   • Analizzabilità: Abilita analisi statiche per il rilevamento di contraddizioni, ridondanza, sussunzione e raggiungibilità condizionale, permettendo agli autori di verificare l'intento della politica e risolvere le ambiguità intrinseche nelle specifiche in linguaggio naturale.
   • Traduzione: Una pipeline traduce documenti di politiche in linguaggio naturale in programmi Datalog, annotati con collegamenti a livello di clausola al testo sorgente per la verifica della copertura e della conseguenza logica.

3. Substrato delle Politiche e Contratto Ambientale:

   • Substrato ($\Sigma$): Un insieme di predicati astratti (Ruolo, Provenienza, Specifici di Dominio) che descrivono il contesto di esecuzione.
   • Servizio di Osservabilità: Mantiene un grafo delle dipendenze causali degli eventi (messaggi, chiamate agli strumenti, risultati) e popola i predicati del substrato.
   • Contratto Assume/Guarantee: La correttezza è garantita sotto l'assunzione che l'ambiente soddisfi un contratto: deve popolare in modo sonoro e sufficiente i predicati del substrato con fatti coerenti con le loro interpretazioni intese (ad esempio, una genealogia causale accurata). Se il contratto vale, le decisioni del monitor di riferimento coincidono con la semantica intesa della politica.

Contributi Chiave

1. Framework Formale per l'Applicazione Agentic: Il documento presenta il primo framework in grado di applicare automaticamente le politiche nei sistemi multi-agente con garanzie di correttezza formale, utilizzando un paradigma AOP per separare le preoccupazioni trasversali dalla logica di base.
2. Specificazione delle Politiche Basata su Datalog: Introduce Datalog come linguaggio di politica per i sistemi agentici, sfruttando il suo supporto per la ricorsione e l'analisi statica per gestire politiche complesse e con stato che i prompt in linguaggio naturale non possono esprimere.
3. Il Sistema FORGE: Un'implementazione pratica composta da un tessitore di aspetti, un servizio di osservabilità e un monitor di riferimento. FORGE strumenta i framework per agenti (ad esempio, Langroid, $\tau^2$) per applicare le politiche a runtime senza alterare il codice dell'agente.
4. Teorema di Correttezza: Gli autori dimostrano un teorema assume/guarantee affermando che se l'ambiente soddisfa il contratto del substrato, le decisioni di applicazione a runtime sono corrette rispetto alla semantica intesa della politica.

Risultati della Valutazione

Il framework è stato valutato su tre studi di caso quantitativi e due dispiegamenti reali:

1. Difesa dall'Iniezione di Prompt (Flusso di Informazioni):

   • Obiettivo: Prevenire l'esfiltrazione di dati tramite iniezione di prompt.
   • Risultato: Gli agenti non strumentati hanno avuto un tasso di successo dell'attacco del 100%. FORGE lo ha ridotto allo 0% mantenendo il 100% di utilità nei compiti benigni.
   • Sovraccarico: La latenza è aumentata di circa 12–15 secondi per prova; l'aumento dei costi è stato trascurabile (<$0,003).

2. Flussi di Lavoro di Servizio Clienti ($\tau^2$-Bench):

   • Obiettivo: Applicare regole aziendali (cancellazioni, rimborsi, bagagli) su tre modelli all'avanguardia.
   • Risultato: La conformità è migliorata dal 58% al 98%. Il successo dei compiti è stato preservato o migliorato (ad esempio, i tassi di superamento sono passati dal 58% al 98%).
   • Sovraccarico: La latenza end-to-end è aumentata del 19–38% (decisione di autorizzazione mediana sub-millisecondo); l'aumento dei costi è stato < $0,05 per prova.

3. Farmacovigilanza Multi-Agente (MALADE):

   • Obiettivo: Applicare flussi di lavoro di approvazione per l'accesso ai dati FDA attraverso una pipeline multi-agente.
   • Risultato: Gli accessi non autorizzati alla FDA sono scesi da 40 a 0 su 15 prove. L'accuratezza del compito è rimasta al 100% (15/15 previsioni corrette).
   • Sovraccarico: La latenza è aumentata da 72,5s a 95,4s (guidata da cicli bloccati-poi-ripetuti); i costi sono aumentati da $0,072 a$0,103 per prova.

Dispiegamenti Reali: Il documento descrive anche l'applicazione riuscita in OpenClaw (applicazione della privacy tra agenti) e VS Code Copilot Chat (blocco del git push fino al superamento dell'analisi statica).

Significato e Affermazioni

Il documento afferma che FORGE rappresenta un avanzamento significativo colmando il divario tra specifiche di politiche informali e applicazione rigorosa a runtime nei sistemi agentic. Il suo significato principale risiede in:

• Garanzie Deterministiche: A differenza degli approcci basati su prompt, FORGE elimina le violazioni delle politiche per costruzione, a patto che il contratto ambientale sia soddisfatto.
• Applicazione con Stato: Supporta in modo unico politiche dipendenti dalla storia causale e relazioni transitve tra più agenti, una capacità assente nei sistemi esistenti privi di stato o basati su tracce lineari.
• Modularità: Intrecciando l'applicazione nel runtime, permette l'applicazione di politiche organizzative complesse senza richiedere modifiche al ragionamento interno dell'agente o agli strumenti sottostanti.
• Analizzabilità: L'uso di Datalog permette il rilevamento di contraddizioni e ambiguità nelle politiche prima del dispiegamento, trattando le politiche come artefatti revisionabili piuttosto che prompt opachi.

Gli autori mantengono modestia riguardo alla pipeline di traduzione, riconoscendo che, sebbene la traduzione dal linguaggio naturale a Datalog sia realizzata tramite LLM, attualmente manca di garanzie di correttezza formale e richiede revisione manuale e validazione iterativa. Identificano la robustezza di questa traduzione e l'estensione ad autori di politiche non esperti come problemi aperti per lavori futuri.