通过形式验证为视觉语言模型中的临床推理提供保证
Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification
AI总结：
通过形式验证框架，为视觉语言模型的临床推理提供保证，验证诊断主张的数学推导性，提升生成临床助手的正确性和精度。
摘要：
视觉语言模型（VLMs）在撰写放射学报告方面展现出潜力，但它们经常出现逻辑不一致的问题，生成的诊断印象缺乏自身感知发现的支持或遗漏了逻辑上可推导的结论。标准的词法度量对临床改写极为严厉，无法在无参考的情况下捕捉这些演绎失败。为了为临床推理提供保证，我们引入了一个神经符号验证框架，该框架确定性地审计VLM生成报告的一致性。我们的流程将自由文本的放射学发现自动形式化为结构化的命题证据，利用SMT求解器（Z3）和临床知识库来验证每个诊断主张是否在数学上被推导、虚构或遗漏。在五个胸部X光基准上评估七种VLMs，我们的验证器揭示了不同的推理失败模式，如保守观察和随机虚构，这些模式在传统度量中是不可见的。在标记数据集上，强制求解器支持的推导作为严格的后验保证，系统地消除不支持的虚构，显著提高生成临床助手的诊断正确性和精度。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
