Resumen Técnico: KBSpec

Planteamiento del Problema

La generación automatizada de especificaciones formales es un paso crítico para la comprensión de programas y la verificación formal. Aunque los Modelos de Lenguaje Extensos (LLMs) han mostrado potencial en la generación de código, su aplicación a la especificación formal (por ejemplo, Java Modeling Language, JML) enfrenta un obstáculo significativo: la escasez de corpora de especificación formal en los datos de entrenamiento. Este estado de "bajos recursos" conduce a errores sintácticos frecuentes y fallos semánticos (por ejemplo, falta de comprobaciones de límites, invariantes incorrectos).

Los intentos existentes para aumentar los LLMs con conocimiento externo (por ejemplo, documentación oficial) son insuficientes porque los recursos de especificación formal suelen ser incompletos, carecen de cobertura de patrones de verificación diversos o contienen características experimentales no totalmente soportadas por los verificadores. Además, depender únicamente de conocimiento externo estático no logra capturar las restricciones matizadas y específicas del verificador necesarias para una verificación exitosa.

Metodología: KBSpec

Los autores proponen KBSpec (Generación de Especificaciones Aumentada por Base de Conocimientos), un marco que aumenta los LLMs con una base de conocimientos de doble fuente y autoevolutiva. El sistema opera sin modificar los parámetros del LLM ni requerir datos de referencia etiquetados, basándose en su lugar en la retroalimentación de los verificadores formales.

El flujo de trabajo de KBSpec consta de tres etapas principales:

1. Inicialización de la Base de Conocimientos

El sistema inicializa una base de conocimientos de especificación ($M$) utilizando conocimiento externo proveniente de la documentación oficial (por ejemplo, tutoriales, ejemplos y ejercicios de OpenJML) y directrices de reparación escritas por humanos. Cada elemento de conocimiento se estructura como un triplete: contenido original ($c_i$), un resumen ($s_i$) y palabras clave ($k_i$), generados por un LLM para facilitar la recuperación.

2. Evolución de la Base de Conocimientos (Fase de Entrenamiento)

Esta es la innovación central. La base de conocimientos se actualiza dinámicamente mediante un flujo de generación y reparación ejecutado sobre un corpus de "entrenamiento" de programas Java.

• Generación: Para un programa dado, el LLM genera una especificación base. Luego, recupera elementos de conocimiento relevantes y genera nuevas especificaciones basadas en diferentes combinaciones de conocimiento recuperado.
• Verificación y Calificación: Las especificaciones generadas se verifican mediante un verificador formal (OpenJML). Se asigna una puntuación de utilidad a cada elemento de conocimiento recuperado basada en si ayudó al LLM a superar la verificación cuando anteriormente falló, o si causó un fallo cuando anteriormente pasó.
• Reparación Iterativa: Para las especificaciones que fallan, el sistema realiza hasta tres rondas de reparación. El LLM utiliza la especificación original, el mensaje de error del verificador y el conocimiento recuperado para generar una versión corregida. La utilidad de los elementos recuperados se actualiza según la reducción de errores o la verificación exitosa.
• Actualización y Filtrado: Después de cada época, la base de conocimientos se actualiza. Los elementos con puntuaciones de utilidad bajas se filtran, y se añaden nuevas trayectorias exitosas (generación o reparación). La redundancia se gestiona mediante comprobaciones de similitud.

3. Inferencia Aumentada por Conocimiento

Durante la fase de evaluación, KBSpec utiliza la base de conocimientos evolucionada para asistir en la generación de especificaciones. A diferencia de la fase de entrenamiento, que utiliza el muestreo aleatorio de grupos de conocimiento, la etapa de inferencia emplea un selector basado en LLM. El LLM elige autónomamente los elementos de conocimiento más relevantes (hasta 3) del conjunto recuperado para guiar la generación y la posterior reparación de las especificaciones.

Contribuciones Clave

1. Marco KBSpec: Un enfoque novedoso y libre de parámetros para la generación de especificaciones formales que integra una base de conocimientos autoevolutiva impulsada por la retroalimentación del verificador.
2. Conocimiento de Doble Fuente: La identificación y validación de que combinar el conocimiento externo de la documentación (para la comprensión inicial del lenguaje) con el conocimiento interno (destilado de las trayectorias de generación/reparación del verificador) es esencial para superar las limitaciones de los LLMs en la especificación formal.
3. Validación Empírica: Una evaluación exhaustiva en el benchmark FormalBench (generación de especificaciones JML) que demuestra que KBSpec supera significativamente a los baselines de vanguardia, incluyendo SpecGen y diversas estrategias de prompting (Few-shot, Least-to-Most, Self-repair).

Resultados

Los experimentos se realizaron utilizando tres backends de LLM: GPT-5.2, GPT-5-mini y DeepSeek-v3.2.

• Mejora en la Tasa de Aprobación: KBSpec mejoró las tasas de verificación de aprobación entre un 10–25% respecto a los enfoques basados en LLM de vanguardia (por ejemplo, SpecGen). En GPT-5.2, la tasa de aprobación aumentó del 43.35% (SpecGen) al 58.94%.
• Reducción de Fallos: El marco redujo sustancialmente las tasas de fallo (por ejemplo, reduciendo la tasa de fallo para GPT-5.2 al 20.6%).
• Completitud: Aunque las puntuaciones promedio de completitud mostraron cierta varianza, KBSpec produjo el mayor número de especificaciones de alta completitud (completitud $\ge$ 0.5). El análisis de programas verificados mutuamente mostró que KBSpec mantuvo o mejoró la completitud en comparación con SpecGen, indicando que las ganancias en la tasa de aprobación no se lograron mediante la generación de contratos trivialmente débiles.
• Estudio de Ablación: El estudio confirmó que el mecanismo de evolución de la base de conocimientos (conocimiento interno) era el componente más crítico, contribuyendo más al rendimiento que la documentación externa inicial. La reparación iterativa también fue identificada como un motor principal de éxito.

Significado y Reivindicaciones

El artículo afirma que KBSpec aborda la naturaleza de "bajos recursos" de los lenguajes de especificación formal mediante la creación de un bucle de automejora donde el sistema aprende de sus propios éxitos y fracasos a través de la retroalimentación del verificador.

• Agnóstico al Modelo: El enfoque es ligero y puede aplicarse a cualquier LLM sin necesidad de ajuste fino (fine-tuning).
• Generalizabilidad: Aunque se evaluó en JML, los autores afirman que el diseño es agnóstico al lenguaje y puede adaptarse a cualquier lenguaje de especificación con un verificador automatizado.
• Ingeniería Pragmática: El análisis del conocimiento aprendido revela que el sistema aprende eficazmente estrategias de reparación pragmáticas (por ejemplo, el manejo de desbordamientos aritméticos, la eliminación de constructos no soportados) en lugar de simplemente debilitar las especificaciones para pasar la verificación.

Los autores concluyen que la integración del conocimiento derivado de la documentación con la evolución de la memoria basada en el verificador mejora sustancialmente la capacidad de los LLM para generar especificaciones formales sintácticamente correctas y semánticamente verificables.