Resumen Técnico: AxDafny – Generación de Código Verificado Agéntico en Dafny

Declaración del Problema

El artículo aborda el desafío de la generación de código agéntico en el contexto de la verificación formal. A diferencia de las tareas estándar de generación de código donde los modelos producen código ejecutable evaluado contra casos de prueba, la generación de código verificado requiere que el modelo produzca tanto la implementación ejecutable como los artefactos de prueba (como invariantes de bucle, aserciones y argumentos de terminación) necesarios para que un verificador formal demuestre la corrección.

Los autores identifican una brecha en las aplicaciones actuales de los métodos formales en la IA: mientras que la verificación proporciona señales de retroalimentación ricas (identificando violaciones de especificación, anotaciones faltantes y casos de borde no manejados), las tareas de IA convencionales rara vez utilizan esto debido a la alta especialización requerida. El problema específico es desarrollar un marco que aproveche la retroalimentación del verificador para refinar iterativamente tanto la lógica del programa como las estructuras de prueba en Dafny, un lenguaje con soporte de verificación formal integrado.

Metodología: Marco de Trabajo AxDafny

Los autores proponen AxDafny, un marco de reparación guiado por el verificador diseñado para la síntesis conjunta de programas y pruebas. El sistema opera en un bucle iterativo de generar–verificar–reparar, adaptando una arquitectura agéntica utilizada previamente para la demostración en Lean.

1. Arquitectura de Agentes

El marco consta de tres componentes principales:

• Agente Proponente: Genera un archivo Dafny completo basado en el enunciado del problema, las especificaciones originales y el contexto histórico. Crucialmente, está restringido para no modificar las cláusulas requires (precondiciones) o ensures (postcondiciones) que definen el problema, centrándose en cambio en la implementación y las anotaciones de prueba.
• Sistema Revisor: Un mecanismo de validación de dos etapas:
  • Verificaciones Deterministas: Asegura que las especificaciones originales se preserven (sin debilitamiento), rechaza constructos de "elusión de prueba" (por ejemplo, {:verify false}, assume, {:extern}) y ejecuta el verificador de Dafny (dafny verify). Extrae mensajes de diagnóstico específicos sobre fallos en las obligaciones de prueba (precondiciones, postcondiciones, invariantes, terminación).
  • Revisión basada en LLM: Detecta patrones de engaño sutiles no captados por las comprobaciones estáticas, como la reescritura de predicados para que sean trivialmente verdaderos.
• Módulo de Memoria: Mantiene una "memoria de reflexión" que condensa las lecciones de iteraciones previas. El proponente recibe tanto el historial inmediato del último intento (código, razonamiento, retroalimentación) como un resumen acumulado de los conocimientos obtenidos para guiar los refinamientos subsecuentes.

2. Benchmarks

Para evaluar el marco, los autores introducen LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny):

• Composición: 250 problemas de estilo competencia traducidos desde LiveCodeBench-Pro hacia Dafny, estratificados por dificultad (100 Fáciles, 100 Medios, 50 Difíciles).
• Construcción: Cada instancia incluye el problema en lenguaje natural, una firma de método de Dafny y una especificación formal. El proceso de construcción implicó una curación rigurosa, incluyendo la revisión de un LLM como juez y verificación manual para asegurar la alineación semántica con los problemas originales.
• Protocolo de Evaluación: Una solución se acepta solo si se verifica en Dafny sin modificar las especificaciones originales ni depender de pruebas vacuas. Una métrica secundaria compila las soluciones verificadas a Python para probarlas contra el entorno de pruebas de tiempo de ejecución original.

Los autores también evalúan sobre DafnyBench, un benchmark establecido para la síntesis de pistas de prueba (proof-hint synthesis) donde la implementación es fija y el agente debe restaurar invariantes y aserciones faltantes.

Contribuciones Clave

1. Marco AxDafny: Un sistema agéntico que sintetiza con éxito tanto el código ejecutable como las anotaciones de prueba necesarias mediante la reparación iterativa guiada por el verificador.
2. Benchmark LCB-Pro-Dafny: Un nuevo benchmark a gran escala (250 instancias) para evaluar la síntesis de programas verificados de extremo a extremo en un entorno de competencia, abordando la falta de benchmarks rigurosos con restricciones de tiempo de ejecución en la verificación formal.
3. Validación Empírica: Demostración de que la reparación guiada por el verificador supera significativamente a las líneas base de generación directa tanto en tareas de síntesis de pruebas como de síntesis de programas completos.

Resultados

El artículo reporta el rendimiento en dos tareas distintas:

1. Síntesis de Pruebas (DafnyBench)

• Rendimiento: AxDafny utilizando Gemini-3.1-Pro verificó el 92.7% (725/782) de las instancias.
• Comparación: Esto supera al baseline más fuerte reportado anteriormente, DafnyPro (86.2%), por 6.5 puntos porcentuales. Notablemente, AxDafny logra esto sin depender de una biblioteca de recuperación de pistas de prueba curada manualmente, que fue un componente clave del éxito de DafnyPro.
• Dinámica de Iteración: Las ganancias se concentran fuertemente en las primeras 5 iteraciones, alcanzando el sistema un rendimiento cercano a la saturación rápidamente.

2. Síntesis de Programas (LCB-Pro-Dafny)

• Rendimiento: AxDafny verificó el 56.4% de las tareas totales.
  • Fácil: 75.0%
  • Medio: 52.0%
  • Difícil: 28.0%
• Comparación: Esto representa una mejora sustancial sobre la línea base directa de GPT-5.5 pass@1, que logró solo un 11.6% de éxito general.
• Correctitud Ejecutable: Cuando las soluciones verificadas se compilaron a Python y se ejecutaron contra el entorno de pruebas original, muchas fallaron debido a Tiempo Límite Excedido (TLE) o Límite de Memoria Excedido (MLE) en lugar de incorrectitud funcional. Esto indica que, si bien los agentes generaron con éxito código funcionalmente correcto (probado por el verificador), a menudo fallaron en cumplir con las restricciones de complejidad asintótica inherentes a la programación competitiva, ya que las especificaciones de Dafny típicamente imponen la corrección funcional pero no los límites de rendimiento.

Significado y Reivindicaciones

El artículo afirma que la reparación guiada por el verificador es una estrategia altamente efectiva para generar código verificado, particularmente para la tarea compleja de sintetizar anotaciones de prueba junto con las implementaciones.

• Objetivos Distintos: Los autores destacan una distincción crítica entre el éxito de la verificación (corrección funcional probada por el verificador) y el rendimiento en tiempo de ejecución (satisfacer las restricciones de la programación competitiva). Los resultados muestran que un agente puede probar con éxito que un programa es correcto mientras falla en producir una implementación eficiente.
• Escalabilidad: El marco demuestra que el escalado de la inferencia (refinamiento iterativo) aumenta significamente el rendimiento en tareas de verificación formal, yendo más allá de las capacidades de la generación de un solo paso.
• Escasez de Datos: El artículo señala que la relativa escasez de datos de entrenamiento de Dafny (órdenes de magnitud menos que Python) sigue siendo un desafío, sin embargo, el enfoque agéntico logra cerrar esta brecha aprovechando la retroalimentación del verificador en lugar de depender únicamente de los datos de pre-entrenamiento.

El trabajo posiciona a LCB-Pro-Dafny como un banco de pruebas desafiante para la investigación futura en codificación agéntica, específicamente para tareas que requieren la síntesis tanto de la lógica como de la prueba.