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

Este artigo apresenta um quadro de verificação neurosimbólico que utiliza solvers SMT e bases de conhecimento clínico para auditar a consistência lógica de relatórios radiológicos gerados por modelos de visão e linguagem, eliminando alucinações e garantindo a validade dedutiva das conclusões diagnósticas.

O essencial

Imagine que você tem um assistente de inteligência artificial muito inteligente, capaz de olhar para uma radiografia de tórax e escrever um relatório médico. Ele é tão bom que parece um médico de verdade: usa palavras técnicas, frases complexas e soa muito confiante.

O problema é que, às vezes, esse assistente é como um ator de teatro brilhante, mas que esqueceu o roteiro. Ele pode descrever perfeitamente o que vê na imagem (ex: "o ângulo da costela está apagado"), mas na conclusão do relatório, ele inventa uma doença que não tem nada a ver com o que descreveu, ou esquece de mencionar uma doença que obrigatoriamente deveria estar lá.

Aqui está a explicação do que os autores desse artigo fizeram, usando uma analogia simples:

O Problema: O "Alucinação" do Assistente

Hoje, para saber se esse assistente está bom, os cientistas usam regras simples de comparação de texto (como contar quantas palavras iguais ele usou em relação a um relatório de um médico humano).

• A falha: Se o assistente diz "o pulmão está inchado" e o médico humano escreveu "há um derrame pleural", os computadores antigos acham que estão errados porque as palavras são diferentes, mesmo que o significado seja o mesmo.
• O perigo: Se o assistente diz "não vejo nada errado" na descrição, mas na conclusão diz "o paciente tem pneumonia", os antigos computadores não percebem essa contradição lógica. Eles só olham para as palavras, não para a lógica.

A Solução: O "Detetive Lógico" (Verificação Formal)

Os autores criaram um novo sistema, chamado Verificador Neurosimbólico. Pense nele como um detetive lógico ou um inspetor de qualidade que trabalha em tempo real.

O processo funciona em três etapas, como uma linha de montagem:

1. O Tradutor (Autoformalização):
   O relatório escrito pelo assistente (que é texto livre e bagunçado) é traduzido para uma "linguagem de lógica pura".

   • Analogia: É como transformar um poema confuso em uma equação matemática simples. "O ângulo da costela está apagado" vira uma variável X = Verdadeiro.

2. O Livro de Regras (Base de Conhecimento):
   Eles criaram um "livro de regras" médico, validado por especialistas.

   • Analogia: É como um manual de instruções que diz: "SE X (ângulo apagado) for verdadeiro, ENTÃO Y (derrame pleural) é obrigatoriamente verdadeiro".

3. O Juiz Matemático (SMT Solver Z3):
   Aqui entra a mágica. Um software matemático (o Z3) pega a equação do relatório e as regras do livro e pergunta: "Isso faz sentido?"

   • Ele não compara com um humano. Ele verifica a consistência interna.
   • Se o assistente diz "X é verdade" e conclui "Z é verdade", mas a regra diz "X só leva a Y", o Juiz grita: "ALERTA! Isso é uma alucinação! A conclusão não é apoiada pelo que foi dito antes!"

O Que Eles Descobriram?

Ao testar 7 assistentes diferentes, eles viram que a maioria estava "mentindo" de formas que os testes antigos não viam:

• O Conservador: Alguns assistentes tinham medo de errar. Eles descreviam tudo corretamente, mas na conclusão diziam "não vejo nada", mesmo que a lógica dissesse que havia uma doença. Eles eram "seguros", mas inúteis (incompletos).
• O Sonhador: Outros assistentes inventavam doenças que nunca foram mencionadas na descrição. Eles eram criativos, mas perigosos (alucinações).

O Resultado Final: O "Filtro de Segurança"

O grande trunfo desse trabalho é que eles podem usar esse "Juiz Matemático" para limpar os relatórios antes de um médico humano ler.

• Se o assistente diz algo que a lógica não suporta, o sistema corta essa frase.
• Isso torna o relatório final muito mais confiável. Ele pode perder um pouquinho de detalhes (porque cortou algumas suposições), mas ganha muita segurança.

Resumo em uma frase

Os autores criaram um sistema de segurança matemática que garante que o relatório médico gerado por uma IA faça sentido lógico, impedindo que ela invente diagnósticos que contradizem o que ela mesma viu na imagem, transformando a IA de um "ator confiante" em um "assistente verificável".

Resumo técnico

1. O Problema

Os Modelos de Linguagem e Visão (VLMs) demonstram potencial para auxiliar na redação de laudos radiológicos, mas sofrem de uma vulnerabilidade fundamental: a falta de garantias formais de raciocínio lógico.

• Inconsistências Lógicas: Os VLMs frequentemente geram laudos onde as "Impressões" (diagnósticos) não são dedutivamente suportadas pelas "Achados" (evidências perceptivas) ou omitem conclusões logicamente necessárias.
• Falhas nas Métricas Atuais: As métricas padrão de Processamento de Linguagem Natural (como BLEU e ROUGE) avaliam apenas a similaridade lexical com um laudo de referência (ground truth). Elas penalizam paráfrases clinicamente equivalentes e são incapazes de detectar falhas dedutivas em cenários onde o "ground truth" não está disponível (comum na prática clínica real).
• Risco de Segurança: A natureza estocástica dos VLMs cria uma "ilusão de raciocínio", onde textos fluentes podem conter contradições lógicas perigosas, levando a vieses de automação e riscos para os pacientes.

