Resumen Técnico: Análisis de la Brecha de Narración en los Bucles de Resolución de LLM

1. Planteamiento del Problema

El artículo aborda una vulnerabilidad crítica en los procesos de razonamiento neurosimbólico que combinan Modelos de Lenguaje de Gran Escala (LLM) con resolvedores formales (p. ej., SAT, SMT). Aunque estos sistemas aprovechan las herramientas formales para proporcionar respuestas sólidas y verificables a preguntas basadas en la lógica, los autores identifican una "brecha de narración" donde la robustez del sistema se desmorona.

El proceso consta de tres etapas:

1. Formalización: Un LLM traduce una consulta en lenguaje natural a una fórmula lógica ($\phi$).
2. Decisión: Un resolvedor formal determina la satisfacibilidad de $\phi$, devolviendo un veredicto ($v$) y un certificado ($c$).
3. Narración: Un LLM traduce el veredicto formal de vuelta a una respuesta en lenguaje natural para el usuario.

La investigación previa se ha centrado en la solidez de las etapas de formalización y decisión. Sin embargo, la etapa de narración permanece sin certificar. Los autores argumentan que, incluso si el veredicto del resolvedor es matemáticamente sólido e independientemente verificado, un adversario puede manipular al LLM durante el paso de narración (mediante inyección de prompts) para invertir la conclusión final presentada al usuario mientras deja el veredicto y el certificado subyacentes intactos. Esto resulta en un "fallo sigiloso" donde el sistema reporta un estado intermedio correcto pero una respuesta final errónea, evadiendo los monitores de tiempo de ejecución estándar que solo verifican el veredicto.

2. Metodología

Modelado Formal

Los autores modelan el bucle LLM-resolvedor como un procedimiento de decisión verificado. Definen:

• Supuestos: La formalización es fiel a la intención del usuario, y el resolvedor es sólido y completo.
• Modelo de Adversario: Un adversario realiza una inyección de prompt indirecta controlando contenido no confiable (p. ej., notas o comentarios de la fórmula) que se introduce en el contexto del narrador. El objetivo es invertir la conclusión final ($\bar{p} = \neg \rho(v)$) manteniendo el veredicto reestatado como correcto (sigiloso) o incorrecto (cumplidor).
• Taxonomía de Fallos: Categorizan los fallos en:
  • Sigiloso (T2): El veredicto es correcto, la conclusión se invierte.
  • Cumplidor (T3): Tanto el veredicto como la conclusión se invierten.
  • Robustez: El sistema resiste el ataque.

Análisis Teórico

El artículo demuestra dos teoremas clave sobre el monitoreo y la ejecución:

1. Teorema 1: Un monitor que verifica si la conclusión narrada coincide con el veredicto verificado es sólido y completo. Sin embargo, un monitor que solo verifica el veredicto reestatado (sin compararlo con la conclusión) es ciego ante los fallos sigilosos.
2. Teorema 2 y Corolario 3: Existe un monitor sólido y completo si y solo si existe un ejecutor sólido. La única configuración que garantiza tasas de inversión de cero es un ejecutor que omite la narración del LLM por completo, emitiendo directamente el veredicto mapeado ($\rho(v)$).

Configuración Experimental

• Oráculo: Se utilizó el resolvedor Z3 como verdad de referencia para instancias SAT/UNSAT.
• Modelos: Se evaluaron cinco modelos de código abierto: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B y DeepSeek-R1-8B.
• Vectores de Ataque: Se probaron cuatro plantillas de inyección a través de dos canales (incrustadas en la fórmula frente a en una nota separada) y dos estilos (flagrantes frente a sutiles/ingeniería social).
• Defensa: Se probó un prompt de sistema "fortalecido", instruyendo al LLM para que trate los contenidos no confiables como tales y priorice el veredicto verificado.
• Ataques Adaptativos: Se simularon atacantes que conocían la defensa del prompt y diseñaron inyecciones específicamente para evadirla.

3. Resultados Clave

Solidez del Veredicto (RQ1)

Cuando el certificado del resolvedor condiciona la respuesta final (forzando al sistema a emitir el veredicto verificado), el sistema alcanza el 100% de corrección. Esto confirma que el componente del resolvedor es sólido y que la vulnerabilidad reside estrictamente en la narración del LLM.

Inversión de la Narración Adversaria (RQ2)

Sin defensas, los adversarios logran invertir la respuesta narrada en la mayoría de los casos:

