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

Each language version is independently generated for its own context, not a direct translation.

Imagina que tienes un asistente médico muy inteligente, pero un poco distraído, capaz de mirar una radiografía de tórax y escribir un informe médico. Este asistente es una "Inteligencia Artificial" (específicamente un modelo de lenguaje visión).

El problema es que, aunque este asistente escribe con una gramática perfecta y suena muy profesional, a veces alucina (inventa cosas que no están ahí) o olvida conclusiones obvias. Es como si un detective viera una huella dactilar en la escena del crimen (el hallazgo), pero en su informe final (la impresión) acusara a alguien que no tiene nada que ver, o simplemente no mencionara al culpable real.

Hasta ahora, para evaluar si estos informes eran buenos, los expertos comparaban el texto generado con otro texto escrito por un humano, contando cuántas palabras coincidían. Pero esto es como juzgar un ensayo solo por la ortografía: si el asistente escribe "el corazón está agrandado" y el humano escribió "cardiomegalia", las palabras son diferentes, pero el significado es el mismo. Las métricas tradicionales castigan esto injustamente y no detectan si la lógica del informe tiene sentido.

La Solución: El "Juez Lógico" (Verificación Formal)

Los autores de este paper proponen una solución brillante: en lugar de solo comparar palabras, construyen un sistema de verificación lógico, como un juez muy estricto que no se deja engañar por la belleza del texto.

Aquí te explico cómo funciona con una analogía sencilla:

1. El Traductor (Autoformalización)

Primero, el sistema toma el texto libre del asistente (ej. "se ve un borde borroso en la base del pulmón") y lo traduce a un lenguaje de lógica matemática (como un código binario: "Sí, hay un borde borroso"). Imagina que es como convertir una historia contada en voz alta a una ecuación matemática precisa.

2. El Juez (El Solucionador SMT)

Luego, entra en acción un "juez" digital (un programa llamado Z3). Este juez tiene un libro de reglas médicas (una base de conocimientos) que dice cosas como:

Regla: "Si hay un borde borroso en la base del pulmón, entonces debe haber líquido en el pulmón (derrame pleural)."

El juez compara lo que el asistente vio (la ecuación) con lo que el asistente diagnosticó en la conclusión.

3. Los Tres Veredictos

El juez puede dar tres tipos de veredictos sobre el diagnóstico del asistente:

✅ Lógico (Soportado): El asistente vio el borde borroso y dijo "derrame pleural". ¡Correcto! La lógica es sólida.
❌ Alucinación (No soportado): El asistente vio el borde borroso, pero dijo "tengo un tumor". El juez revisa las reglas, ve que no hay evidencia para el tumor y grita: ¡Falso! Esto es una alucinación.
⚠️ Omisión (Olvido): El asistente vio el borde borroso, pero en su conclusión no mencionó el derrame pleural. El juez dice: ¡Oye! La lógica te obliga a decirlo, pero lo omitiste.

¿Qué descubrieron?

Al poner a 7 diferentes "asistentes" (modelos de IA) a prueba con este sistema, descubrieron cosas que las métricas tradicionales no veían:

Algunos son demasiado tímidos: Hay modelos que nunca inventan diagnósticos falsos (son muy seguros), pero a veces se callan diagnósticos que deberían haber hecho. Son como un médico que tiene miedo de equivocarse y no dice nada.
Algunos son muy alucinadores: Otros modelos escriben diagnósticos muy creativos pero que no tienen ninguna base en la radiografía. Son como un novelista que escribe una historia emocionante pero que no tiene nada que ver con la foto.
Las métricas antiguas fallan: Los modelos que parecían "peores" por las métricas de palabras (porque usaban sinónimos diferentes) en realidad tenían una lógica muy sólida.

El Resultado Final: Un Filtro de Seguridad

La parte más importante es que pueden usar a este "Juez Lógico" como un filtro de seguridad antes de entregar el informe al médico real.

Si el modelo genera un informe, el sistema lo revisa:

Si el modelo dice "tumor" pero no hay evidencia, el sistema borra esa frase automáticamente.
Si el modelo olvida algo obvio, el sistema puede advertirlo.

En resumen:
Este trabajo no intenta reemplazar al médico, sino crear un sistema de garantía para la IA. Es como poner un cinturón de seguridad y un airbag en un coche. El coche (la IA) puede conducir rápido y escribir bien, pero este sistema asegura que, si la lógica falla, el "airbag" (el verificador) detenga la información falsa antes de que llegue al médico, haciendo que la asistencia médica sea mucho más segura y confiable.

Ya no se trata de si el texto suena bonito, sino de si la lógica es matemáticamente correcta.

Each language version is independently generated for its own context, not a direct translation.

Aquí tienes un resumen técnico detallado del artículo "Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification" (Hacia garantías para el razonamiento clínico en Modelos de Lenguaje y Visión mediante Verificación Formal), presentado en español.

1. El Problema

Los Modelos de Lenguaje y Visión (VLMs) han mostrado gran potencial para redactar informes de radiología preliminares, reduciendo la fatiga de los clínicos. Sin embargo, su despliegue en entornos clínicos críticos enfrenta una vulnerabilidad fundamental: la ausencia de garantías formales de corrección lógica.

Inconsistencias Lógicas: Los VLMs, al ser generadores de texto probabilísticos optimizados para la fluidez, a menudo generan impresiones diagnósticas que no están respaldadas por sus propias observaciones perceptuales (hallucinaciones) o omiten conclusiones lógicamente forzadas por los hallazgos.
Fallo de las Métricas Actuales: Las métricas estándar de PLN (como BLEU y ROUGE) se basan en la similitud léxica con un informe de referencia ("ground truth"). Estas métricas penalizan el parafraseo clínico válido y, lo más grave, no pueden detectar fallos deductivos en entornos donde no existe un texto de referencia (escenarios del mundo real).
Riesgo de Seguridad: La falta de validación lógica interna crea una "ilusión de razonamiento", donde un informe fluido pero contradictorio puede inducir a errores por sesgo de automatización en los médicos.

