A Neuro-Symbolic Framework for Accountability in Public-Sector AI

Questa tesi propone un framework neuro-simbolico che integra un'ontologia normativa, l'estrazione di regole e il ragionamento basato su solver per garantire che le decisioni automatizzate di ammissibilità per CalFresh siano allineate alle norme giuridiche, consentendo così una responsabilità procedurale tracciabile e contestabile.

L'essenziale

Immagina un ufficio governativo che decide chi riceve assistenza alimentare. Quando dicono "no" a un richiedente, inviano una lettera che spiega il motivo. Di solito, queste lettere sono scritte in un gergo legale confuso. Il richiedente la legge, pensa: "Sembra ragionevole", ma non può effettivamente verificare se il governo sta seguendo correttamente le regole. È costretto a fidarsi della lettera perché non dispone degli strumenti legali per verificarla.

Questo documento propone un nuovo "arbitro digitale" per controllare quelle lettere. Ecco come funziona, scomposto in concetti semplici:

Il Problema: La "Scatola Nera" della Burocrazia

Pensa al processo decisionale del governo come a una scatola nera. Inserisci le tue informazioni e ne esce una decisione. A volte, la scatola è un programma informatico; a volte, è un umano che segue un complesso regolamento. Il problema è che la "lettera di spiegazione" inviata a te potrebbe sembrare buona in superficie, ma potrebbe segretamente violare le regole.

Attualmente, facciamo affidamento sulla "interpretabilità" — cercando di rendere visibile il pensiero del computer. Ma gli autori sostengono che, in un contesto legale, semplicemente vedere il pensiero non è sufficiente. Hai bisogno di auditabilità. Devi sapere se la spiegazione corrisponde effettivamente alla legge, come controllare se uno scontrino corrisponde agli articoli acquistati.

La Soluzione: Un "Traduttore" e un "Controllore di Regole"

Gli autori hanno costruito un sistema chiamato Framework Neuro-Simbolico. Puoi immaginarlo come una squadra di due persone che lavorano insieme:

1. Il Traduttore (La Parte "Neurale"):
   Immagina un robot super-intelligente che legge le leggi governative disordinate e complesse (scritte in inglese) e le lettere di spiegazione disordinate inviate ai richiedenti. Il compito di questo robot è tradurre quel linguaggio umano in un linguaggio matematico rigoroso che i computer possono comprendere perfettamente. È come un traduttore che trasforma una poesia in un insieme preciso di equazioni matematiche.

   • Nel documento: Hanno utilizzato un Modello Linguistico di Grande Dimensione (LLM) per trasformare leggi come "Devi guadagnare meno di 2.000 dollari" in una regola formale: Se Reddito > 2000, Allora Non Elegibile.

2. Il Controllore di Regole (La Parte "Simbolica"):
   Una volta che le leggi e le lettere di spiegazione sono state trasformate in equazioni matematiche, entra in gioco una macchina logica rigorosa (chiamata risolutore SMT). Questa macchina non indovina; calcola. Chiede: "La lettera di spiegazione matematicamente prova la decisione?"

   • Se la lettera dice: "Ti è stato negato perché guadagni troppo", e la matematica mostra che effettivamente guadagni troppo, la macchina dice SAT (Soddisfacibile/Valido). La spiegazione regge.
   • Se la lettera dice: "Ti è stato negato perché guadagni troppo", ma la matematica mostra che non guadagni troppo, la macchina dice UNSAT (Insoddisfacibile/Invalido). La spiegazione è una menzogna o un errore, anche se sembra plausibile a un umano.

Il Test nel Mondo Reale: CalFresh

Il team ha testato questo sistema su CalFresh, il programma di assistenza alimentare della California. Hanno preso 50 casi reali in cui le persone avevano visto i loro benefici negati o ridotti.

• La Configurazione: Hanno fornito al sistema la legge effettiva, i fatti del richiedente (reddito, numero di familiari) e la lettera ufficiale inviata dal governo.
• Il Risultato: Il sistema ha individuato con successo "disallineamenti legali". In un test, hanno ingannato il sistema cambiando una decisione "Negata" in "Approvata" ma mantenendo la stessa spiegazione (che diceva che la persona guadagnava troppo). Il sistema ha immediatamente urlato UNSAT, indicando che la spiegazione contraddiceva la nuova decisione.
• La "Prova Fumante": Quando il sistema trovava un errore, non diceva semplicemente "Errore". Indicava la pagina esatta e il paragrafo della legge che era stato violato. È come un arbitro che non solo fischia, ma indica la pagina specifica del regolamento che il giocatore ha infranto.

Perché Questo È Importante

Gli autori sostengono che dobbiamo smettere di cercare di semplicemente "spiegare" come pensa l'IA e iniziare a verificare le giustificazioni legali che produce.

• Modo Attuale: "Ecco perché il computer ha detto di no. Si basa su un modello che ha appreso." (Questo è difficile da contestare in tribunale).
• Nuovo Modo: "Ecco la lettera. Il nostro sistema l'ha controllata contro la legge e ha scoperto che viola la Sezione 63-409.111." (Questo è facile da contestare in tribunale).