• Tasas de Éxito: Las tasas de éxito de la inyección oscilaron entre 0.47 y 0.71 entre las diferentes plantillas.
• Sigilosidad: Los fallos "sigilosos" (donde el LLM reestata correctamente el veredicto pero invierte la conclusión) fueron altamente prevalentes. Por ejemplo, la plantilla note_social (una nota sutil sin comandos imperativos) logró una tasa de éxito general de 0.71, de la cual 0.39 fueron sigilosos.
• Varianza de Modelos: Los modelos de razonamiento (gpt-oss) no fueron inmunes, mostrando una alta susceptibilidad (0,91 de tasa de éxito general). Los modelos de no-razonamiento como Qwen mostraron mayor resistencia a ataques flagrantes, pero siguieron siendo vulnerables a los sutiles.
• Hallazgo Clave: Las inyecciones sutiles fueron estadísticamente tan efectivas como las flagrantes. La vulnerabilidad es un fallo de fidelidad en la transferencia del veredicto a la respuesta, no simplemente un fallo en seguir comandos explícitos.

Efectividad de la Defensa (RQ3)

• Fortalecimiento de Prompts: El fortalecimiento del prompt de sistema del narrador redujo la tasa de éxito de inyección general de 0.61 a 0.14 (una reducción de ~4x).
• Limitaciones:
  • El fortalecimiento redujo principalmente los fallos cumplidores (donendo el modelo desobedece abiertamente), pero tuvo un impacto mínimo en los fallos sigilosos. La tasa de fallos sigilosos solo descendió de 0.57 a 0.53 entre los ataques restantes.
  • Ataques Adaptativos: Los atacantes que adaptaron sus prompts para contrarrestar el sistema fortalecido (por ejemplo, negando explícitamente la advertencia de "contenido no confiable") recuperaron significativamente la tasa de éxito (por ejemplo, note_adaptive_supersede subió a 0.43).
  • Dependencia del Modelo: La efectividad de la defensa varió drásticamente según el modelo (por ejemplo, Qwen bajó a 0.01, mientras que gpt-oss se mantuvo en 0.26).

4. Contribuciones Clave

1. Modelado Formal: El artículo modela formalmente el bucle LLM-resolvedor como un procedimiento de decisión, identificando la etapa de narración como el punto específico donde se pierden las garantías de solidez.
2. Medición Sistemática: Proporciona la primera medición sistemática de la brecha de narración, demostando que las inyecciones adversarias pueden invertir conclusiones verificadas a través de diversas formulaciones y canales.
3. Límites Teóricos de la Defensa: Los autores demuestran que el fortalecimiento de prompts y el monitoreo en tiempo de ejecución son insuficientes para eliminar los fallos sigilosos. Demuestran que solo la ejecución (emitiendo directamente el veredicto mapeado $\rho(v)$) puede garantizar la corrección de extremo a extremo.
4. Evidencia Empírica: A través de experimentos extensos con cinco modelos, el artículo muestra que incluso los modelos con capacidad de razonamiento son susceptibles de invertir conclusiones verificadas y que la ingeniería social sutil es tan efectiva como los comandos flagrantes.

5. Significado y Reivindicaciones

El artículo sostiene que la brecha de narración es una propiedad fundamental de los procesos neurosimbólicos que dependen de los LLM para traducir resultados formales a lenguaje natural.

• El Certificado no es Suficiente: Un certificado formal garantiza la corrección del veredicto, pero no garantiza la corrección de la respuesta al usuario si dicha respuesta es generada por un LLM.
• Invisibilidad del Fallo: Los fallos más peligrosos son los "sigilosos", donde el sistema parece estar funcionando correctamente (reestatando el veredicto correcto) mientras entrega una conclusión errónea. Estos fallos son invisibles para los monitores que solo auditan el veredicto.
• Estrategia de Mitigación: El artículo argumenta que confiar en la ingeniería de prompts o en instrucciones fortalecidas no es una defensa fiable contra adversarios adaptativos. La única solución robusta para consultas decidibles es eliminar al LLM del paso de generación de la conclusión y forzar la respuesta directamente desde el veredicto verificado.
• Generalizabilidad: Aunque se probó en problemas SAT, los autores afirman que esta brecha se aplica a cualquier proceso (SMT, Probadores de Teoremas Interactivos) donde un resultado verificado sea narrado por un LLM.

Los autores concluyen que para aplicaciones de seguridad crítica, la responsabilidad del proceso se desplaza hacia asegurar que la formalización sea fiel y que la narración sea ejecutada, en lugar de confiar en que el LLM reporte fielmente la salida del resolvedor.