💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

Este artículo presenta VerIbmc, un flujo de trabajo neurosimbólico que aprovecha modelos de lenguaje locales de pesos abiertos combinados con la síntesis de invariantes simbólicos y la retroalimentación iterativa de verificadores para lograr la generación de invariantes de bucle de vanguardia para la verificación de software, ofreciendo una alternativa que preserva la privacidad y es rentable frente a las herramientas propietarias basadas en la nube.

Autores originales: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Publicado 2026-06-16

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás intentando demostrar que una máquina compleja (un programa informático) nunca se romperá, sin importar cuántas veces la ejecutes. La parte más difícil de esta demostración es entender los "bucles" de la máquina: partes donde repite una tarea una y otra vez. Para demostrar que la máquina es segura, necesitas encontrar un Invariante de Bucle.

Piensa en un Invariante de Bucle como una "regla de seguridad" que debe cumplirse cada vez que la máquina inicia un nuevo ciclo de su bucle. Por ejemplo, si un bucle cuenta hacia atrás de 10 a 0, la regla de seguridad podría ser: "El número siempre está entre 0 y 10". Si puedes demostrar que esta regla se mantiene al inicio, permanece verdadera después de cada paso y conduce a un final seguro, toda la máquina queda demostrada como segura.

El problema es que encontrar estas reglas automáticamente es increíblemente difícil. Es como intentar adivinar la combinación secreta de una caja fuerte sin ninguna pista.

La forma antigua vs. La forma nueva

La forma antigua (Razonamiento Simbólico):
Tradicionalmente, las computadoras intentaban encontrar estas reglas usando matemáticas y lógica estrictas. Es como un contable súper preciso revisando cada número. Es muy fiable, pero lento y a menudo se queda estancado en problemas complejos y desordenados. Es como intentar resolver un laberinto revisando cada pared una por una.

La forma de la "Nube" (Grandes modelos de IA):
Recientemente, la gente ha empezado a usar modelos de Inteligencia Artificial (IA) masivos para adivinar estas reglas. Estas IA son como estudiantes brillantes y muy cultos que han leído millones de ejemplos de código. Pueden adivinar la regla correcta muy rápidamente. Sin embargo, para usarlas, normalmente tienes que enviar tu código a un servidor gigante y costoso en la nube (como enviar tus planos secretos a un extraño). Esto es malo para las empresas que necesitan mantener la privacidad de su código y cuesta mucho dinero.

La solución: VerIbmc (El "Súper-Ayudante" Local)

Los autores de este artículo construyeron un nuevo sistema llamado VerIbmc. Piensa en esto como un taller local donde puedes usar un asistente de IA inteligente sin tener que salir de tu edificio.

Así es como funciona VerIbmc, usando una analogía sencilla:

Imagina que estás intentando resolver un rompecabezas difícil (el invariante de bucle).

El Detective Determinista (Fase 0 y 1): Antes de pedir ayuda a la IA, VerIbmc envía a un detective estricto y lógico (una herramienta llamada ESBMC) para que examine el rompecabezas. El detective comprueba primero los hechos simples. Si el rompecabezas es fácil, el detective lo resuelve instantáneamente. Si el detective encuentra algunas pistas sólidas (como "el número siempre es positivo"), las anota en una pizarra.
El Asistente de IA Local (Fase 2): Si el detective se queda atascado, llama al Asistente de IA Local. Pero aquí está el truco: la IA no empieza desde cero. El detective le entrega a la IA la pizarra con las pistas que ya encontró.
El Bucle de Retroalimentación: La IA adivina una solución completa. El detective la comprueba.
- Si es incorrecta, el detective no solo dice "No". Dice: "Esta parte está mal, pero esta otra parte es en realidad correcta". Toma la parte correcta, la escribe en la pizarra y le pide a la IA que lo intente de nuevo, utilizando las nuevas pistas.
- Esto sucede una y otra vez hasta que el rompecabezas se resuelve o se agota el tiempo.