La Conclusione

Questo documento non afferma di voler sostituire il governo o prendere le decisioni finali. Invece, costruisce una rete di sicurezza digitale. Assicura che quando il governo ti invia una lettera che dice "No", quella lettera sia effettivamente una ragione legale valida, non solo una scusa confusa. Trasforma la "spiegazione" da un pezzo di carta a cui devi fidarti, in una prova che puoi verificare.

Punto Chiave: Nel mondo dei benefici pubblici, una spiegazione non riguarda solo la chiarezza; riguarda l'essere legalmente vera. Questo sistema è lo strumento che verifica se la verità viene effettivamente raccontata.

Sommario tecnico

Riepilogo Tecnico: Un Framework Neuro-Simbolico per la Responsabilità Legale nell'IA del Settore Pubblico

1. Enunciato del Problema

Le agenzie pubbliche fanno sempre più affidamento su sistemi di decisione automatizzata (ADM) per governare l'accesso ai benefici di welfare. Sebbene tali sistemi promettano efficienza, spesso mancano di trasparenza, rendendo difficile per i richiedenti comprendere o contestare le determinazioni di ammissibilità. Gli approcci attuali all'Intelligenza Artificiale Spiegabile (XAI) si concentrano sull'interpretabilità del modello, sulla fedeltà o sulla fiducia dell'utente. Tuttavia, nei contesti legali e amministrativi, la funzione primaria di una spiegazione non è semplicemente essere compresa, ma servire come giustificazione legale che possa essere contestata in contesti adversariali o quasi-giudiziari.

Il problema centrale identificato è che le spiegazioni esistenti (ad esempio, gli Avvisi di Azione) possono apparire plausibili ai lettori umani, ma falliscono nel fare riferimento alla corretta autorità legale o nel dichiarare erroneamente le condizioni statutarie. Manca un'infrastruttura tecnica per verificare se questi artefatti giustificativi siano legalmente validi rispetto alle leggi vigenti. I metodi di audit attuali si concentrano spesso sulla conformità a livello di decisione o sul comportamento del modello, trascurando l'integrità legale delle spiegazioni stesse. Questo divario impedisce ai richiedenti e agli organi di vigilanza di valutare efficacemente se una decisione soddisfi i criteri statutari e le norme procedurali.

2. Metodologia

Gli autori propongono un framework neuro-simbolico progettato per verificare automaticamente l'adeguatezza legale delle spiegazioni di ammissibilità ai benefici di welfare. Il sistema sposta il focus dall'interpretazione degli interni del modello alla verifica delle giustificazioni fornite ai richiedenti. L'architettura consta di quattro fasi principali:

2.1 Fonti di Dati

• Corpus Statutario: Il Manuale delle Politiche e delle Procedure (MPP) della California, Divisione 63, che disciplina il programma CalFresh (SNAP).
• Dati di Caso: 50 decisioni di appello amministrativo della Divisione Udienze Statali del Dipartimento dei Servizi Sociali della California (CDSS). Questi record includono la spiegazione originale dell'agenzia, l'esito della determinazione e le circostanze fattuali presentate dal ricorrente.

2.2 Architettura del Sistema

Il framework opera attraverso una pipeline che separa le regole legali dalle affermazioni specifiche del caso:

1. Costruzione dell'Ontologia:

   • Un vocabolario legale controllato è derivato dalle regolamentazioni MPP utilizzando il Riconoscimento di Entità Nominate (NER) e il matching di similarità basato su embedding (utilizzando Qwen3-Embedding-8B).
   • L'ontologia mira alle dimensioni fondamentali di ammissibilità: reddito, residenza, cittadinanza, risorse e status di studente.
   • Questa struttura garantisce la tracciabilità verso fonti autorevoli e previene la ridondanza.

2. Codifica TBox (Terminological Box):

   • Rappresenta la struttura normativa della legge (regole invarianti rispetto al caso).
   • Le disposizioni statutarie sono segmentate e i termini operativi sono estratti.
   • Un Modello Linguistico di Grande Formato (LLM), specificamente OpenAI's o1, viene istruito a tradurre queste disposizioni in regole logiche formali pronte per il solver (ad esempio, implicazioni, condizioni necessarie).
   • Ogni regola è collegata alla sua citazione di origine (ad esempio, MPP §63-409.111).

3. Costruzione ABox (Assertion Box):

   • Rappresenta il contenuto a livello di caso (fatti e affermazioni esplicative).
   • La spiegazione dell'agenzia è tradotta nello stesso formato logico della TBox utilizzando l'LLM.
   • I predicati fattuali (ad esempio, dimensione del nucleo familiare, importi del reddito) sono estratti dai record delle udienze.
   • L'ABox combina le regole TBox recuperate invocate dalla spiegazione, la logica della spiegazione tradotta e i fatti specifici del caso.

