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

Deze paper introduceert een neurosymbolisch verificatiekader dat de logische consistentie van door Vision-Language Models gegenereerde radiologierapporten garandeert door diagnostische claims te verifiëren met een SMT-oplosser, waardoor hallucinaties worden geëlimineerd en de klinische nauwkeurigheid wordt verbeterd.

De kern

Stel je voor dat je een zeer slimme, maar soms wat onvoorspelbare assistent-arts hebt die een computer is. Deze computer kijkt naar röntgenfoto's van longen en schrijft vervolgens een verslag voor de echte arts. Hij is snel, beleefd en schrijft vloeiende zinnen. Maar hier zit het probleem: soms zegt hij dingen die niet logisch kloppen. Hij ziet misschien een vlekje op de foto, maar schrijft in zijn conclusie dat de patiënt een gebroken bot heeft, terwijl dat nergens voor staat. Of hij ziet een duidelijk gebroken bot, maar zegt in zijn conclusie: "Ik zie niets."

Deze paper (wetenschappelijk artikel) introduceert een digitale "waarheidscontroleur" om ervoor te zorgen dat deze computer-assistent niet alleen goed klinkt, maar ook logisch correct redeneert.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. Het Probleem: De "Vlotte Leugenaar"

Huidige AI-modellen (zoals die in dit artikel getest worden) werken als een schrijver die alleen naar de volgende woordkansen kijkt. Als ze een foto zien, proberen ze een tekst te maken die klinkt als een medisch verslag.

• Het risico: Ze kunnen een heel mooi verslag schrijven dat er perfect uitziet, maar vol zit met logische fouten.
• De oude manier om dit te testen: Wetenschappers keken vroeger of de AI-tekst leek op een menselijk verslag (woorden tellen). Maar dat werkt niet goed. Als de AI schrijft "er is een beetje vocht in de longen" en de mens schrijft "er is een pleurale effusie", zijn ze hetzelfde, maar telt de computer dat als een fout. En als de AI een vreselijke logische fout maakt maar wel dezelfde woorden gebruikt, denkt de computer dat het goed is.

2. De Oplossing: De "Logische Politieagent"

De auteurs van dit artikel hebben een nieuw systeem bedacht dat ze een neuro-symbolische verificatie noemen. Laten we het vergelijken met een rechter die een getuige ondervraagt.

Het proces werkt in drie stappen:

• Stap 1: De Vertaler (Autoformalisatie)
  De AI schrijft zijn verslag in gewone taal (bijv. "De hoek van het borstvlies is afgerond"). De "rechter" (een speciaal computerprogramma) vertaalt deze zinnen direct naar een strikt logisch taal (als een wiskundige vergelijking).

  • Voorbeeld: "Afgeronde hoek" wordt omgezet in een simpele code: HOEK_AFGEROND = WAAR.

• Stap 2: De Regelboek-Check (De Kennisbank)
  Er is een digitaal boek met medische regels, gemaakt door echte artsen.

  • De regel: "ALS HOEK_AFGEROND = WAAR, DAN MOET LONGVOCHT = WAAR."
    Dit is de basis van de logica.

• Stap 3: De Rechter (De Z3 Solver)
  Nu komt de echte magie. De computer kijkt naar wat de AI heeft gezien (de feiten) en vraagt zich af: "Is de conclusie die de AI treedt, een logisch gevolg van deze feiten?"
  De computer gebruikt een wiskundige motor (een 'solver') om dit 100% zeker te maken. Er is geen gokken meer.

3. Wat Ontdekt de Rechter?

Met dit systeem kunnen ze drie soorten fouten vinden die de oude methoden nooit zagen:

1. De "Stochastische Hallucinator": De AI zegt: "De patiënt heeft longkanker," terwijl er op de foto niets staat dat daarop wijst. De rechter zegt: "Fout! Je hebt geen bewijs voor deze conclusie."
2. De "Angstige Observer": De AI ziet duidelijk longkanker op de foto, maar durft het niet in de conclusie te zetten. De rechter zegt: "Fout! Je hebt het bewijs gezien, maar je concludeert niets. Dat is ook fout."
3. De "Logische Consistente": De AI ziet het bewijs én trekt de juiste conclusie. De rechter zegt: "Goed gedaan!"