Dos formas de pensar (CoT vs. ToT)

El artículo también probó cómo la IA debería "pensar" mientras resuelve el rompecabezas:

Cadena de Pensamiento (Chain-of-Thought - CoT): La IA piensa en línea recta, paso a paso, como si escribiera una sola historia.
Árbol de Pensamientos (Tree-of-Thoughts - ToT): La IA se ramifica, como un árbol. Intenta varios caminos a la vez, ve cuál parece prometedor y luego concentra su energía en los mejores caminos. El artículo encontró que para los modelos de IA más fuertes, este método de ramificación era excelente, pero para los modelos más pequeños y débiles, a veces perdía el tiempo.

Los resultados: Por qué esto es importante

Los investigadores probaron este sistema en cientos de diferentes rompecabezas de programación utilizando cinco modelos de IA de "pesos abiertos" (modelos que cualquiera puede descargar y ejecutar en su propia computadora).

Privacidad ante todo: Debido a que todo se ejecuta en una máquina local, la información de la organización nunca sale de ella. Es como hacer la tarea de matemáticas en tu propia habitación en lugar de entregársela a un extraño.
Rentabilidad: No necesitas pagar tarifas costosas a las grandes compañías de la nube.
Rendimiento: La mejor configuración (usando un modelo local grande llamado GPT-OSS-120B) resolvió el 86.4% de los problemas. Esto es mejor que muchas herramientas tradicionales y competitivo con las herramientas de IA basadas en la nube que son costosas.
El impulso "Gratuito": El sistema descubrió que la fase del "Detective" (la parte simbólica) resolvió 75 problemas por sí sola sin necesidad de la IA. Para los modelos de IA más débiles, las pistas del detective les ayudaron a resolver 35 problemas más de los que podrían haber resuelto solos.

La conclusión

VerIbmc demuestra que no necesitas supercomputadoras en la nube, que son caras y violan la privacidad, para verificar la seguridad del software. Al combinar un detective lógico estricto con un asistente de IA local e inteligente que aprende de sus errores, puedes obtener resultados de primer nivel directamente en tu propia computadora. Es una forma de hacer que la verificación de software sea privada, asequible y poderosa.

Resumen Técnico: Verificación de Software Neuro-Simbólica con VerIbmc

Planteamiento del Problema

La síntesis de invariantes de bucle sigue siendo un cuello de botella central en la verificación formal de software. Aunque existen técnicas simbólicas (p. ej., interpretación abstracta, resolución de restricciones) y métodos basados en datos de "suposición y comprobación", estas suelen tener dificultades con la escalabilidad, la expresividad o la diversidad del código del mundo real. Recientemente, los Modelos de Lenguaje de Gran Escala (LLMs) han mostrado promesa en la generación de invariantes candidatos al aprovechar patrones aprendidos de corpus de código. Sin embargo, los enfoques neuro-simbólicos existentes dependen típicamente de modelos propietarios y cerrados accedidos a través de APIs de la nube externas. Esta dependencia introduce obstáculos significativos para el despliegue industrial:

Privacidad y Cumplimiento: El código fuente debe transmitirse a servicios de terceros, lo que plantea preocupaciones de confidencialidad.
Reproducibilidad: La dependencia de proveedores externos complica la integración en canales de verificación controlados.
Costo y Sostenibilidad: Los modelos de gran escala son computacionalmente costosos y demandan mucha energía, lo que limita su practicidad para flujos de trabajo de verificación continua.

Los autores postulan que estos desafíos requieren un cambio hacia modelos de lenguaje de pesos abiertos, desplegables localmente, que puedan operar enteramente dentro de la infraestructura de una organización sin exponer código propietario.

Metodología: El Pipeline VerIbmc

