Riepilogo Tecnico: Analisi del "Narration Gap" nei cicli LLM-Solver

1. Definizione del Problema

Il documento affronta una vulnerabilità critica nelle pipeline di ragionamento neurosimbolico che combinano i Large Language Models (LLM) con solver formali (es. SAT, SMT). Sebbene questi sistemi sfruttino strumenti formali per fornire risposte fondate e verificabili a quesiti logici, gli autori identificano un "narration gap" (divario di narrazione) dove la robustezza del sistema viene meno.

La pipeline consiste in tre fasi:

1. Formalizzazione: Un LLM traduce una query in linguaggio naturale in una formula logica ($\phi$).
2. Decisione: Un solver formale determina la soddisfacibilità di $\phi$, restituendo un verdetto ($v$) e un certificato ($c$).
3. Narrazione: Un LLM traduce il verdetto formale nuovamente in una risposta in linguaggio naturale per l'utente.

La ricerca precedente si è concentrata sulla correttezza della formalizzazione e della fase decisionale. Tuttavia, la fase di narrazione rimane non certificata. Gli autori sostengono che, anche se il verdetto del solver è matematicamente corretto e indipendentemente verificato, un avversario può manipolare l'LLM durante la fase di narrazione (tramite prompt injection) per invertire la conclusione finale rivolta all'utente, lasciando intatti il verdetto e il certificato sottostanti. Ciò risulta in un "fallimento furtivo" (stealthy failure) in cui il sistema riporta uno stato intermedio corretto ma una risposta finale errata, eludendo i monitor di runtime standard che controllano solo il verdetto.

2. Metodologia

Modellazione Formale

Gli autori modellano il ciclo LLM-solver come una procedura decisionale verificata. Definiscono:

• Assunzioni: La formalizzazione è fedele all'intento dell'utente e il solver è sound (corretto) e complete (completo).
• Modello di Avversario: Un avversario esegue un'iniezione di prompt indiretta controllando contenuti non attendibili (es. note o commenti alle formule) forniti al contesto del narratore. L'obiettivo è invertire la conclusione finale ($\bar{p} = \neg \rho(v)$) mantenendo il verdetto riespresso corretto (stealthy) o errato (compliant).
• Tassonomia dei Fallimenti: Categorizzano i fallimenti in:
  • Stealthy (T2): Il verdetto è corretto, la conclusione è invertita.
  • Compliant (T3): Sia il verdetto che la conclusione sono invertiti.
  • Robustness (Robustezza): Il sistema resiste all'attacco.

Analisi Teorica

Il documento dimostra due teoremi chiave riguardanti il monitoraggio e l'applicazione (enforcement):

1. Teorema 1: Un monitor che controlla se la conclusione narrata corrisponde al verdetto verificato è sound e complete. Tuttavia, un monitor che controlla solo il verdetto riespresso (senza confrontarlo con la conclusione) è cieco rispetto ai fallimenti stealthy.
2. Teorema 2 & Corollario 3: Un monitor sound e complete esiste se e solo se esiste un enforcer (attuatore) sound e complete. L'unica configurazione che garantisce tassi di inversione pari a zero è un enforcer che bypassa completamente la narrazione dell'LLM, outputtando direttamente il verdetto mappato ($\rho(v)$).

Configurazione Sperimentale

• Oracle: Z3 solver utilizzato come verità fondamentale per le istanze SAT/UNSAT.
• Modelli: Sono stati valutati cinque modelli open-source: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B e DeepSeek-R1-8B.
• Vettori di Attacco: Sono stati testati quattro template di iniezione attraverso due canali (incorporati nella formula vs. in una nota separata) e due stili (blatant/esplicito vs. subtle/social engineering).
• Difesa: È stato testato un prompt di sistema "indurito" (hardened), che istruisce l'LLM a trattare gli input non attendibili come tali e a dare priorità al verdetto verificato.
• Attacchi Adattivi: Sono stati simulati attaccanti che conoscevano il prompt di difesa e hanno creato iniezioni specifiche per aggirarlo.

3. Risultati Chiave

Correttezza del Verdetto (RQ1)

Quando il certificato del solver funge da gate per la risposta finale (costringendo il sistema a outputtare il verdetto verificato), il sistema raggiunge il 100% di correttezza. Ciò conferma che la componente del solver è sound e che la vulnerabilità risiede strettamente nella narrazione dell'LLM.

Inversione della Narrazione Avversaria (RQ2)

Senza difese, gli avversari riescono a invertire la risposta narrata nella maggior parte dei casi:

