Can Large Language Models Model Programs Formally?

Resumen Técnico: Model-Bench y la Capacidad de Modelado Formal de LLMs

1. Planteamiento del Problema

En la era digital, la verificación formal es crucial para garantizar la corrección, seguridad y fiabilidad del software, especialmente en infraestructuras críticas. La verificación formal se divide principalmente en dos enfoques:

• Demostración de Teoremas: Ha visto avances significativos asistidos por IA (LLMs).
• Verificación de Modelos (Model Checking): Ha recibido menos atención debido a la dificultad de automatizar la extracción de modelos de comportamiento precisos a partir de código fuente.

El problema central es que los lenguajes dinámicos modernos (como Python) presentan comportamientos complejos en tiempo de ejecución (aliasing mutable, funciones de orden superior, bibliotecas de terceros, async/await) que deben abstraerse en un espacio de estados finito pero fiel para ser compatibles con verificadores de modelos como TLC (basado en TLA+). Existe una brecha entre la complejidad del código fuente y la capacidad de los LLMs para generar especificaciones formales correctas y ejecutables.

2. Metodología

Los autores introducen Model-Bench, un nuevo benchmark y una tubería (pipeline) diseñada para evaluar y mejorar la capacidad de los LLMs para modelar programas.

• Construcción del Dataset (Model-Bench):

  • Origen: Se derivaron 400 programas de Python de tres benchmarks populares: HumanEval, MBPP y LiveCodeBench.
  • Procesamiento: Se aplicó un flujo de trabajo riguroso que incluye:
    1. Normalización: Eliminación de duplicados y estandarización.
    2. Simplificación y Reescritura: Filtrado de bibliotecas externas (manteniendo solo typing y math), eliminación de características de lenguaje complejas (recursión, comprensiones de listas, clases) mediante reescritura asistida por LLMs, y filtrado de tipos de datos complejos no soportados por TLA+.
    3. Validación: Ejecución de los casos de prueba para asegurar que el código original sea funcional.
  • Transformación de Código: Se propone una técnica para convertir el código Python en una representación más alineada con TLA+ (máquinas de estados). Esto implica:
    • Generar un Gráfico de Flujo de Control (CFG).
    • Reescribir el código en un patrón de máquina de estados con una variable pc (contador de programa) para rastrear el estado actual.
    • Convertir cadenas de texto en arreglos de números (valores ASCII) debido a la inmutabilidad de las cadenas en TLA+.

• Evaluación:

  • Se utilizaron múltiples LLMs (DeepSeek, Qwen, Gemma, Llama) con configuraciones de prompting (Zero-shot, Few-shot) y con/sin código transformado.
  • Métricas:
    1. Runnable@k: Proporción de modelos generados que pasan la verificación del verificador TLC sin errores (al menos una vez en $k$ intentos).
    2. Similitud de Estados: Medida formal que compara la superposición de los estados observados en el modelo generado ($M_g$) frente a un modelo "oráculo" verificado manualmente ($M_o$). Se define como la proporción de estados del oráculo presentes en el modelo generado.

3. Contribuciones Clave

1. Model-Bench: El primer benchmark generalista y automatizado para evaluar la capacidad de los LLMs de generar especificaciones de verificación de modelos (TLA+) directamente desde código fuente.
2. Técnica de Transformación de Código: Una metodología novedosa que reduce la brecha semántica entre Python y TLA+ mediante la conversión a un patrón de máquina de estados, facilitando la tarea de modelado para los LLMs.
3. Análisis Exhaustivo: Un estudio empírico que revela limitaciones actuales y proporciona direcciones para futuras investigaciones, incluyendo un análisis detallado de casos de error (compilación, tiempo de ejecución y aserciones).

4. Resultados Principales

Los experimentos revelaron limitaciones significativas pero también oportunidades de mejora:

• Rendimiento General:
  • Los modelos con mejor desempeño fueron DeepSeek-V3, DeepSeek-V2.5 y Qwen3-32B.
  • Incluso con Few-shot learning, la tasa de modelos ejecutables (Runnable@1) alcanzó un máximo del 66.25% (DeepSeek-V3), lo que indica que la mayoría de los intentos aún fallan.
  • La similitud de estados promedio fue del 49.55% en el mejor escenario, sugiriendo que los modelos generados a menudo no capturan completamente el comportamiento del programa original.
• Impacto del Few-shot Learning:
  • El uso de ejemplos (Few-shot) mejoró drásticamente el rendimiento en comparación con Zero-shot. Por ejemplo, modelos que tenían una tasa de éxito cercana a 0 en Zero-shot lograron superar el 4-16% con Few-shot.
• Efectividad de la Transformación de Código:
  • El uso de código transformado (patrón de máquina de estados) aumentó significativamente la similitud de estados (ej. +18.99% para DeepSeek-V3), aunque causó una ligera disminución en la tasa de ejecutabilidad (Runnable@k) debido a la mayor longitud del código y la complejidad sintáctica.
  • La combinación de ambos enfoques (código original + transformado) demostró ser complementaria, aumentando el número total de modelos ejecutables.
• Complejidad vs. Rendimiento:
  • La dificultad de modelado no está correlacionada directamente con la dificultad algorítmica del problema, sino con la complejidad sintáctica: mayor complejidad ciclomática, profundidad de bucles anidados y número de variables reducen drásticamente la tasa de éxito.
• Análisis de Casos de Error:
  • Errores de Compilación: Uso de operadores desconocidos en TLA+ (ej. funciones de Python que no existen en TLA+).
  • Errores de Tiempo de Ejecución: Desalineación de convenciones (ej. índices de arrays basados en 1 en TLA+ vs. 0 en Python).
  • Errores de Aserción: Omisión de llamadas a funciones o uso incorrecto de constantes en lugar de dinámicas (ej. usar una longitud fija en lugar de Len(arr)).

5. Significado e Impacto

Este trabajo es fundamental porque:

• Cierra una brecha crítica: Mueve la investigación de la verificación asistida por IA desde la demostración de teoremas hacia la verificación de modelos, un área previamente descuidada debido a la dificultad de automatización.
• Establece un estándar: Proporciona una base sólida y reproducible (Model-Bench) para medir el progreso en la generación de especificaciones formales.
• Guía el desarrollo futuro: Demuestra que, aunque los LLMs actuales tienen limitaciones significativas en la fidelidad semántica para la verificación formal, técnicas de pre-procesamiento (como la transformación de código) y el aprendizaje con pocos ejemplos pueden mejorar sustancialmente la calidad de los modelos.
• Impulsa la seguridad del software: Al mejorar la capacidad de generar modelos verificables, se abre la puerta a la aplicación de verificación formal en sistemas de software más complejos y críticos, reduciendo la dependencia de pruebas empíricas que no garantizan la ausencia de errores.

En conclusión, el artículo concluye que, si bien los LLMs aún no son perfectos para el modelado formal automático, herramientas como Model-Bench y estrategias de transformación de código son pasos esenciales hacia la automatización de la verificación de software a gran escala.