El artículo presenta VerIbmc, un pipeline neuro-simbólico diseñado para sintetizar invariantes de bucle para programas en C, combinando el razonamiento simbólico con LLMs de pesos abiertos alojados localmente. El sistema utiliza ESBMC (Efficient SMT-Based Context-Bounded Model Checker) como el oráculo de verificación. El pipeline está diseñado bajo el principio de "escalar solo cuando sea necesario", priorizando el razonamiento simbólico determinista y económico antes de invocar al LLM.

Arquitectura Central

El pipeline opera en tres fases distintas:

Fase 0 (Verificación de Línea Base): ESBMC verifica el programa no anotado. Si el programa es trivialmente seguro o demostrablemente inseguro, el proceso termina inmediatamente, evitando esfuerzos de síntesis innecesarios.
Fase 1 (Generación de Candidatos Simbólicos): Si la Fase 0 devuelve "Desconocido", el sistema enumera simbólicamente átomos candidatos mediante la comparación por pares de variables de entrada del bucle y constantes. Estos átomos se verifican para su inductividad usando ESBMC. El sistema mantiene tres almacenes: Provables ( $P$ ), Demostrables como Falsos ( $D$ ) e Desconocidos ( $U$ ). Si la conjunción de todos los átomos provables es suficiente para probar la postcondición, el pipeline termina exitosamente sin realizar ninguna llamada al LLM.
Fase 2 (Bucle de Refinamiento del LLM): Si la fase simbólica es insuficiente, el pipeline entra en un bucle iterativo donde un LLM es instado a generar nuevos invariantes.
- Mecanismo de Retroalimentación: El LLM recibe el programa actual, el contenido de los almacenes $P$ , $D$ y $U$ como retroalimentación estructurada, y ejemplos de pocos disparos (few-shot).
- Descomposición y Recombinación: Cuando un candidato generado por el LLM falla la verificación, el sistema lo descompone en subfórmulas (átomos). Los átomos se verifican individualmente y se añaden al almacén correspondiente. La conjunción de todos los átomos actualmente provables se vuelve a verificar. Esto permite al sistema rescatar componentes útiles de las propuestas fallidas del LLoma.
- Terminación: El bucle continúa hasta que se encuentra un invariante válido, se agota el presupuesto de iteración o ocurre un tiempo de espera (timeout).

Estrategias de Inferencia

Los autores evalúan cuatro estrategias de inferencia basadas en dos ejes de diseño:

Retroalimentación del Verificador (Prior Simbólico):
- Básica (Basic): Ejecuta el flujo completo de tres fases, utilizando el prior simbólico de la Fase 1 y la filtración a nivel de átomo.
- Solo LLM (LLM-Only): Omite la Fase 1 y la descomposición a nivel de átomo, confiando únicamente en que el LLM genere invariantes inductivos como un todo. Esto sirve como una línea base de ablación.
Estructura de Razonamiento:
- Cadena de Pensamiento (CoT - Chain-of-Thought): Utiliza un prompting estándar con ejemplos de razonamiento paso a paso (Inductivo, Lógica de Hoare, Cláusula de Horn o derivación directa).
- Árbol de Pensamientos (ToT - Tree-of-Thoughts): Explora múltiples estilos de derivación en paralelo durante una etapa de "exploración", los califica según el número de átomos provables generados y concentra el presupuesto de iteración restante en los dos estilos con mejor desempeño.

Contribuciones Clave

