Resumen: Las herramientas formales como los solucionadores SAT y SMT están cada vez más integradas en los procesos de razonamiento de modelos de lenguaje cuando una pregunta crítica de seguridad se puede formular en lógica. A diferencia de la cadena de pensamiento cuyos pasos se toman de la distribución del modelo sin garantía formal, un solucionador produce una respuesta sólida y verificable de forma independiente. Sin embargo, la garantía de solidez puede perderse en la interacción entre el solucionador y el modelo. El pipeline híbrido tiene tres componentes: formalizar la pregunta, decidirla y narrar el resultado. Trabajos anteriores han estudiado la formalización y la decisión, pero no la narración, que es el paso que convierte el resultado de una herramienta formal en la respuesta del usuario. Para llenar el vacío narrativo, primero modelamos el bucle LLM-solver como un procedimiento de decisión verificado. Evaluamos más a fondo cinco modelos de código abierto mediante inyección rápida y descubrimos que la activación de certificados hace que el veredicto del solucionador suene, mientras que un adversario puede invertir una conclusión verificada a través de frases y canales. Estudiamos la mitigación a través de un aviso reforzado que reduce significativamente la inyección pero no puede eliminarla y aún sufre el ataque adaptativo. Combinando el análisis formal y los estudios empíricos, mostramos en el bucle LLM-solver que la robustez no llega a la respuesta que el usuario finalmente lee.
Publicado originalmente en export.arxiv.org el 18 de junio de 2026.
Ver fuente original
