Evaluating LLM-Generated ACSL Annotations for Formal Verification

Título: Evaluación de Anotaciones ACSL Generadas por LLM para Verificación Formal

1. Problema

La especificación formal es fundamental para construir sistemas de software verificables y fiables, pero generar especificaciones precisas y verificables para programas C del mundo real sigue siendo un desafío significativo. Aunque los métodos formales ofrecen garantías matemáticas, su aplicación práctica es costosa debido a la dificultad de escribir y mantener especificaciones, la mala escalabilidad de las pruebas y las limitaciones de las técnicas puramente simbólicas ante bases de código modernas.

El objetivo de este trabajo es evaluar empíricamente hasta qué punto las herramientas de análisis formal pueden generar y verificar automáticamente especificaciones en ACSL (ANSI/ISO C Specification Language) para programas C, sin asistencia humana ni basada en aprendizaje previo. El estudio busca llenar la brecha entre la generación de especificaciones por modelos de lenguaje grandes (LLM) y la verificación rigurosa mediante demostradores de teoremas.

2. Metodología

Los autores realizaron un estudio controlado utilizando un conjunto de datos recién publicado (noviembre de 2025) que contiene 506 programas C (filtrados a 355 archivos C puros tras eliminar archivos vacíos o incompletos).

• Entorno de Verificación: Se utilizó la plataforma Frama-C en un entorno Linux (WSL 2). La verificación se llevó a cabo mediante el plugin WP (Weak Precondition) de Frama-C, utilizando múltiples solucionadores SMT (Alt-Ergo, CVC4, CVC5 y Z3) bajo condiciones idénticas.
• Sistemas de Generación Comparados: Se evaluaron cinco estrategias distintas para generar anotaciones ACSL:
  1. Script basado en reglas (Python): Un enfoque determinista y simple.
  2. Plugin RTE de Frama-C: Genera especificaciones basadas en la detección de errores en tiempo de ejecución (enfoque de herramienta).
  3. DeepSeek-V3.2: Un modelo de lenguaje grande (LLM).
  4. GPT-5.2: Un modelo de lenguaje grande (LLM).
  5. OLMo 3.1 32B Instruct: Un modelo de lenguaje grande de código abierto (LLM).
• Métricas de Evaluación:
  • Tasa de éxito de la prueba: Porcentaje de objetivos de prueba demostrados automáticamente.
  • Estabilidad del solucionador: Número de timeouts (tiempos de espera agotados).
  • Eficiencia: Tiempo de demostración (Qed time) y su variabilidad (desviación estándar).
  • Análisis estático previo: Uso de la herramienta EVA de Frama-C para cobertura de sentencias y generación de alarmas.

3. Contribuciones Clave

• Evaluación Empírica Controlada: A diferencia de estudios previos basados en encuestas o flujos de trabajo interactivos (donde los desarrolladores corrigen iterativamente), este estudio automatiza completamente el proceso de generación y verificación en un conjunto de datos moderno y estandarizado (CASP).
• Comparación Directa Tool-vs-LLM: Proporciona una comparación rigurosa entre generadores tradicionales (basados en reglas y plugins de herramientas) y LLMs de última generación, aislando el impacto de la calidad de la anotación, la sensibilidad del solucionador y la estabilidad de la prueba.
• Análisis Multidimensional de Solucionadores: No solo se mide el éxito binario, sino que se analiza la variabilidad en el tiempo de demostración y la frecuencia de timeouts a través de cuatro solucionadores SMT diferentes, revelando cómo la complejidad de la especificación afecta a cada motor de prueba.
• Nuevas Evidencias sobre LLMs: Documenta las capacidades y limitaciones actuales de modelos específicos (DeepSeek, GPT-5, OLMo) en la generación de contratos formales para C, complementando trabajos anteriores sobre la formalización de requisitos.

4. Resultados Principales

• Rendimiento de Herramientas Tradicionales:
  • Las especificaciones generadas por el Script Python y el plugin RTE lograron las tasas de éxito de prueba más altas (cercanas al 100% en RTE) y los tiempos de demostración más bajos y estables.
  • El plugin RTE mostró una robustez excepcional, con muy pocos timeouts, aunque su cobertura de sentencias fue menor que la del análisis estático completo.
• Rendimiento de LLMs:
  • DeepSeek: Mostró el mejor rendimiento entre los LLMs, con tasas de éxito y tiempos de timeout que se acercaban a los de las herramientas tradicionales (RTE), aunque con mayor variabilidad.
  • GPT-5: Presentó tasas de éxito moderadas pero una alta frecuencia de timeouts, especialmente con el solucionador Alt-Ergo, lo que sugiere especificaciones ambiguas o demasiado débiles que expanden el espacio de búsqueda del solucionador.
  • OLMo3: Mostró un rendimiento intermedio, con una variabilidad en el tiempo de demostración menor que GPT-5 y DeepSeek, pero con tasas de éxito inferiores a las herramientas tradicionales.
• Comportamiento de los Solucionadores:
  • CVC4 y CVC5: Fueron los solucionadores más estables y consistentes, especialmente con entradas generadas por herramientas.
  • Alt-Ergo: Sufrió la mayor tasa de timeouts en configuraciones con LLMs, indicando sensibilidad a especificaciones complejas o mal estructuradas.
  • Z3: Mostró una variabilidad central baja pero fluctuaciones más amplias en entradas complejas.
• Compensación (Trade-off): Se identificó una clara compensación entre expresividad y estabilidad. Las especificaciones generadas por LLMs (especialmente GPT-5 y DeepSeek) son más heterogéneas y expresivas, lo que conduce a una mayor dispersión en los tiempos de demostración y una menor predictibilidad en comparación con las técnicas basadas en reglas o herramientas.

5. Significado e Implicaciones

• Viabilidad de la Automatización: El estudio demuestra que es posible generar especificaciones verificables automáticamente, pero la calidad varía drásticamente según el método de generación.
• Limitaciones de los LLMs: Aunque los LLMs pueden producir especificaciones sintácticamente válidas, su semántica a menudo carece de la robustez necesaria para una verificación automatizada fiable a gran escala sin intervención humana o refinamiento.
• Guía para Futuras Investigaciones: Los resultados sugieren que para la verificación a escala industrial, es crucial equilibrar la riqueza de la especificación con la variabilidad controlada. Las técnicas híbridas que combinan la estructura de las herramientas tradicionales con la capacidad de inferencia de los LLMs parecen ser el camino más prometedor.
• Impacto en la Industria: Proporciona una línea base empírica para que los desarrolladores y investigadores evalúen si confiar en LLMs para la generación de especificaciones formales en sistemas críticos, destacando que, por ahora, las herramientas tradicionales siguen siendo más fiables para la verificación automática pura.

En conclusión, el papel establece que, si bien los LLMs representan un avance significativo en la expresividad de la generación de especificaciones, las herramientas basadas en reglas y los plugins de análisis estático siguen siendo superiores en términos de estabilidad, eficiencia y predictibilidad para la verificación formal automatizada.