Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Vikash Singh, Debargha Ganguly, Haotian Yu, Chengwei Zhou, Prerna Singh, Brandon Lee, Vipin Chaudhary, Gourav Datta

TL;DR

This work introduces a neurosymbolic verification framework that deterministically audits the internal consistency of VLM-generated reports, and enforces solver-backed entailment on labeled datasets to significantly increase diagnostic soundness and precision in generative clinical assistants.

Abstract

Vision-language models (VLMs) show promise in drafting radiology reports, yet they frequently suffer from logical inconsistencies, generating diagnostic impressions unsupported by their own perceptual findings or missing logically entailed conclusions. Standard lexical metrics heavily penalize clinical paraphrasing and fail to capture these deductive failures in reference-free settings. Toward guarantees for clinical reasoning, we introduce a neurosymbolic verification framework that deterministically audits the internal consistency of VLM-generated reports. Our pipeline autoformalizes free-text radiographic findings into structured propositional evidence, utilizing an SMT solver (Z3) and a clinical knowledge base to verify whether each diagnostic claim is mathematically entailed, hallucinated, or omitted. Evaluating seven VLMs across five chest X-ray benchmarks, our verifier exposes distinct reasoning failure modes, such as conservative observation and stochastic hallucination, that remain invisible to traditional metrics. On labeled datasets, enforcing solver-backed entailment acts as a rigorous post-hoc guarantee, systematically eliminating unsupported hallucinations to significantly increase diagnostic soundness and precision in generative clinical assistants.

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

TL;DR

This work introduces a neurosymbolic verification framework that deterministically audits the internal consistency of VLM-generated reports, and enforces solver-backed entailment on labeled datasets to significantly increase diagnostic soundness and precision in generative clinical assistants.

Abstract

Vision-language models (VLMs) show promise in drafting radiology reports, yet they frequently suffer from logical inconsistencies, generating diagnostic impressions unsupported by their own perceptual findings or missing logically entailed conclusions. Standard lexical metrics heavily penalize clinical paraphrasing and fail to capture these deductive failures in reference-free settings. Toward guarantees for clinical reasoning, we introduce a neurosymbolic verification framework that deterministically audits the internal consistency of VLM-generated reports. Our pipeline autoformalizes free-text radiographic findings into structured propositional evidence, utilizing an SMT solver (Z3) and a clinical knowledge base to verify whether each diagnostic claim is mathematically entailed, hallucinated, or omitted. Evaluating seven VLMs across five chest X-ray benchmarks, our verifier exposes distinct reasoning failure modes, such as conservative observation and stochastic hallucination, that remain invisible to traditional metrics. On labeled datasets, enforcing solver-backed entailment acts as a rigorous post-hoc guarantee, systematically eliminating unsupported hallucinations to significantly increase diagnostic soundness and precision in generative clinical assistants.
Paper Structure (10 sections, 4 equations, 2 figures, 3 tables)

This paper contains 10 sections, 4 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Methodology
  3. Ontological Grounding and Autoformalization
  4. Diagnostic Entailment via Satisfiability
  5. Experiments and Analysis
  6. Datasets and VLMs
  7. Baseline: Lexical Overlap
  8. Reference-Free Auditing of Internal Consistency
  9. Impact of Symbolic Filtering (on Labeled Datasets)
  10. Conclusion

Figures (2)

  • Figure 1: Neurosymbolic verification pipeline. A VLM generates Findings and Impression text, which are autoformalized into structured evidence and checked against a clinical knowledge base using Z3 to verify clinical reasoning.
  • Figure 2: Heatmap of model performance under neurosymbolic auditing across precision, recall, F1, soundness, completeness, and specificity, revealing distinct reasoning profiles across VLM families.