Resumen Técnico: Un Estudio Empírico de Especificaciones Generadas por LLM para VeriFast

Planteamiento del Problema

Las herramientas de verificación estática, particularmente aquellas basadas en Lógica de Separación (SL) como VeriFast, son capaces de verificar software de escala industrial para la corrección funcional y la seguridad de memoria. Sin embargo, su adopción se ve obstaculizada por la significativa labor humana requerida para escribir las especificaciones. A diferencia de los verificadores que no utilizan SL, los verificadores de SL requieren especificaciones auxiliares complejas —incluyendo invariantes de bucle, lemas inductivos y "folds" y "unfolds" (aperturas y cierres) explícitos de predicados— para razonar sobre estructuras de montículo (heap) y propiedad (ownership). Si bien investigaciones recientes han aplicado con éxito Modelos de Lenguaje de Gran Escala (LLM) para generar especificaciones para verificadores que no son de SL (por ejemplo, Dafny, Frama-C), existe una falta de evaluación empírica sobre su capacidad para generar especificaciones para verificadores basados en SL, los cuales demandan patrones de razonamiento únicos respecto a la disyunción del montículo y la propiedad.

Metodología

Los autores llevaron a cabo un estudio empírico de dos etapas para evaluar el desempeño de los LLM en la generación de especificaciones para el verificador de SL VeriFast.

Construcción del Conjunto de Datos:
El estudio utilizó un conjunto de datos de 303 funciones provenientes de 60 programas en C. Para cada función, se crearon cuatro versiones:

1. Verdad de Referencia (Ground Truth): Completamente especificada y verificada con VeriFast.
2. Lenguaje Natural (NL): Código fuente con descripciones informales en lenguaje natural del comportamiento.
3. Comportamiento Funcional (FB): Código fuente con precondiciones y postcondiciones formales en el lenguaje de especificación de VeriFast.
4. Comportamiento Funcional Plus (FBP): Código fuente con pre/postcondiciones formales más constructos adicionales requeridos para la verificación (por ejemplo, estado de asignación de memoria, límites de enteros).

Diseño Experimental:
El estudio procedió en dos etapas:

1. Estudios Piloto: Realizados en un subconjunto de 45 funciones (de 10 programas desarrollados por los autores) para seleccionar la configuración óptima.

   • Enfoques de Prompting: Se probaron ocho enfoques, incluyendo Basic, Chain-of-Thought (CoT), RAG-sparse y RAG-dense, con variaciones en la granularidad de la entrada (programa completo vs. función individual).
   • Selección de LLM: Se evaluaron diez LLM. Basándose en las tasas de éxito de verificación, la severidad de los errores y la preservación del comportamiento funcional, se seleccionaron tres modelos para el estudio completo: Claude 3.7 Sonnet, Gemini 2.5 Pro y GPT-4o.
   • Resultado de la Selección: El enfoque RAG-sparse con división de entrada (procesando una función a la vez) fue seleccionado como la estrategia de prompting más efectiva.

2. Estudio Completo: El prompt seleccionado y los tres LLM se aplicaron al conjunto de datos completo de 303 funciones a través de los tres tipos de entrada (NL, FB, FBP), generando 2,727 funciones de salida.

Métricas de Análisis:

• RQ1 (Comportamiento Funcional): Análisis cualitativo de si el LLM alteró el código fuente o debilitó/fortaleció las pre/postcondiciones en comparación con la entrada.
• RQ2 (Verificabilidad): Medición cuantitativa del porcentaje de especificaciones generadas que se verificaron exitosamente con VeriFast.
• RQ3 (Errores): Un análisis profundo de 354 funciones fallidas (muestreadas para representar la distribución de características del lenguaje), corrigiendo manualmente los errores para categorizarlos por severidad (Compilación, Práctica, Teórica) y ubicación (por ejemplo, predicados, invariantes de bucle, sentencias de apertura/cierre).

Contribuciones Clave

