Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification

Questo lavoro introduce un framework di verifica neuro-simbolica che utilizza un risolutore SMT e una base di conoscenze cliniche per garantire la coerenza logica e l'assenza di allucinazioni nei rapporti radiologici generati da modelli visione-linguaggio, superando i limiti delle metriche lessicali tradizionali.

L'essenziale

Immagina di avere un assistente medico digitale molto intelligente, capace di guardare una radiografia del torace e scrivere il rapporto per il dottore. Questo assistente è un'intelligenza artificiale chiamata "Vision-Language Model" (VLM). Sembra perfetto: parla bene, usa termini medici corretti e sembra molto sicuro di sé.

Tuttavia, c'è un problema nascosto: a volte l'assistente mente o si contraddice da solo, anche se lo fa con molta sicurezza.

Ecco di cosa parla questo articolo, spiegato come se stessimo chiacchierando al bar:

1. Il Problema: L'Assistente che "Allucina"

Immagina che il tuo assistente guardi una radiografia e scriva nella sezione "Osservazioni": "Vedo un angolo del polmone un po' schiacciato".
Poi, nella sezione "Diagnosi", scrive: "Il paziente ha un versamento pleurico grave".

Per un medico umano, questo ha senso: l'angolo schiacciato significa versamento. Ma per l'IA, a volte non c'è un vero collegamento logico.

