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

Cet article présente un cadre de vérification neurosymbolique utilisant des solveurs SMT pour auditer de manière déterministe la cohérence logique des rapports générés par des modèles vision-langage en radiologie, éliminant ainsi les hallucinations et garantissant la validité clinique des conclusions diagnostiques.

L'essentiel

🏥 Le Problème : L'Assistant Radiologue qui "Rêve"

Imaginez que vous avez engagé un assistant très intelligent pour vous aider à rédiger des rapports médicaux à partir de radiographies (des photos des poumons). Cet assistant, appelé un "modèle de langage vision" (VLM), est capable de décrire ce qu'il voit avec un français parfait et très fluide.

Le souci ? Cet assistant est un peu comme un écrivain créatif qui a trop lu de romans policiers.

• Il voit une tache sur la photo (un fait réel).
• Mais au lieu de dire simplement "il y a une tache", il peut inventer une conclusion dramatique ("c'est une pneumonie grave !") sans avoir vraiment les preuves logiques pour le soutenir.
• Ou alors, il voit la preuve, mais oublie de la mentionner dans sa conclusion.

C'est ce qu'on appelle une hallucination ou une incohérence logique. En médecine, dire "je pense que c'est grave" sans preuve est dangereux. Les méthodes actuelles pour vérifier ces rapports (comparer le texte à un rapport humain) sont comme vérifier si deux phrases se ressemblent : elles ne détectent pas si le raisonnement est faux.

---

🕵️‍♂️ La Solution : Le Détective Mathématique (Vérification Neurosymbolique)

Les chercheurs de cette étude ont créé un système de vérification automatique qui agit comme un détective mathématique ou un gardien de la logique.

Voici comment cela fonctionne, étape par étape, avec une analogie :

1. Le Traducteur (De la parole aux mathématiques)

L'assistant écrit son rapport en langage naturel (ex: "l'angle costophrenique est émoussé").
Le système prend ce texte et le traduit instantanément en un langage de logique pure (comme un code binaire ou des équations mathématiques).

• Analogie : C'est comme si un traducteur prenait une lettre poétique et la transformait en une liste de faits bruts et vérifiables : "Fact A = Vrai", "Fact B = Faux".

2. Le Livre des Règles (La Base de Connaissances)

Le système possède un manuel de règles médicales très strict, vérifié par de vrais médecins.

• Exemple de règle : "SI 'l'angle costophrenique est émoussé' EST VRAI, ALORS 'il y a un épanchement pleural' EST OBLIGATOIREMENT VRAI."

3. Le Juge Mathématique (Le Solveur Z3)

C'est ici que la magie opère. Le système utilise un outil mathématique puissant (un "solveur SMT") pour poser une question simple :

"Est-ce que les faits observés (l'évidence) obligent mathématiquement à conclure ce diagnostic ?"

Le système ne se fie pas à l'intuition, il fait un calcul de vérité absolue.

---

🚦 Les Trois Scénarios Possibles

Grâce à ce détective, on peut classer les rapports en trois catégories claires :

1. Le Rapport Solide (Entailment) :

   • Analogie : Vous avez vu un gâteau sur la table. Vous dites "Il y a un gâteau".
   • Résultat : Le détective dit "C'est logique !". ✅

2. L'Hallucination (Hallucination) :

   • Analogie : Vous voyez une chaise vide. Pourtant, l'assistant écrit "Il y a un gâteau sur la table".
   • Résultat : Le détective dit "Faux ! Rien ne prouve le gâteau". ❌ Le système rejette cette affirmation.

3. L'Oubli (Omission) :

   • Analogie : Vous voyez un gâteau, mais l'assistant oublie de le mentionner dans sa conclusion.
   • Résultat : Le détective dit "Attends, tu as vu le gâteau, tu devrais le dire !". ⚠️ Le système signale l'oubli.

---

📊 Les Résultats : Pourquoi c'est important ?

Les chercheurs ont testé ce système sur 7 assistants différents et 5 bases de données de radiographies.

• Les anciennes méthodes (comparer les mots) pensaient que les rapports étaient bons s'ils ressemblaient à des rapports humains. Résultat : elles ne voyaient pas les erreurs de logique.
• Le nouveau système a révélé que beaucoup d'assistants "rêvent" (inventent des diagnostics) ou sont trop prudents (oublient des diagnostics évidents).

Le plus gros avantage ?
Si on utilise ce système comme un filtre de sécurité avant de montrer le rapport au médecin :

• On élimine les mensonges (les diagnostics inventés sans preuve).
• On augmente la fiabilité (la précision).
• On accepte un tout petit risque de manquer quelques détails (pour être sûr de ne pas mentir).

💡 En Résumé

Imaginez que vous construisez une maison. Les modèles actuels sont comme des architectes qui dessinent de très beaux plans, mais qui oublient parfois de vérifier si les murs portent bien le toit.

Ce papier propose d'installer un ingénieur de contrôle qualité automatique qui vérifie, grâce aux mathématiques, que chaque mur soutient bien le toit avant que le bâtiment ne soit livré. Cela ne remplace pas l'architecte, mais cela garantit que la maison ne s'effondrera pas à cause d'une erreur de logique.

C'est une étape cruciale pour rendre l'Intelligence Artificielle sûre et digne de confiance dans les hôpitaux.

Résumé technique

1. Problématique

L'adoption des modèles vision-langage (VLM) en radiologie pour la rédaction de rapports préliminaires se heurte à une vulnérabilité fondamentale : l'absence de garanties formelles de validité logique.