4. Het Resultaat: Een Veiligere AI

De auteurs hebben dit getest op zeven verschillende AI-modellen met duizenden röntgenfoto's.

• Ze ontdekten dat veel modellen, die op papier heel goed leken, in feite vaak logische fouten maakten.
• Door deze "rechter" na te laten kijken, konden ze de fouten eruit filteren.
• Het resultaat: De AI werd iets minder "volledig" (soms liet hij een diagnose weg als het bewijs niet 100% klopte), maar wat hij wel zei, was veel betrouwbaarder en veiliger.

Samenvattend in één zin

Stel je voor dat je een assistent hebt die verslagen schrijft; in plaats van te kijken of de tekst mooi klinkt, laat je nu een wiskundige controleur kijken of de conclusies echt logisch volgen uit de feiten, zodat je zeker weet dat de assistent niet uit zijn duim zuigt.

Dit maakt AI in de geneeskunde niet alleen slimmer, maar vooral verantwoordelijker.

Technische samenvatting

Probleemstelling

Vision-Language Models (VLM's) tonen veelbelovende resultaten bij het opstellen van radiologierapporten, maar lijden onder fundamentele tekortkomingen in klinisch redeneren. De huidige modellen genereren tekst op basis van probabilistische patronen (maximalisatie van de waarschijnlijkheid van het volgende token) in plaats van strikte logische afleiding. Dit leidt tot twee kritieke problemen:

1. Logische inconsistentie: Een model kan visuele bewijslast correct waarnemen in het "Findings"-gedeelte (bijv. "stompe costofrenische hoek"), maar faalt om de logisch noodzakelijke conclusie in het "Impression"-gedeelte te trekken (bijv. "pleurale effusie").
2. Hallucinatie: Modellen kunnen diagnoses genereren die niet worden ondersteund door de visuele waarnemingen, maar wel gebaseerd zijn op trainingspriors.

Bestaande evaluatiemethoden (zoals BLEU en ROUGE) zijn onvoldoende omdat ze puur op tekstuele overeenkomst met een referentierapport vertrouwen. Ze straffen klinisch equivalente parafrasingen onterecht af en kunnen geen interne logische consistentie detecteren, vooral niet in real-world scenario's waar geen "ground truth" beschikbaar is. Er is een urgent behoefte aan formele garanties voor klinisch redeneren om automatische bias en fouten te voorkomen.

Methodologie: Neurosymbolische Verificatie

De auteurs introduceren een neurosymbolisch verificatiekader dat probabilistische tekstgeneratie koppelt aan deterministische logische verificatie. Het proces verloopt als volgt:

1. Ontologische Grounding en Autoformalisatie:

   • Er wordt een lichtgewicht formele ontologie ($O$) gedefinieerd met observationele predikaten ($F$), diagnostische predikaten ($D$) en een klinische kennisbank ($K$).
   • De kennisbank $K$ bestaat uit propositional regels (afgeleid van klinische richtlijnen en geauditeerd door artsen) die aangeven welke diagnoses logisch volgen uit welke observaties.
   • Een autoformalisatiefunctie ($T$) zet de vrije tekst van de "Findings" om in een gestructureerde, binaire vector ($V$). Hierbij wordt aangenomen dat niet-genoemde bevindingen afwezig zijn (Closed-World Assumption).

2. Diagnostische Afleiding via Satisfiability (SAT):

   • Het rapportverificatieprobleem wordt omgezet in een formele satisfiability-probleem (SAT) met behulp van een SMT-oplosser (Z3).
   • De logische context ($\Phi_V$) wordt opgebouwd uit de geautomatiseerde bevindingen.
   • Voor elke gestelde diagnose $d$ in het "Impression"-gedeelte wordt gecontroleerd of deze logisch volgt uit de bewijslast onder de kennisbank: $\Phi_V \land K \models d$.
   • De solver controleert de satisfiabiliteit van de tegenzetting: IsSat(ΦV ∧ K ∧ ¬d).

3. Verificatie-uitkomsten:
   Het systeem classificeert elke diagnose in vier categorieën:

   • Ondersteund (Entailed): De diagnose is logisch noodzakelijk (Unsat bij tegenzetting).
   • Ondersteund niet (Hallucinated): De diagnose wordt gesteld, maar is niet logisch noodzakelijk (Sat bij tegenzetting).
   • Gemist (Omitted): De diagnose is logisch noodzakelijk maar ontbreekt in het rapport.
   • Correct uitgesloten: Geen van beide.

Belangrijkste Bijdragen

1. Referentievrij Neurosymbolisch Kader: Een systeem dat diagnostische logica automatisch verifieert zonder afhankelijk te zijn van menselijke referentieteksten, door vrije tekst om te zetten in SMT-beperkingen via een klinische ontologie.
2. Identificatie van Foutmodi: Het blootleggen van specifieke redeneringsfouten (zoals conservatief observeren versus stochastische hallucinatie) die onzichtbaar zijn voor traditionele NLP-metrics.
3. Post-hoc Veiligheidsmechanisme: Het aantonen dat het toepassen van een SMT-oplosser als filter hallucinaties systematisch elimineert, wat leidt tot een significant hogere diagnostische nauwkeurigheid en geluid (soundness).

Resultaten

De methode werd getest op zeven VLM's (waaronder MedGemma, LLaVA-varianten en Qwen) over vijf benchmarks voor borstfoto's (CXR).

• Tekstuele Metrics vs. Logica: Traditionele metrics (BLEU/ROUGE) toonden zeer lage scores en faalden in het onderscheiden van klinisch correcte maar anders geformuleerde rapporten.
• Referentievrije Audit:
  • Modellen vertoonden verschillende profielen: sommige waren conservatief (hoge 'soundness', lage 'completeness' – ze hallucineren zelden maar missen vaak noodzakelijke conclusies), terwijl andere stochastisch waren (lage precisie, frequente hallucinaties).
  • De 'Soundness' (het percentage gestelde diagnoses dat logisch onderbouwd is) varieerde van 0,95 tot 0,99, wat aangeeft dat zelfs de beste modellen nog fouten maken die door de solver worden opgepikt.
• Impact van Symbolische Filtering:
  • Op datasets met gelabelde ground truth (CheXpert, NIH-CXR) leidde het filteren van diagnoses via de solver tot een toename in precisie en soundness voor alle modellen.
  • Er was een kleine daling in 'recall' en 'completeness', omdat diagnoses die niet strikt door de gevonden bewijslast werden ondersteund, werden verwijderd. Dit is een aanvaardbare trade-off voor klinische veiligheid, omdat het het risico op ongegronde diagnoses elimineert.

Betekenis en Conclusie

Dit werk markeert een verschuiving in de evaluatie van generatieve AI in de geneeskunde: van oppervlakkige tekstovereenkomst naar verifieerbare interne consistentie.

• Veiligheid: Het biedt een formele garantie dat een gegenereerd rapport logisch samenhangend is met de waargenomen beelden, wat cruciaal is voor veilige klinische implementatie.
• Auditbaarheid: Het systeem maakt het mogelijk om fouten in het redeneerproces van AI-systemen kwantitatief te meten en te corrigeren zonder menselijke referenties.
• Toekomstperspectief: Het kader biedt een pad naar "generatieve klinische assistenten" die werken onder strikte "assume-guarantee" voorwaarden, waarbij de AI verantwoordelijk is voor de perceptie en het systeem voor de logische validatie.

Kortom, de auteurs bewijzen dat neurosymbolische verificatie een praktische en noodzakelijke stap is om het vertrouwen in AI-gestuurde radiologierapporten te vergroten en de "illusie van redeneren" te doorbreken.