4. Verifica Basata su SMT:

   • Un solver Satisfiability Modulo Theories (SMT) valuta la soddisfacibilità congiunta della TBox (regole legali) e dell'ABox (affermazioni del caso).
   • Esito SAT: La spiegazione è coerente con la legge vigente e può funzionare come una giustificazione legalmente ammissibile.
   • Esito UNSAT: La spiegazione è incoerente con la legge. Il solver estrae un nucleo insoddisfacibile — un sottoinsieme minimo di vincoli responsabili del conflitto — e li mappa nuovamente su specifiche disposizioni statutarie.

3. Contributi Chiave

• Passaggio dall'Interpretabilità alla Verificabilità: Il documento sostiene un cambiamento di paradigma in cui la responsabilità algoritmica pubblica è misurata dalla validità legale delle spiegazioni piuttosto che dalla sola interpretabilità del modello.
• Pipeline di Verifica Neuro-Simbolica: Una nuova integrazione in cui i componenti neurali (LLM) gestiscono l'estrazione e la traduzione di testi e spiegazioni legali non strutturati, mentre i componenti simbolici (solver SMT) forniscono verifica deterministica e tracciabilità.
• Responsabilità a Livello di Spiegazione: A differenza di lavori precedenti che formalizzavano strumenti di screening (ad esempio, Escher e Banovic, 2020), questo framework valuta gli artefatti giustificativi (avvisi di azione) emessi ai richiedenti, sostenendo i diritti di contestazione e appello.
• Segnali Basati sulla Legge: Il sistema non segnala semplicemente errori; produce segnali di responsabilità azionabili identificando esattamente quali disposizioni statutarie sono violate da una spiegazione.

4. Risultati

Il framework è stato valutato su 50 casi CalFresh in cinque categorie di ammissibilità (Status di Studente, Reddito, Residenza, Cittadinanza, Risorse). Per la valutazione, gli autori hanno creato istanze appaiate invertendo la determinazione di ammissibilità mantenendo costante la spiegazione per testare le contraddizioni legali.

• Accuratezza di Verifica: Il sistema ha raggiunto un'accuratezza complessiva del 97,7% nel distinguere tra spiegazioni legalmente coerenti (SAT) e incoerenti (UNSAT).
• Precisione di Localizzazione: Quando è stata rilevata un'incoerenza (UNSAT), il sistema ha localizzato con successo la specifica disposizione statutaria implicata.
  • Punteggio F1 di Localizzazione: Variava per categoria, da 0,51 (Reddito) a 0,83 (Cittadinanza), con una media complessiva di 0,977 per i casi UNSAT in cui la localizzazione era applicabile.
  • Le categorie con regole più determinate (Cittadinanza, Residenza) hanno mostrato un'accuratezza di recupero superiore rispetto a quelle con sfumature contestuali (Reddito, Status di Studente).
• Studio di Caso: In un caso specifico in cui la cessazione di un beneficio era giustificata da "il reddito lordo supera il limite", il sistema ha confermato che la spiegazione era SAT. Quando la determinazione è stata invertita in "ammissibile" mantenendo la stessa spiegazione, il sistema ha restituito correttamente UNSAT e ha identificato MPP §63-409.111 come la disposizione violata.

5. Significato e Affermazioni

Gli autori affermano che questo lavoro offre una prova di concetto per incorporare la responsabilità legale nel substrato tecnico dell'IA del settore pubblico.

• Impalcatura Istituzionale: Il sistema è progettato non per sostituire il potere discrezionale amministrativo o automatizzare il giudizio legale, ma per agire come "impalcatura istituzionale" che rafforza la vigilanza e la contestabilità. Automatizza la verifica delle giustificazioni, non le decisioni stesse.
• Governance oltre la Trasparenza: Il documento riformula l'esplicabilità come una sfida di governance. Afferma che per gli algoritmi pubblici, le spiegazioni devono fare più che rivelare associazioni statistiche; devono articolare la base legale di una decisione per soddisfare i diritti di processo dovuto.
• Applicabilità: Il framework è applicabile indipendentemente dal fatto che il motore decisionale sottostante sia predittivo, basato su regole o ibrido, poiché valuta il livello esplicativo emesso al richiedente.
• Limitazioni: Gli autori notano modestamente che il sistema si basa su una formalizzazione specifica del compito delle leggi e non può catturare pienamente standard a trama aperta o giudizi discrezionali. La valutazione ha utilizzato casi controllati e a singola legge per garantire un'attribuzione chiara, il che significa che la complessità del mondo reale che coinvolge molteplici leggi interagenti potrebbe presentare sfide aggiuntive. Il sistema è uno strumento tecnico per l'infrastruttura di responsabilità, non un sostituto del giudizio legale olistico.

In conclusione, il documento dimostra che la responsabilità legale a livello di spiegazione può essere resa computazionalmente trattabile attraverso metodi neuro-simbolici, fornendo un meccanismo per agenzie, organi di vigilanza e individui per valutare se le giustificazioni automatizzate soddisfino i requisiti statutari.