• Incohérences logiques : Les VLM, optimisés pour la fluidité textuelle (génération probabiliste de tokens), produisent souvent des rapports où les "Impressions" (diagnostics) ne sont pas déductivement soutenues par les "Constats" (observations visuelles), ou inversement, omettent des conclusions logiquement forcées.
• Limites des métriques actuelles : Les métriques d'évaluation standard (BLEU, ROUGE) se basent sur la similarité lexicale avec un rapport de référence. Elles pénalisent le paraphrase clinique équivalent et, plus grave, échouent à détecter les erreurs de déduction interne (ex: un rapport fluent mais contradictoire) en l'absence de vérité terrain.
• Risque clinique : Cette "illusion de raisonnement" crée un risque de biais d'automatisation, où les cliniciens pourraient faire confiance à des diagnostics générés mais non validés logiquement.

2. Méthodologie : Cadre Neurosymbolique de Vérification

Les auteurs proposent un pipeline de vérification qui découple la perception visuelle (probabiliste) du raisonnement clinique (déterministe) en utilisant une approche neurosymbolique.

A. Fondement Ontologique et Auto-formalisation

• Ontologie ($O$) : Définition d'un ensemble d'observations atomiques ($F$) et de diagnostics ($D$), reliés par une base de connaissances cliniques ($K$) sous forme de règles propositionnelles (ex: $d \Rightarrow \neg d'$).
• Auto-formalisation ($T$) : Une fonction (implémentée via un LLM contraint) transforme le texte libre des "Constats" ($R_F$) en un vecteur d'état binaire $V$. Sous l'hypothèse de monde clos (CWA), les findings non mentionnés sont considérés comme absents.
• Extraction : Les diagnostics de l'"Impression" ($R_I$) sont extraits via un appariement de chaînes strict.

B. Vérification par Satisfiabilité (SAT/SMT)

Le problème de vérification est formulé comme un problème de satisfiabilité logique :

1. Le contexte propositionnel $\Phi_V$ est construit à partir des findings observés.
2. Pour chaque diagnostic affirmé $d$ dans l'impression, le système vérifie si $d$ est une conséquence logique de $\Phi_V$ couplé à la base de connaissances $K$ ($\Phi_V \land K \models d$).
3. Utilisation du solveur Z3 (SMT) pour vérifier la satisfiabilité de la négation de la conclusion : IsSat(ΦV ∧ K ∧ ¬d).

C. Taxonomie des Erreurs

Le système classe les diagnostics en quatre catégories :

1. Soutenu (Entailment) : La conclusion est logiquement forcée par les preuves (Vérification = Unsat).
2. Non soutenu (Hallucination) : La conclusion est affirmée mais n'est pas forcée par les preuves (Vérification = Sat).
3. Manquant (Omission) : La conclusion est logiquement forcée mais absente du rapport.
4. Correctement exclu : La conclusion n'est ni forcée ni affirmée.

3. Contributions Clés

1. Cadre de vérification sans référence : Un système capable d'auditer la cohérence interne d'un rapport radiologique sans avoir besoin d'un rapport de référence humain (ground truth), en reliant la génération textuelle probabiliste à la logique déterministe.
2. Révélation de modes d'échec invisibles : Identification de trois profils de défaillance des VLM (observateurs conservateurs, hallucinations stochastiques, modèles équilibrés) que les métriques lexicales ne peuvent pas détecter.
3. Garantie post-hoc : Démonstration que l'application d'un solveur SMT comme filtre de sécurité élimine systématiquement les hallucinations non soutenues, augmentant la précision et la validité diagnostique.

4. Résultats Expérimentaux

L'évaluation a porté sur 7 VLM (généraux et médicaux) sur 5 benchmarks de radiographie thoracique (MIMIC-CXR, CheXpert, NIH-CXR, etc.).

• Échec des métriques lexicales : Les scores BLEU et ROUGE sont proches de zéro, confirmant leur inadéquation pour évaluer la qualité du raisonnement clinique.
• Audit de cohérence interne (Sans référence) :
  • Les modèles varient considérablement. MedGemma-27B montre un bon équilibre entre justesse (Soundness) et complétude.
  • Qwen3-VL-8B est très "conservateur" (Soundness élevée, mais oublie souvent des diagnostics forcés).
  • Llava-Vicuna-7B présente une forte stochasticité (faible précision et complétude), générant des impressions non fondées.
• Impact du filtrage symbolique (Sur données étiquetées) :
  • L'application du filtre de vérification augmente systématiquement la Soundness (de 0,90 à >0,96) et la Précision.
  • Il en résulte une légère baisse de la Complétude et du Rappel (Recall), car certains diagnostics correspondant à la vérité terrain sont supprimés si les preuves dans le texte des "Constats" ne les soutiennent pas formellement.
  • Ce compromis est jugé acceptable pour des applications critiques, car il élimine les faux positifs non justifiés.

5. Signification et Conclusion

Cet article marque un changement de paradigme dans l'évaluation des IA médicales : passer d'une similarité de surface (texte vs texte) à une vérification de cohérence interne (texte vs logique).

• Sécurité : Le cadre offre des garanties formelles de type "assume-guarantee", où la validité du diagnostic est prouvée mathématiquement par rapport aux observations déclarées.
• Auditabilité : Il permet de détecter et de corriger les hallucinations de manière transparente, rendant les assistants cliniques génératifs plus sûrs et auditable.
• Futur : Cette approche neurosymbolique ouvre la voie à des systèmes où le raisonnement clinique est vérifiable, réduisant la charge cognitive des radiologues et minimisant les risques d'erreurs de diagnostic dues à l'IA.

En résumé, les auteurs démontrent que l'intégration de solveurs de contraintes logiques (SMT) dans le pipeline des VLM est une étape nécessaire pour transformer ces modèles de générateurs de texte probabilistes en assistants cliniques fiables et déductivement valides.