• Tassi di Successo: I tassi di successo dell'iniezione sono variati da 0,47 a 0,71 tra i diversi template.
• Stealthiness (Furtività): I fallimenti "stealthy" (dove l'LLM riespone correttamente il verdetto ma inverte la conclusione) sono stati molto prevalenti. Ad esempio, il template note_social (una nota sottile senza comandi imperativi) ha ottenuto un tasso di successo complessivo di 0,71, di cui 0,39 erano stealthy.
• Varianza dei Modelli: I modelli di ragionamento (gpt-oss) non sono stati immuni, mostrando un'alta suscettibilità (0,91 di tasso di successo complessivo). Modelli non orientati al ragionamento come Qwen hanno mostrato maggiore resistenza agli attacchi espliciti, ma sono rimasti vulnerabili a quelli sottili.
• Risultato Chiave: Le iniezioni sottili sono state statisticamente efficaci quanto quelle esplicite. La vulnerabilità è un fallimento della fedeltà nel trasferimento dal verdetto alla risposta, non semplicemente un fallimento nel seguire comandi espliciti.

Efficacia della Difesa (RQ3)

• Hardening del Prompt: L'indurimento del prompt di sistema del narratore ha ridotto il tasso di successo dell'iniezione complessivo da 0,61 a 0,14 (una riduzione di circa 4 volte).
• Limitazioni:
  • L'hardening ha ridotto principalmente i fallimenti compliant (dove il modello disobbedisce apertamente) ma ha avuto un impatto minimo sui fallimenti stealthy. Il tasso di fallimenti stealthy è sceso solo da 0,57 a 0,53 tra gli attacchi rimanenti.
  • Attacchi Adattivi: Quando gli attaccanti hanno adattato i loro prompt per contrastare il sistema indurito (es. negando esplicitamente l'avviso di "input non attendibile"), il tasso di successo è tornato significativamente alto (es. note_adaptive_supersede è salito a 0,43).
  • Dipendenza dal Modello: L'efficacia della difesa variava enormemente a seconda del modello (es. Qwen è sceso a 0,01, mentre gpt-oss è rimasto a 0,26).

4. Contributi Chiave

1. Modellazione Formale: Il documento modella formalmente il ciclo LLM-solver come una procedura decisionale, identificando il passaggio di narrazione come il punto specifico in cui le garanzie di correttezza vanno perse.
2. Misurazione Sistematica: Fornisce la prima misurazione sistematica del "narration gap", dimostrando che le iniezioni avversarie possono invertire conclusioni verificate attraverso varie formulazioni e canali.
3. Limiti Teorici della Difesa: Gli autori dimostrano che l'indurimento del prompt e il monitoraggio a runtime sono insufficienti per eliminare i fallimenti stealthy. Dimostrano che solo l'enforcement (output diretto del verdetto mappato $\rho(v)$) può garantire la correttezza end-to-end.
4. Evidenza Empirica: Attraverso estesi esperimenti su cinque modelli, il documento mostra che anche i modelli capaci di ragionamento sono suscettibili di invertire conclusioni verificate e che l'ingegneria sociale sottile è efficace quanto quella esplicita.

5. Significato e Rivendicazioni

Il documento sostiene che il narration gap è una proprietà fondamentale delle pipeline neurosimboliche che si affidano agli LLM per tradurre risultati formali in linguaggio naturale.

• Il Certificato non è Sufficiente: Un certificato formale garantisce la correttezza del verdetto, ma non garantisce la correttezza della risposta all'utente se tale risposta è generata da un LLM.
• Invisibilità del Fallimento: I fallimenti più pericolosi sono quelli "stealthy", in cui il sistema sembra funzionare correttamente (riespone il verdetto corretto) pur fornendo una conclusione errata. Questi fallimenti sono invisibili ai monitor che controllano solo il verdetto.
• Strategia di Mitigazione: Il documento sostiene che fare affidamento sul prompt engineering o su istruzioni indurite non è una difesa affidabile contro avversari adattivi. L'unica soluzione robusta per query decidibili è rimuovere l'LLM dal passaggio di generazione della conclusione e imporre la risposta direttamente dal verdetto verificato.
• Generalizzabilità: Sebbene testato su problemi SAT, gli autori affermano che questo divario si applica a qualsiasi pipeline (SMT, Dimostratori di Teoremi Interattivi) in cui un risultato verificato viene narrato da un LLM.

Gli autori concludono che per le applicazioni critiche per la sicurezza, la responsabilità della pipeline si sposta dal garantire che la formalizzazione sia fedele al garantire che la narrazione sia imposta (enforced), piuttosto che fidarsi che l'LLM riporti fedelmente l'output del solver.