• Scenario A (L'errore silenzioso): L'IA vede l'angolo schiacciato ma dimentica di scrivere la diagnosi nel rapporto finale.
• Scenario B (L'allucinazione): L'IA inventa una diagnosi grave (es. "tumore") anche se nelle osservazioni non ha scritto nulla che lo giustifichi. Lo fa solo perché "pensa" che sia probabile, basandosi su ciò che ha letto nei suoi libri di testo, non su ciò che vede in quel momento.

I metodi tradizionali per controllare queste IA (che confrontano le parole usate con quelle di un rapporto umano perfetto) falliscono qui. Se l'IA dice "c'è un po' di liquido" invece di "versamento pleurico", i vecchi sistemi pensano che sia sbagliata, anche se il significato è lo stesso. E se l'IA inventa una malattia, i vecchi sistemi non se ne accorgono se le parole sono grammaticalmente corrette.

2. La Soluzione: Il "Controllore Logico" (Verifica Neuro-Simbolica)

Gli autori di questo studio hanno creato un controllore di sicurezza che funziona come un detective matematico. Non si fida delle parole, ma della logica.

Ecco come funziona il loro sistema, passo dopo passo:

1. Traduzione in Matematica: L'IA scrive il rapporto in linguaggio umano. Il sistema prende queste parole e le traduce in un linguaggio di logica pura (come se trasformasse una storia in un'equazione matematica).
   • Esempio: "Angolo schiacciato" diventa la variabile A = VERO.
2. Il Libro delle Regole (La Base di Conoscenza): Hanno creato un "libro delle regole mediche" digitale.
   • Regola: "SE A = VERO, ALLORA Diagnosi_Versamento = VERO".
3. Il Detective (Il Solvitore Z3): Qui entra in gioco il vero eroe: un software chiamato Z3. È un detective matematico infallibile. Prende le osservazioni (A=VERO) e la regola (Se A allora B) e chiede: "È matematicamente possibile che A sia vero e B sia falso?".
   • Se la risposta è NO (impossibile), allora la diagnosi è garantita.
   • Se la risposta è SÌ (è possibile), allora la diagnosi è inventata (un'allucinazione) o manca una prova.

3. Cosa hanno scoperto?

Hanno fatto fare il test a 7 diversi assistenti IA su migliaia di radiografie. Il loro "detective matematico" ha scoperto cose che nessuno aveva mai visto prima:

• I "Timidi": Alcuni assistenti sono così prudenti che non inventano mai nulla, ma spesso dimenticano di scrivere diagnosi che avrebbero dovuto dedurre (come un detective che vede il colpevole ma non osa accusarlo).
• I "Sognatori": Altri assistenti sono molto creativi ma pericolosi. Inventano diagnosi gravi senza alcuna prova nelle osservazioni.
• I "Equilibrati": Alcuni (come MedGemma-27B) sono molto bravi a collegare le osservazioni alle conclusioni.

4. Il Risultato: Un Filtro di Sicurezza

La parte più bella è che questo sistema può essere usato come un filtro di sicurezza dopo che l'IA ha scritto il rapporto.
Prima di mostrare il rapporto al dottore, il sistema controlla: "Questa diagnosi è supportata da ciò che hai scritto prima?".

• Se sì: Approvato.
• Se no (è un'allucinazione): Cancellato.

Il risultato?
Il rapporto finale diventa molto più sicuro. L'IA smette di inventare malattie (aumenta la precisione) e dice solo quello che può dimostrare. Certo, a volte potrebbe essere un po' più "cauto" e non scrivere una diagnosi che avrebbe potuto indovinare (perde un po' di "completezza"), ma in medicina è meglio essere cauti che inventare.

In Sintesi

Immagina di avere un segretario che scrive le tue note. A volte scrive cose che non hai detto. Questo nuovo sistema è come un segretario secondario che legge tutto e dice: "Ehi, nel primo paragrafo non hai detto che pioveva, quindi non puoi scrivere nel secondo paragrafo che abbiamo preso l'ombrello!".

Questo trasforma l'IA da un "generatore di testo fluido" (che può mentire) a un "assistente logico verificabile" (che deve avere prove per ogni affermazione), rendendo l'uso dell'IA in ospedale molto più sicuro e affidabile.

Sommario tecnico

1. Il Problema: L'Assenza di Garanzie Formali nel Ragionamento Clinico

I modelli Vision-Language (VLM) mostrano un grande potenziale nella stesura di referti radiologici, ma soffrono di una vulnerabilità fondamentale: la mancanza di garanzie formali sulla correttezza logica.

• Incoerenza Logica: I VLM spesso generano impressioni diagnostiche non supportate dalle proprie osservazioni percettive (allucinazioni) o omettono conclusioni logicamente necessarie.
• Limiti delle Metriche Attuali: Le metriche NLP standard (BLEU, ROUGE) si basano sulla similarità lessicale rispetto a un testo di riferimento ("ground truth"). Queste falliscono nel catturare errori deduttivi, penalizzano la parafrasi clinica e non offrono garanzie di sicurezza in scenari reali dove il ground truth non è disponibile.
• Natura Probabilistica: I VLM sono ottimizzati per la fluidità testuale (massimizzazione della probabilità del token successivo) piuttosto che per la validità deduttiva, creando un "illusione di ragionamento" pericolosa in contesti critici come la medicina.

2. Metodologia: Un Framework Neuro-Simbolico di Verifica

Gli autori propongono un framework che decoupla la percezione visiva (probabilistica, gestita dal VLM) dal ragionamento clinico (deterministico, verificato da un solver simbolico). Il processo si articola in tre fasi principali:

A. Fondazione Ontologica e Autoformalizzazione

• Viene definita un'ontologia formale leggera $O = \langle F, D, K \rangle$, dove $F$ sono le osservazioni atomiche (es. "angolo costofrenico ottuso"), $D$ le diagnosi e $K$ la base di conoscenza clinica (regole proposizionali).
• Una funzione di autoformalizzazione ($T$) converte il testo libero delle "Osservazioni" (Findings) in un vettore di evidenze strutturato binario ($V \in \{0, 1\}$), assumendo che le osservazioni non menzionate siano assenti (Closed-World Assumption).
• Le diagnosi nell'"Impressione" (Impression) vengono estratte tramite matching stringato su schema.

B. Verifica tramite Soddisfacibilità (SMT)

Il problema di verifica viene formulato come un problema di soddisfacibilità booleana (SAT) utilizzando il solver Z3:

• Si costruisce un contesto proposizionale $\Phi_V$ basato sulle evidenze estratte.
• Per ogni diagnosi $d$ affermata nel referto, si verifica se $d$ è una conseguenza logica di $\Phi_V \land K$.
• Il solver controlla la soddisfacibilità della negazione: IsSat(ΦV ∧ K ∧ ¬d).
  • Se Unsat: La diagnosi è Supportata (logicamente necessaria).
  • Se Sat: La diagnosi è Non Supportata (allucinazione).
  • Se una diagnosi necessaria è assente, è Mancata (omissione).

C. Valutazione Reference-Free

Il sistema introduce metriche di affidabilità deduttiva che non richiedono un testo di riferimento umano:

• Soundness (Correttezza): La proporzione di diagnosi generate che sono logicamente supportate dalle osservazioni.
• Completeness (Completezza): La proporzione di diagnosi logicamente necessarie che vengono effettivamente verbalizzate.

3. Contributi Chiave

1. Framework Neuro-Simbolico Reference-Free: Un sistema che mappa il testo libero in vincoli SMT tramite un'ontologia clinica, permettendo la verifica automatica della logica diagnostica senza dipendere da testi di riferimento.
2. Identificazione di Modalità di Fallimento: L'audit formale su 7 VLM e 5 benchmark ha rivelato errori deduttivi specifici (osservazione conservativa, allucinazione stocastica) invisibili alle metriche tradizionali.
3. Garanzie Post-Hoc: Dimostrazione che l'applicazione di un solver SMT come filtro a posteriori elimina sistematicamente le allucinazioni non supportate, migliorando la precisione e la correttezza diagnostica.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su dataset come MIMIC-CXR, CheXpert e NIH-CXR, utilizzando modelli come MedGemma, LLaVA-Med e Qwen3-VL.

• Fallimento delle Metriche Lessicali: I punteggi BLEU e ROUGE sono risultati prossimi allo zero, confermando che la similarità testuale non riflette la qualità del ragionamento clinico.
• Analisi dei Modelli:
  • Modelli Conservativi (es. Qwen3-VL-8B): Alta Soundness (raramente allucinano), ma bassa Completeness (omettono diagnosi necessarie).
  • Modelli Stocastici (es. Llava-Vicuna-7B): Bassa Soundness e Completeness, trattano il compito come generazione statistica di testo.
  • Modelli Bilanciati (es. MedGemma-27B): Elevate prestazioni sia in correttezza che in completezza.
• Impatto del Filtro Simbolico: Applicando il filtro di verifica sui dataset etichettati:
  • La Soundness è aumentata in modo consistente per tutti i modelli (es. da ~0.90 a ~0.96).
  • La Precisione è migliorata significativamente.
  • C'è stata una lieve riduzione nella Completeness e nel Recall, poiché il sistema rimuove le diagnosi non sufficientemente supportate dalle evidenze estratte, ma questo trade-off è considerato accettabile per la sicurezza clinica.

5. Significato e Implicazioni

Questo lavoro rappresenta un passo cruciale verso l'adozione sicura dei VLM in ambito medico:

• Transizione Epistemologica: Sposta il paradigma di valutazione dalla similarità superficiale del testo alla coerenza interna verificabile.
• Sicurezza Clinica: Fornisce un meccanismo di "safety guard" (guardia di sicurezza) che garantisce che le conclusioni diagnostiche siano matematicamente dedotte dalle osservazioni, riducendo il rischio di bias di automazione.
• Auditabilità: Offre un approccio pratico per rendere i sistemi generativi clinici più trasparenti e auditabili, soddisfacendo i requisiti di "assume-guarantee" tipici della verifica formale.

In sintesi, il paper dimostra che integrare la logica simbolica e i solver SMT nei flussi di lavoro dei VLM permette di trasformare i referti radiologici da testi probabilistici a documenti clinicamente validati, eliminando le allucinazioni logiche che le metriche tradizionali non riescono a rilevare.