Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)

Riepilogo Tecnico: Verifica Neuro-Simbolica delle Uscite degli LLM per Domini Sensibili ai Dati

Enunciato del Problema
I Large Language Models (LLM) affrontano sfide fondamentali di affidabilità quando vengono distribuiti in ambiti ad alto rischio e sensibili ai dati, come la diagnosi medica, la revisione legale e gli affari normativi. Queste sfide includono allucinazioni (generazione di informazioni credibili ma false), incoerenze e vulnerabilità alla privacy. In questi contesti, gli errori comportano conseguenze legali, finanziarie o per la sicurezza, rendendo inaccettabili i tassi di allucinazione del 3–10% osservati nei modelli più avanzati. Inoltre, vincoli normativi e istitutivi rigorosi spesso impongono l'elaborazione locale dei dati per garantire la sovranità dei dati, limitando l'utilità delle API basate sul cloud e degli LLM generici. Gli approcci esistenti, come la generazione aumentata dal recupero (RAG) o il prompting a catena di pensiero, mancano delle garanzie necessarie per ambienti specializzati, mentre i metodi di auto-verifica ereditano i bias distribuzionali dei modelli che tentano di verificare.

Metodologia
Il documento propone un'architettura di verifica ibrida che combina metodi simbolici formali con analisi semantica neurale per fornire garanzie complementari. Il sistema è progettato attorno a quattro principi fondamentali: elaborazione "local-first", separazione modulare dei componenti simbolici e neurali, isolamento dei guasti basato su attori e verifica delle affermazioni consapevole dei tipi.

1. Verifica Simbolica degli Input (Pre-elaborazione):
   L'architettura impiega la logica basata su tableaux per convalidare i vincoli di input prima che avvenga qualsiasi inferenza LLM. Questo metodo scompone i requisiti di convalida in una gerarchia configurabile di condizioni dichiarative. Le condizioni di base valutano predicati atomici (ad esempio, la presenza di metadati), mentre le meta-condizioni di ordine superiore esprimono relazioni insiemistiche (ad esempio, obblighi cumulativi o percorsi di sufficienza alternativi). Questo approccio fornisce garanzie decidibili, solide e complete per i requisiti strutturati, agendo come un "blocco critico" per violazioni critiche o come un sistema di avviso graduato per disallineamenti minori.

2. Concorrenza Basata su Attori:
   Per garantire robustezza e isolamento dei guasti, il sistema utilizza il modello ad attori (implementato tramite Elixir sulla macchina virtuale Erlang). Le pipeline di verifica eseguono più flussi di analisi eterogenei (convalida delle regole simboliche, estrazione di entità, confronti di embedding neurali) in concorrenza senza stato mutabile condiviso. Gli attori supervisori monitorano i processi worker, riavviando automaticamente i componenti falliti (ad esempio, timeout di inferenza neurale) senza corrompere lo stato più ampio di convalida simbolica.

3. Verifica Ibrida delle Uscite (Post-elaborazione):
   L'architettura implementa una strategia di verifica consapevole dei tipi per i contenuti generati dall'LLM:

   • Entità Strutturate: Per dati deterministici (date, identificatori, valori numerici), il sistema utilizza il matching di pattern simbolico e il confronto basato su regex per fornire una verifica esatta.
   • Affermazioni in Testo Libero: Per i contenuti semantici, il sistema impiega la similarità semantica basata su embedding (utilizzando encoder di frasi multilingue) per rilevare allucinazioni contestuali dove i metodi formali mancano di espressività.
   • Integrazione Parallela: I flussi di elaborazione simbolica e neurale vengono eseguiti in parallelo. Negli scenari di recupero, il filtraggio simbolico riduce lo spazio di ricerca (ad esempio, per tipo di sezione o ID rapporto) prima del ranking neurale, riducendo il rumore e l'utilizzo dei token per i modelli distribuiti localmente.

4. Progettazione a Salvaguardia della Privacy:
   Il sistema impone un'elaborazione "local-first", garantendo che tutta l'inferenza, gli embedding e la verifica avvengano su hardware locale. I dati sensibili sono isolati all'interno di sottoalberi di supervisione dedicati, e gli embedding vettoriali fungono da trasformazioni con perdita per collezioni indicizzate, garantendo una protezione di tipo informativo.

Implementazione del Sistema: HAIMEDA
L'architettura è istanziata in HAIMEDA (Hybrid AI for Medical Device Assessment), un sistema sviluppato attraverso la Ricerca per Progettazione di Azione (ADR) con un esperto di dominio. HAIMEDA è progettato per il contesto legale tedesco, dove un perito giurato deve produrre relazioni di valutazione del danno in condizioni di stretta riservatezza e vincoli di sovranità dei dati. Il sistema integra:

• Modulo di Redazione del Rapporto (RAM): Gestisce la generazione tramite modelli Llama3-DiscoLeo-Instruct-8B fine-tunati.
• Modulo di Ricerca e Indagine (RIM): Esegue il restringimento ibrido per il recupero di conoscenze di dominio.
• Modulo di Verifica dell'Integrità delle Informazioni (IIVM): Esegue una verifica multistadio rispetto al materiale sorgente.

Risultati
La valutazione è stata condotta su hardware di livello consumer (AMD Ryzen 9, NVIDIA RTX 4090) per riflettere i vincoli realistici di distribuzione locale.

• Rilevamento delle Allucinazioni: Il sistema ha raggiunto tassi di rilevamento superiori all'83% per le entità strutturate (tramite controlli simbolici) e del 72% per le fabbricazioni semantiche (tramite similarità neurale). La logica di pre-elaborazione ha raggiunto il 100% di rilevamento delle condizioni richieste mancanti.
• Efficienza del Flusso di Lavoro: La valutazione pratica con un esperto di dominio ha rivelato una riduzione del 30% nel tempo totale di creazione del rapporto. Nello specifico, il tempo di scrittura dei contenuti è diminuito del 50% e il tempo di ricerca basata su documenti è diminuito del 33%, sebbene il tempo di revisione finale sia aumentato a causa del processo di verifica.
• Usabilità del Sistema: Il sistema ha ottenuto un punteggio della Scala di Usabilità del Sistema (SUS) di 62,5.

Significato e Affermazioni
Il documento afferma che le architetture neuro-simboliche possono fornire salvaguardie principiate per la distribuzione degli LLM in domini sensibili ai dati affrontando i limiti degli approcci puramente neurali. Il contributo principale è un'architettura agnostica rispetto al modello che fonda le garanzie formali nella convalida simbolica piuttosto che fare affidamento sulle capacità di un singolo modello di base. Separando i compiti di verifica in base alla loro natura (vincoli decidibili vs. ambiguità semantica), il sistema offre una soluzione scalabile per garantire l'integrità delle informazioni senza compromettere la sovranità dei dati. Gli autori sottolineano che questo approccio va oltre le soluzioni puntuali per offrire un pattern architetturale generalizzabile per l'IA ibrida, abilitando pipeline di controllo qualità distribuibili localmente e con isolamento dei guasti, essenziali per le industrie regolamentate. Il documento riconosce le limitazioni, inclusa la dipendenza dalla copertura delle regole specifiche del dominio e la necessità di lavori futuri sul trasferimento tra domini e sugli studi di ablazione.