2. Metodologia

Os autores propõem um framework de verificação neurosimbólica que desacopla a percepção visual (probabilística) do raciocínio clínico (determinístico). O pipeline funciona da seguinte forma:

1. Autoformalização (Text-to-Symbolic):
   • O texto livre gerado pelo VLM (seções de "Achados" e "Impressão") é mapeado para um domínio computável.
   • Define-se uma ontologia formal leve ($O$) contendo predicados observacionais (ex: blunted_costophrenic_angle) e diagnósticos (ex: pleural_effusion).
   • Um LLM estritamente restrito (com temperatura 0.0) converte os achados em um vetor de estado binário ($V$), assumindo que achados não mencionados são inexistentes (Hipótese de Mundo Fechado).
2. Base de Conhecimento Clínica ($K$):
   • Regras clínicas e condições suficientes para diagnósticos são extraídas de diretrizes e refinadas por clínicos, modeladas como fórmulas proposicionais.
3. Verificação via Satisfatibilidade (SAT/SMT):
   • O problema de verificação é formulado como um problema de satisfatibilidade usando o solver Z3.
   • Para cada diagnóstico $d$ na "Impressão", o sistema verifica se a conjunção dos achados formalizados ($\Phi_V$) e a base de conhecimento ($K$) implicam logicamente $d$ ($\Phi_V \land K \models d$).
   • O solver verifica a insatisfatibilidade da negação da conclusão: IsSat(ΦV ∧ K ∧ ¬d).
4. Taxonomia de Erros:
   O sistema classifica os resultados em quatro categorias:
   • Suportado (Entailed): O diagnóstico é logicamente forçado pelas evidências.
   • Não Suportado (Hallucinated): O diagnóstico é afirmado, mas não é logicamente forçado (existe um estado válido onde as evidências são verdadeiras e o diagnóstico é falso).
   • Omitido (Missed): O diagnóstico é logicamente forçado, mas não foi incluído no laudo.
   • Corretamente Excluído: Nem forçado, nem afirmado.

3. Principais Contribuições

1. Framework Neurosimbólico sem Referência: Introduz uma abordagem que valida a lógica interna dos laudos sem depender de textos de referência (ground truth), mapeando texto livre para restrições SMT via ontologia clínica.
2. Descoberta de Modos de Falha Ocultos: Ao auditar 7 VLMs em 5 benchmarks de raios-X de tórax, o método expõe falhas de raciocínio (como observação conservadora e alucinação estocástica) que métricas baseadas em sobreposição lexical não conseguem detectar.
3. Garantia Pós-Hoc Rigorosa: Demonstra que o uso de um solver SMT como filtro pós-processamento elimina sistematicamente alucinações não suportadas, aumentando a precisão e a solidez diagnóstica com um custo mínimo na sensibilidade.

4. Resultados

Os experimentos foram realizados em datasets como MIMIC-CXR, CheXpert e NIH-CXR, utilizando modelos como MedGemma, LLaVA-Med, Lingshu e Qwen3-VL.

• Ineficácia das Métricas Tradicionais: As pontuações de BLEU e ROUGE foram extremamente baixas (próximas de zero), falhando em capturar a qualidade clínica devido à penalização de paráfrases.
• Auditoria de Consistência Interna:
  • O framework revelou perfis distintos de modelos:
    • Modelos Conservadores (ex: Qwen3-VL-8B): Alta solidez (Soundness), mas baixa completude (omitem diagnósticos forçados).
    • Modelos Estocásticos (ex: Llava-Vicuna-7B): Baixa precisão e completude, gerando diagnósticos sem base nas evidências.
    • Modelos Equilibrados (ex: MedGemma-27B): Alta solidez e completude.
• Impacto do Filtro Simbólico:
  • Ao aplicar o filtro de verificação nos datasets rotulados, houve um aumento consistente na Solidez (Soundness) e Precisão para todos os modelos.
  • Houve uma redução mínima na Completude e Recall, indicando que o filtro remove principalmente diagnósticos não fundamentados, preservando a maioria das conclusões logicamente válidas.
  • Exemplo: No CheXpert, o modelo MedGemma-27B viu sua solidez aumentar de 0.9301 para 0.9599 após a verificação.

5. Significado e Conclusão

Este trabalho representa uma mudança de paradigma na avaliação de IA médica:

• Transição de Empírico para Formal: Move a validação de modelos de "similaridade de string" para "verificação de consistência interna".
• Segurança Clínica: Oferece um mecanismo de segurança (guardrail) que pode ser implantado em tempo de execução para garantir que os diagnósticos gerados por IA sejam dedutivamente válidos em relação às evidências observadas.
• Auditoria e Confiança: Estabelece um caminho para assistentes clínicos gerativos mais seguros e auditáveis, onde a confiança não é baseada apenas na fluência do texto, mas em garantias matemáticas de raciocínio, alinhando-se com os princípios de verificação formal em sistemas críticos.

Em suma, o paper demonstra que é possível auditar e melhorar o raciocínio clínico de VLMs transformando o problema de linguagem natural em um problema de lógica formal verificável, mitigando riscos de alucinação e inconsistência lógica.