Sintesi Tecnica: Agenti LLM Provabilmente Verificabili e Sicuri da Ontologie Autorevoli da Umani

1. Definizione del Problema

Gli agenti basati su Large Language Models (LLM) esibiscono un comportamento nondeterministico e allucinazioni, ponendo rischi significativi in domini critici per la sicurezza che richiedono una verificabilità lineare, come la conformità sanitaria e la sicurezza finanziaria. Gli approcci attuali alla sicurezza degli agenti si affidano a "guardrail" operativi (ad esempio, la sostituzione dei harness degli agenti o l'uso di LLM come giudici) che mancano di garanzie semantiche. Nello specifico, i sistemi multi-agente soffrono spesso di anomalie di "Write Skew", in cui agenti che operano su fette di stato locale disgiunte propongono indipendentemente azioni che, se combinate, violano gli invarianti globali del sistema (ad esempio, superando un budget o violando vincoli normativi). Gli framework esistenti faticano a fornire una garanzia matematica che le transizioni di stato globale preservino sempre tali invarianti, indipendentemente dal comportamento degli agenti o da input esterni avversari.

2. Metodologia

2.1 Architettura Agentic Redux

Il documento introduce Agentic Redux, un'architettura per agenti ispirata al pattern di gestione dello stato Redux. Essa separa il sistema in tre livelli:

1. Sotto-agenti (Sub-agents): Ogni agente opera su una "fetta" isolata dello stato globale. Gli agenti propongono azioni basate sulla loro visione locale, potendo utilizzare LLM o strumenti. Non possono modificare direttamente lo stato globale né osservare le fette di stato di altri agenti.
2. Meta-agente: Un adjudicatore centrale con piena visibilità dello stato globale. Riceve le proposte dai sotto-agenti e le valuta rispetto a un insieme di invarianti dichiarati (regole che devono essere sempre vere riguardo allo stato globale).
3. Disciplina di Commit (Commit Discipline): Il meta-agente è l'unica entità autorizzata a modificare lo stato globale. Esso approva la transizione di stato solo se il risultato preserva tutti gli invarianti. Se una proposta viola un invaritore, viene rifiutata o scalata.

2.2 Design degli Agenti "Ontology-First"

Per applicare Agentic Redux a domini specifici, gli autori propongono una metodologia chiamata Ontology-First Agent Design:

1. Ontologizzazione: Un esperto umano costruisce un "ontologia inferiore" del dominio del problema utilizzando la Basic Formal Ontology (BFO). Questa definisce continuanti indipendenti (es. Pazienti, Vulnerabilità), processi e ruoli.
2. Derivazione dei Ruoli: Un LLM ha il compito di analizzare l'ontologia per derivare i ruoli degli agenti. Ciò comporta il raggruppamento di processi con impronte di stato sovrapponibili e l'assegnazione di essi ai ruoli. L'obiettivo è ottenere ruoli granulari che aderiscano al Principio del Minimo Privilegio (PoLP), garantendo che gli agenti vedano solo lo stato necessario per i loro compiti specifici.
3. Derivazione degli Invarianti: Un LLM estrae gli invarianti di sistema dall'ontologia, classificandoli come locali (imponibili da una singola fetta di un agente) o trasversali (che richiedono la visione globale del meta-agente).
4. Costruzione del Modulo di Dominio: L'ontologia e i ruoli/invarianti derivati vengono convertiti in un Modulo di Dominio tipizzato, che viene poi eseguito sul kernel di Agentic Redux.

2.3 Verifica Formale

Il documento utilizza il calcolo lambda tipizzato per modellare formalmente l'architettura Agentic Redux. Il sistema è definito come un "Architecture Functor" che prende in input un Modulo di Dominio. Gli autori dimostrano che per ogni esecuzione ben tipizzata:

• Preservazione degli Invarianti: Se lo stato iniziale soddisfa gli invarianti, ogni stato raggiungibile in qualsiasi esecuzione (inclusi quelli con output LLM nondeterministici o scheduling avversari) preserva tali invarianti.
• Confinamento degli Agenti: Gli agenti sono matematicamente limitati all'osservazione e all'influenza solo delle fette di stato assegnate loro.
• Verificabilità Lineare: Il sistema mantiene un registro append-only dove ogni decisione (approvazione, rifiuto o escalation) viene registrata con una prova del motivo per cui la decisione è stata presa.

3. Contributi Chiave

• Architettura Agentic Redux: Un nuovo framework per agenti che fornisce una garanzia semantica di sicurezza imponendo la preservazione degli invarianti attraverso un meta-agente centralizzato, eliminando efficacemente le anomalie di Write Skew.
• Prove Formali: La prima applicazione del calcolo lambda tipizzato per dimostrare che le esecuzioni degli agenti LLM sono semanticamente garantite nella correttezza (preservazione degli invarianti) e linearmente verificabili, anche quando i sotto-agenti sono difettosi, malevoli o soggetti ad allucinazioni.
• Design degli Agenti Ontology-First: Una metodologia per derivare semi-automaticamente i framework degli agenti da ontologie scritte da umani, sfruttando gli LLM per l'estrazione di ruoli e invarianti pur mantenendo la costruzione critica dell'ontologia nelle mani umane.
• Estensione della Coda del Consigliere (Counselor Queue): Un meccanismo per gestire i casi limite in cui è richiesto l'intervento umano. Il sistema consente a un "Consigliere" umano di sovrascrivere le decisioni, ma il sistema traccia formalmente queste sovrascritture nel log di audit, distinguendo tra "Safe Counselor Commits" (che preservano gli invarianti) e violazioni delle policy.
• Casi Studio di Grado Produttivo: Gli autori dimostrano l'architettura in due domini distinti:
  1. Conformità della Fatturazione Sanitaria (UDT): Garantire che la fatturazione dei test del farmaco nelle urine (Urine Drug Test) aderisca a complesse regolamentazioni dipendenti dal tempo (es. livelli di astinenza) dove agenti clinici e di fatturazione indipendenti potrebbero altrimenti causare errori di copertura.
  2. Divulgazione di Vulnerabilità di Sicurezza: Gestire la pipeline di divulgazione delle vulnerabilità software, garantendo la coordinazione tra lo sviluppo di patch, l'applicazione dell'embargo e l'attribuzione CVE senza far trapelare informazioni sensibili tra divulgazioni concorrenti.

4. Risultati

• Garanzie Teoriche: Il documento presenta il Teorema 1 (Preservazione degli Invarianti), dimostrando che le esecuzioni di Agentic Redux non raggiungono mai uno stato che violi gli invarianti dichiarati, a condizione che lo stato iniziale sia valido. Il Teorema 2 (Integrità del Log di Audit) dimostra che il sistema genera un log lineare e append-only di tutte le decisioni con piena provenienza. Il Corollario 1 stabilisce che le esecuzioni di Write Skew sono strutturalmente impossibili sotto questa architettura.
• Implementazione: Il codice funzionante per il kernel di Agentic Redux e i due esempi di dominio (Conformità UDT e Divulgazione di Vulnerabilità di Sicurezza) è fornito in un repository di supporto. Il codice dimostra l'auto-derivazione degli agenti da ontologie BFO.
• Confronto con Pattern Esistenti: L'architettura si mostra essere isomorfa al framework "Risk Agents" utilizzato da CashApp, suggerendo che Agentic Redux catturi un pattern architettonico "naturale" per workflow complessi e regolamentati.

5. Significato e Rivendicazioni

Il documento sostiene che Agentic Redux sposta l'onere della sicurezza dal monitoraggio operativo a runtime al design architettonico. Utilizzando proprietà di teoria dei tipi, l'architettura assicura che "i comportamenti errati non possano mai accadere" a livello semantico, indipendentemente dall'imprevedibilità degli LLM che agiscono come sotto-agenti.

Gli autori sottolineano che questo approccio permette agli ingegneri di costruire sistemi in cui l' "harness" (il meccanismo di sicurezza) non ha bisogno di essere sostituito man mano che gli LLM evolvono, poiché la sicurezza è garantita dal sistema di tipi dell'architettura, non dall'output del modello specifico. La metodologia del Design degli Agenti Ontology-First è presentata come un modo scalabile per tradurre l'esperienza di dominio umana in framework di agenti provabilmente sicuri, concentrando l'impegno umano sull'ontologia (la "verità") e sfruttando gli LLM per la derivazione meccanica di ruoli e codice.

Il documento delimita esplicitamente le sue rivendicazioni alla sicurezza (prevenire cose brutte) e alla verificabilità, notando che la liveness (garantire che le cose buone accadano eventualmente) e le metriche di complessità sono affrontate in lavori futuri. Riconosce che, sebbene l'architettura prevenga le violazioni degli invarianti, non impedisce al sistema di comportarsi male se gli invarianti stessi sono scarsamente specificati; pertanto, la qualità dell'ontologia scritta dall'uomo rimane il fattore critico.