1. Primer Estudio Empírico sobre Verificadores de SL: Este es el primer estudio exhaustivo de la evaluación de LLM generando especificaciones para un verificador de SL (VeriFast), cubriendo 8 enfoques de prompting, 10 LLM y 3 tipos de entrada.
2. Conjunto de Datos Integral: Un conjunto de datos públicamente disponible de 60 programas en C (303 funciones) que presenta cuatro variantes de especificación (incluyendo la verdad de referencia) para facilitar investigaciones futuras.
3. Análisis de Errores Granular: Una taxonomía detallada de errores de verificación, distinguiendo entre errores de compilación, fallos de razonamiento práctico (por ejemplo, falta de sentencias open/close) e inconsistencias lógicas teóricas, junto con correcciones codificadas por humanos.
4. Información Accionable: Guía específica sobre la optimización de entornos de verificación basados en LLM, incluyendo los beneficios de las especificaciones de entrada formales y la utilidad de las funciones automáticas de VeriFast.

Resultados

Preservación del Comportamiento Funcional (RQ1):

• Los LLM preservaron mayoritariamente el comportamiento funcional pretendido.
• Código Fuente: El 91.0% de las salidas permanecieron sin cambios; el 9.0% contuvo cambios (principalmente ediciones semánticas menores o cabeceras alucinadas).
• Especificaciones: El 92% de las pre y postcondiciones preservaron el comportamiento funcional (equivalente o fortalecido).
• Impacto de la Entrada: Las entradas formales (FB/FBP) resultaron en tasas de preservación más altas que las entradas de Lenguaje Natural (NL). Gemini 2.5 Pro demostró la mayor robustez contra la ambigüedad.

Verificabilidad (RQ2):

• La tasa de éxito de verificación general fue del 31.4% (aproximadamente 1 de cada 3 funciones).
• Tipo de Entrada: Las tasas de éxito se correlacionaron con la completitud de la entrada: FBP (39.9%) > FB (29.5%) > NL (24.6%).
• Desempeño de los Modelos: Gemini 2.5 Pro superó a los demás (39.7% de promedio de éxito) en comparación con Claude 3.7 (29.8%) y GPT-4o (24.5%).
• Complejidad: Las tasas de éxito disminuyeron significamente para características complejas: SL Normal (51.2%) > Predicados Recursivos (30.9%) > Concurrencia (12.3%) y Bucles (11.4%).

Análisis de Errores (RQ3):

• Distribución de Errores: De los 1,652 errores analizados, el 71% fueron Prácticos (insuficientes para el razonamiento automatizado, por ejemplo, falta de sentencias open/close), el 23% fueron errores de Compilación, y solo el 6% fueron Teóricos (inconsistencias lógicas).
• Causas Raíz: La gran mayoría de los errores (94%) derivaron de una falta de conocimiento específico del dominio respecto a la mecánica del verificador de SL (sintaxis, razonamiento de montículo, seguimiento de propiedad) más que de fallos de razonamiento lógico general.
• Fallos Específicos: Los problemas comunes incluyeron la falta de anotaciones malloc_block, la colocación incorrecta de pre/postcondiciones y la falla al proporcionar los invariantes de bucle o lemas necesarios para la transitividad de segmentos de montículo.
• Diferencias de Modelo: Gemini 2.5 produjo la menor cantidad de errores en todas las categorías, particularmente en el razonamiento teórico y práctico.

Significado y Reivindicaciones

El artículo sostiene que, si bien los LLM son capaces de preservar el comportamiento funcional del código fuente y las especificaciones, actualmente logran un éxito modesto en la generación de especificaciones totalmente verificables para herramientas de lógica de separación. El principal cuello de botella no es el razonamiento general, sino la falta de conocimiento específico sobre los patrones de especificación auxiliar únicos de los verificadores de SL (por ejemplo, la gestión de la propiedad del montículo mediante open/close y lemas).

Los autores concluyen que:

1. Las Entradas Formales Importan: Proporcionar contratos formales (FB/FBP) mejora significativamente las tasas de éxito en comparación con el lenguaje natural.
2. La Selección del Modelo es Crítica: Gemini 2.5 Pro es actualmente el modelo superior para esta tarea, particularmente para características complejas como concurrencia y bucles, a pesar de un mayor costo.
3. Mejoras en las Herramientas: Para mejorar el desempeño de los LLM, los verificadores de SL deberían exponer mejor información de depuración (por ejemplo, estados de montículo simbólico) a los LLM durante los bucles de reparación, y aprovechar enfoques híbridos donde las herramientas simbólicas (como la función automática de VeriFast) manejen la generación de open/close simples mientras los LLM manejan el razonamiento complejo.

El estudio no pretende afirmar que los LLM puedan reemplazar actualmente a los expertos humanos para la verificación de SL, sino que proporciona una línea base y una guía específica para construir futuros entornos de verificación asistidos por IA.