Pipeline Neuro-Simbólico: Un sistema completo que integra LLMs de pesos abiertos servidos localmente con ESBMC para la síntesis automatizada de invariantes de bucle, operando enteramente en la infraestructura interna.
Evaluación Sistemática de Estrategias: Una comparación exhaustiva de las variantes de LLM puro, guiado por símbolos y de Árbol de Pensamientos (ToT), demostrando el impacto de la retroalimentación simbólica y las estructuras de razonamiento.
Ganancias de Retroalimentación Simbólica: Demostración de que proporcionar átomos de invariantes provables como contexto al LLM genera ganancias consistentes, particularmente para modelos más débiles (por ejemplo, Llama-3.1-8B gana +35 benchmarks resueltos sobre una línea base de solo LLM).
Análisis de Ingeniería de Prompts: Evaluación de diferentes estilos de prompting (CoT vs. Tocción ToT) y plantillas de razonamiento (Inductivo, Lógica de Hoare, Cláusula de Horn) en la síntesis de invariantes.
Benchmarking a Gran Escala: Una evaluación extensa a través de cinco familias de modelos de pesos abiertos (de 7B a 120B de parámetros), cuatro estrategias de inferencia y cinco familias de benchmarks (520 problemas, 499 efectivos), totalizando 10,400 resultados por problema.

Resultados Experimentales

La evaluación se realizó en un servidor con cuatro GPUs NVIDIA RTX A6000 utilizando cinco modelos de pesos abiertos: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B y Llama-3.1-8B.

Desempeño General: La mejor configuración única (GPT-OSS-120B con la estrategia Basic) resolvió 431 de 499 problemas (86.4%).
Comparación con el Estado del Arte (SOTA):
- VerIbmc supera sustancialmente a las herramientas simbólicas tradicionales (CPA-Checker, 2ls, ESBMC-Kind) y a las herramientas puramente neuronales (Code2Inv) cuando se ejecutan en el mismo hardware local.
- En conjuntos de benchmarks compartidos, VerIbmc es competitivo o ligeramente inferior a las herramientas más fuertes aumentadas con LLM (Clause2Inv, LaM4Inv, LORIS) que dependen de APIs externas costosas (p. ej., GPT-4). Notablemente, VerIbmc logra estos resultados sin transmitir código a la nube.
- VerIbmc escala de forma única al conjunto completo de benchmarks de SV-COMP (154 problemas), incluyendo programas con arreglos, bucles anidados y punteros, que muchas herramientas competidoras no pueden expresar debido a limitaciones del frontend.
Impacto de la Fase Simbólica: La Fase 1 simbólica resolvió 75 problemas sin ninguna llamada al LLM. Para modelos más débiles, el aumento simbólico proporcionó mejoras significativas (hasta +35 problemas adicionales resueltos para Llama-3.1-8B).
ToT vs. CoT: El prompting ToT mostró un intercambio entre diversidad y precisión. Aunque alcanzó pares problema-modelo únicos inaccesibles para CoT, a menudo incurrió en una sobrecarga de tiempo de ejecución (wall-clock) y, para modelos más débiles, resultó en una disminución neta de problemas resueltos debido al agotamiento del presupuesto de iteración. Para los modelos más fuertes (GPT-OSS-120B), la diferencia de desempeño entre CoT y ToT fue insignificante.
Capacidad del Modelo: Los resultados indican que la capacidad del modelo es el principal motor de la precisión. La brecha entre los modelos más fuertes y los más débiles fue significativamente mayor que la varianza de desempeño introducida por cambiar las estrategias dentro de un mismo modelo.

Significado y Reivindicaciones

El artículo afirma que VerIbmc demuestra que un enfoque neuro-simbólico basado en LLMs puede aplicarse eficazmente a la síntesis de invariantes de una manera que preserva la privacidad y es eficiente energéticamente. Al operar enteramente en infraestructura local con modelos de pesos abiertos, el enfoque elimina la necesidad de costosos modelos de frontera propietarios bloqueados tras APIs.

Los autores enfatizan que su método es sólido por construcción: cada invariante candidato es validado por un verificador formal (ESBMC) antes de su aceptación. Aunque el sistema es incompleto debido a la indecidibilidad del problema, proporciona una vía práctica, escalable y reproducible para la verificación asistida por IA de software de producción. El trabajo da un paso hacia canales de verificación listos para la industria donde la privacidad de los datos y la eficiencia de recursos son requisitos críticos.