2. Metodología: Marco de Verificación Neurosimbólica

Los autores proponen un marco novedoso que desacopla la percepción visual (probabilística) del razonamiento clínico (determinista), utilizando principios de verificación formal.

A. Ontología y Autoformalización

Ontología Formal ( $O$ ): Se define una ontología ligera que mapea el texto libre a predicados atómicos:
- $F$ : Observaciones (ej. "ángulo costofrénico embotado").
- $D$ : Diagnósticos (ej. "derrame pleural").
- $K$ : Base de conocimiento clínico, modelada como fórmulas proposicionales que definen condiciones suficientes y restricciones de consistencia (ej. $d \Rightarrow \neg d'$ ). Esta base se construye automatizando guías clínicas con LLMs y refinándolas con expertos médicos.
Función de Autoformalización ( $T$ ): Un LLM estrictamente restringido (temperatura 0.0) convierte la sección de "Hallazgos" ( $R_F$ ) del informe generado en un vector de estado binario ( $V$ ) bajo la hipótesis de mundo cerrado (lo no mencionado se considera ausente). Esto transforma el texto no estructurado en restricciones lógicas computables.

B. Verificación mediante Satisfacibilidad (SAT/SMT)

El proceso de verificación se formula como un problema de satisfacibilidad booleana utilizando el solucionador Z3:

Se construye un contexto proposicional ( $\Phi_V$ ) a partir de los hallazgos observados.
Para cada diagnóstico $d$ en la "Impresión" ( $R_I$ ), se verifica si $d$ es una consecuencia lógica de los hallazgos bajo la base de conocimiento: $\Phi_V \land K \models d$ .
El solucionador verifica la insatisfacibilidad de la negación: IsSat(ΦV ∧ K ∧ ¬d).

C. Taxonomía de Errores

El marco clasifica los diagnósticos en cuatro categorías basadas en la consistencia interna:

Soportado (Entailment): El diagnóstico es lógicamente forzado por los hallazgos (Verificador: Unsat).
No Soportado (Alucinación): El diagnóstico se afirma pero no es lógicamente forzable (Verificador: Sat).
Omitido: El diagnóstico es forzable por los hallazgos pero falta en la impresión.
Correctamente Excluido: No es forzable y no se afirma.

3. Contribuciones Clave

Marco Neurosimbólico sin Referencia: Un sistema que audita la lógica interna de los VLMs sin necesidad de un informe de referencia humano, mapeando texto libre a restricciones SMT mediante una ontología clínica.
Detección de Modos de Fallo Ocultos: Identificación de fallos deductivos específicos (observación conservadora, alucinación estocástica) que las métricas léxicas tradicionales no pueden detectar.
Garantía Post-hoc Rigurosa: Demostración de que aplicar un solucionador SMT como filtro posterior elimina sistemáticamente las alucinaciones no soportadas, aumentando la solidez diagnóstica.

4. Resultados y Análisis

Los autores evaluaron 7 VLMs (incluyendo modelos generales como LLaVA y modelos médicos adaptados como MedGemma y Lingshu) en 5 benchmarks de radiografía de tórax (MIMIC-CXR, CheXpert, NIH-CXR, etc.).

Fallo de las Métricas Léxicas: Las puntuaciones BLEU y ROUGE fueron extremadamente bajas (cercanas a cero), confirmando que la similitud de texto no refleja la calidad del razonamiento clínico.
Auditoría de Consistencia Interna:
- Se definieron métricas de Solidez (Soundness) (proporción de afirmaciones lógicamente soportadas) y Completitud (Completeness).
- Se identificaron tres perfiles de modelos:
  - Consistentes (ej. MedGemma-27B): Alta solidez y completitud.
  - Observadores Conservadores (ej. Qwen3-VL-8B): Alta solidez pero baja completitud (evitan alucinar pero omiten diagnósticos forzados).
  - Estocásticos (ej. Llava-Vicuna-7B): Baja precisión y completitud, tratando la tarea como generación de texto estadístico sin anclaje lógico.
Impacto del Filtrado Simbólico:
- Al aplicar el filtro de verificación en conjuntos de datos etiquetados, la solidez (Soundness) aumentó consistentemente en todos los modelos (ej. de ~0.93 a ~0.96 en MedGemma-27B).
- La precisión mejoró significativamente, mientras que la completitud y el recall disminuyeron ligeramente. Esto indica que el filtro elimina afirmaciones no justificadas sin suprimir masivamente los diagnósticos correctos, actuando como un mecanismo de seguridad conservador.

5. Significado e Impacto

Este trabajo representa un cambio de paradigma en la evaluación de IA clínica:

De la Similitud de Superficie a la Consistencia Interna: Propone mover la evaluación de la comparación de cadenas de texto (que es frágil en medicina) a la verificación formal de la lógica deductiva.
Seguridad Garantizada: Ofrece un camino práctico hacia asistentes clínicos generativos más seguros, donde las afirmaciones diagnósticas pueden ser auditadas matemáticamente antes de ser presentadas al médico.
Marco de "Asume-Garantiza": Establece que la corrección del sistema es condicional a la precisión de la traducción texto-símbolo y a la base de conocimiento curada, alineándose con los estándares de verificación formal en ingeniería de software crítica.

En resumen, el paper demuestra que es posible auditar y mejorar el razonamiento clínico de los VLMs mediante la integración de lógica simbólica, proporcionando garantías cuantificables sobre la validez deductiva de los informes médicos generados.