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

arXiv: https://arxiv.org/abs/2602.24111 · HTML: https://mlsanity.com/paper/2602.24111/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Clinical and biomedical applications, one of 17 directions in LLM reasoning.
- Builds on 14 of its 25 references that are in the map.
- First posted on arXiv 27 Feb 2026.

## Placed in

- LLM reasoning / [Clinical and biomedical applications](https://mlsanity.com/lr/clinical-and-biomedical-applications/)
- Multimodal LLMs / vision-language models / [Medical vision-language models](https://mlsanity.com/mllm/medical-vision-language-models/)

## Builds on (most cited first, 14 of 14)

- [Learning Transferable Visual Models From Natural Language Supervision](https://mlsanity.com/paper/2103.00020/) (2021)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [CheXpert: A Large Chest Radiograph Dataset with Uncertainty Labels and Expert Comparison](https://mlsanity.com/paper/1901.07031/) (2019)
- [ChestX-ray8: Hospital-scale Chest X-ray Database and Benchmarks on Weakly-Supervised Classification and Localization of Common Thorax Diseases](https://mlsanity.com/paper/1705.02315/) (2017)
- [CheXbert: Combining Automatic Labelers and Expert Annotations for Accurate Radiology Report Labeling Using BERT](https://mlsanity.com/paper/2004.09167/) (2020)
- [Towards Generalist Biomedical AI](https://mlsanity.com/paper/2307.14334/) (2023)
- [Neural-Symbolic Learning and Reasoning: A Survey and Interpretation](https://mlsanity.com/paper/1711.03902/) (2017)
- [CheXpert Plus: Augmenting a Large Chest X-ray Dataset with Text Radiology Reports, Patient Demographics and Additional Image Formats](https://mlsanity.com/paper/2405.19538/) (2024)
- [Is Neuro-Symbolic AI Meeting its Promise in Natural Language Processing? A Structured Review](https://mlsanity.com/paper/2202.12205/) (2022)
- [Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning](https://mlsanity.com/paper/2409.17270/) (2024)
- [VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://mlsanity.com/paper/2601.20055/) (2026)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)

## Built on by (most cited first, 4 of 4)

- [Path-Lock Expert: Separating Reasoning Mode in Hybrid Thinking via Architecture-Level Separation](https://mlsanity.com/paper/2604.27201/) (2026)
- [Reliability-Gated Source Anchoring for Continual Test-Time Adaptation](https://mlsanity.com/paper/2605.14063/) (2026)
- [CausalGuard: Conformal Inference under Graph Uncertainty](https://mlsanity.com/paper/2605.21928/) (2026)
- [Physics as the label for measuring and correcting materials reasoning in multimodal models](https://mlsanity.com/paper/2609.12181/) (2026)

## Abstract (arXiv)

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.