AutoReSpec: A Framework for Generating Specification using Large Language Models

1. El Problema

La generación automática de especificaciones formales (como JML en Java) es crucial para la verificación de software, la generación de pruebas y la síntesis de programas. Sin embargo, este proceso enfrenta dos barreras principales:

• Complejidad Manual: Escribir especificaciones a mano requiere expertos en métodos formales y consume mucho tiempo, lo que lleva a que estén ausentes en la mayoría de las bases de código reales.
• Limitaciones de los LLMs Actuales: Aunque los Modelos de Lenguaje Grande (LLMs) han mostrado potencial, los enfoques existentes (como SpecGen y FormalBench) sufren de:
  • Fallos frecuentes en la verificación debido a errores de sintaxis, imprecisiones lógicas o razonamiento incompleto, especialmente en bucles y lógica condicional compleja.
  • Uso de prompts estáticos que no se adaptan a la estructura del programa.
  • Falta de mecanismos para recuperarse de fallos o mejorar iterativamente basándose en la retroalimentación del verificador.
  • Estrategias de un solo modelo que no equilibran costo y precisión según la complejidad del código.

2. Metodología: AutoReSpec

AutoReSpec es un marco colaborativo diseñado para generar especificaciones formales verificables mediante una arquitectura de dos etapas que combina LLMs de código abierto y cerrados. Su funcionamiento se basa en tres pilares:

A. Selección Dinámica de Modelos (Recomendador LLM)

• Analiza el Árbol de Sintaxis Abstracta (AST) del programa de entrada para clasificarlo en categorías de complejidad (secuencial, ramificado, bucles de un solo camino, bucles de múltiples caminos, bucles anidados).
• Selecciona automáticamente el par óptimo de modelos (un modelo primario rápido/económico y un modelo colaborativo más potente/costoso) y la configuración de few-shot (ejemplos) más adecuada para ese tipo de programa específico.

B. Refinamiento Iterativo Guiado por Validador

• Fase Primaria: El modelo primario genera una especificación inicial. Esta se valida inmediatamente usando OpenJML y el solver Z3.
• Si la validación falla, el sistema no descarta el intento, sino que extrae el mensaje de error del validador y lo utiliza para refinar el prompt en un bucle conversacional. El generador de prompts adapta los ejemplos y las instrucciones basándose en el tipo de error (ej. invariantes de bucle, precondiciones).

C. Mecanismo Colaborativo de Recuperación

• Si el modelo primario agota su presupuesto de iteraciones sin éxito, se activa la etapa colaborativa.
• Se invoca al modelo colaborativo (ej. GPT-4o o Claude) con un contexto "limpio" que contiene únicamente la última especificación fallida y los errores de validación específicos.
• Este modelo se enfoca exclusivamente en corregir los errores identificados, evitando el "deslizamiento de contexto" y optimizando el uso de tokens costosos.

3. Contribuciones Clave

1. Marco Colaborativo AutoReSpec: Un sistema que recomienda pares de LLMs basados en la estructura del programa y utiliza un refinamiento conversacional guiado por el validador.
2. Estrategia de Ingeniería de Prompts Colaborativa: Combina ejemplos few-shot, retroalimentación de validadores y recorte automático de prompts para manejar contextos largos y resolver errores específicos.
3. AutoReSpecBench: Un nuevo conjunto de datos de referencia que incluye 72 programas Java (combinando SpecGenBench, SV-COMP y problemas reales de GitHub) diseñados para probar la escalabilidad y la complejidad de control de flujo.
4. Herramienta de Código Abierto: Liberación del marco completo, incluyendo el código, el conjunto de datos y una extensión para VS Code para facilitar su uso.
5. Evaluación Exhaustiva: Demostración de que la selección dinámica y la colaboración mejoran significativamente la probabilidad de éxito y la completitud en comparación con métodos de un solo modelo.

4. Resultados Experimentales

El marco se evaluó en un conjunto de 72 programas reales y sintéticos, comparándose con SpecGen y FormalBench:

• Éxito y Completitud:
  • AutoReSpec logró 67 de 72 programas verificados exitosamente (comparado con 58 de SpecGen y 13 de FormalBench).
  • Probabilidad de Éxito (SP): 58.2% (vs. 51.4% de SpecGen y 24.3% de FormalBench).
  • Completitud (C): 69.2% (vs. 51.4% de SpecGen y 24.3% de FormalBench).
• Eficiencia:
  • Reducción del tiempo de evaluación en un 26.89% en promedio.
  • Costo promedio de API por clase Java: $0.13 (menor que los $0.16 de SpecGen y $0.17 de FormalBench), gracias al uso prioritario de modelos de código abierto y la invocación de modelos propietarios solo cuando es necesario.
• Resolución de Errores:
  • Reducción drástica en la tasa de lucha (struggle ratio) para errores críticos como Postcondition (de 27.06% a 6.55%) e Invariantes de Bucle (de 16.67% a 1.16%) en comparación con SpecGen.

5. Significado e Impacto

AutoReSpec representa un avance significativo en la automatización de la ingeniería de software formal al demostrar que:

• La colaboración entre modelos es superior a la estrategia de un solo modelo: La combinación de un modelo rápido para la generación inicial y un modelo potente para la recuperación de errores ofrece el mejor equilibrio entre costo, velocidad y precisión.
• La adaptación al contexto es vital: La capacidad de ajustar dinámicamente el modelo y el prompt según la complejidad del control de flujo (especialmente en bucles anidados y múltiples caminos) es esencial para la verificación exitosa.
• Viabilidad Práctica: Al reducir el tiempo de ejecución y los costos de API sin sacrificar la calidad, AutoReSpec hace que la generación de especificaciones formales sea una opción viable para integrarse en flujos de trabajo de desarrollo de software reales, no solo en entornos de investigación.

En conclusión, AutoReSpec establece un nuevo estado del arte en la generación de especificaciones asistida por IA, superando las limitaciones de los enfoques estáticos anteriores mediante un ciclo de retroalimentación inteligente y colaborativo.