Automated Proof Generation for Rust Code via Self-Evolution

1. El Problema: Escasez de Datos para Verificación Formal

La generación de código asistida por Grandes Modelos de Lenguaje (LLM) ha avanzado mucho, pero garantizar la corrección formal sigue siendo un desafío crítico. La verificación formal (usando herramientas como Verus para Rust) requiere la construcción de pruebas matemáticas rigurosas que demuestren que el código cumple con sus especificaciones bajo todas las entradas posibles.

El obstáculo principal para automatizar este proceso es la severa escasez de datos:

• A diferencia del código general, existen muy pocas pruebas formales escritas por humanos disponibles para entrenar modelos.
• Para Verus (la herramienta de estado del arte para Rust), hay menos de 500 archivos verificados en GitHub, insuficientes para el fine-tuning de modelos.
• La creación manual de especificaciones y pruebas requiere expertos y mucho tiempo, lo que impide la escalabilidad.

2. Metodología: El Marco SAFE

Los autores proponen SAFE (Self-evolving Automated prooF gEneration), un marco que supera la falta de datos mediante un ciclo de auto-evolución que combina síntesis de datos y ajuste fino (fine-tuning). El sistema utiliza un verificador simbólico (Verus) como "árbitro" definitivo para distinguir pruebas correctas de incorrectas sin intervención humana.

El proceso se divide en tres etapas principales:

A. Generación de Código Compatible con Verus

Dado que Verus no soporta todas las características de Rust (como ciertos iteradores o bibliotecas estándar), SAFE utiliza GPT-4o para "traducir" miles de programas pequeños de Python y Rust (de conjuntos de datos como MBPP y CodeNet) a una sintaxis compatible con Verus. Solo se conservan los programas que compilan correctamente.

B. Síntesis Auto-Evolucionista de Especificaciones

Antes de generar pruebas, se necesitan especificaciones formales (precondiciones y postcondiciones).

1. Arranque (Bootstrapping): GPT-4o genera especificaciones iniciales basadas en docstrings.
2. Evolución: Se entrena un modelo de código abierto (DeepSeekCoder) con las especificaciones de alta calidad para generar mejores especificaciones en rondas sucesivas.
3. Filtrado: Se utiliza una métrica cuantitativa basada en casos de prueba mutados para evaluar la Correctitud (acepta implementaciones correctas) y Completitud (rechaza implementaciones incorrectas). Solo se conservan las especificaciones que superan umbrales específicos (ej. >80% de correctitud, >60% de completitud).

C. Síntesis Auto-Evolucionista de Pruebas y Auto-Depuración

Esta es la fase central donde se generan las pruebas formales.

1. Generación de Pruebas: El modelo intenta generar anotaciones de prueba (invariantes de bucle, aserciones) que permitan a Verus verificar el código.
2. Filtrado Automático: Verus valida cada intento. Las pruebas que fallan se descartan para el entrenamiento de generación, pero...
3. Reutilización para Auto-Depuración (Self-Debugging): Las pruebas incorrectas se convierten en una oportunidad. Para cada prueba fallida ($P_X$) que eventualmente se corrige a una prueba válida ($P_{\checkmark}$), se crea un triple de entrenamiento: {Prueba Incorrecta, Mensaje de Error de Verus, Prueba Correcta}.
4. Entrenamiento Conjunto: El modelo se ajusta finamente para dos tareas simultáneas:
   • Generar pruebas desde cero.
   • Depurar y reparar pruebas existentes basándose en los mensajes de error de Verus.

3. Contribuciones Clave

• Marco SAFE: La primera solución que aborda la escasez de datos para la verificación formal de Rust mediante un ciclo de auto-evolución que no depende de grandes corpus de datos humanos.
• Mecanismo de Auto-Depuración: Una estrategia innovadora que transforma los errores de verificación (que normalmente son datos "basura" para el entrenamiento) en datos de alta calidad para enseñar al modelo a corregir sus propios errores.
• Síntesis de Especificaciones de Alta Calidad: Un método robusto para generar especificaciones formales "suficientemente buenas" (no perfectas) que permitan la síntesis de pruebas sin requerir intervención humana masiva.
• Dataset Masivo Sintético: La creación del conjunto de datos más extenso hasta la fecha para Verus, con 19,017 especificaciones formales y 9,706 funciones Rust verificadas, más de 10,000 pares de datos de depuración.

4. Resultados Experimentales

Los autores evaluaron SAFE en dos benchmarks: VerusBench (creado por humanos) y CodeNet-Test (sintético). Se comparó contra GPT-4o y modelos base sin ajustar (LLaMa3.1, DeepSeekCoder).

• Rendimiento Superior:
  • En VerusBench, SAFE (con DeepSeekCoder) alcanzó una precisión de 43.17% (generación directa) y 52.52% (con auto-depuración), superando drásticamente a GPT-4o, que logró solo 14.39%.
  • En CodeNet-Test, SAFE alcanzó 48.43% con auto-depuración, frente al 0.28% de GPT-4o.
• Eficacia de la Auto-Evolución: El rendimiento mejoró significativamente en cada ronda de evolución (Round 1 a Round 3), demostrando que el modelo aprende efectivamente de sus propios datos sintetizados.
• Impacto de la Depuración: El uso del mecanismo de auto-depuración (SAFE+) mejoró consistentemente la precisión en comparación con la generación directa, especialmente en tareas complejas.
• Calidad de Especificaciones: Se demostró que entrenar con especificaciones de baja calidad reduce drásticamente el rendimiento final, validando la importancia del filtrado estricto en la etapa de especificación.

5. Significado e Impacto

Este trabajo representa un avance fundamental en la verificación formal asistida por IA.

• Democratización: Permite que modelos de código abierto, que inicialmente no conocían la verificación formal, adquieran la capacidad de escribir pruebas complejas para Rust.
• Escalabilidad: Resuelve el cuello de botella de la falta de datos, ofreciendo un camino para aplicar la verificación formal a grandes proyectos de software sin depender de la escritura manual masiva de pruebas.
• Confianza en el Software: Al automatizar la generación de pruebas para un lenguaje seguro como Rust, SAFE contribuye directamente a la creación de software más robusto y libre de errores críticos, un objetivo crucial para la industria de la seguridad y sistemas críticos.

En resumen, SAFE demuestra que mediante un ciclo de retroalimentación cerrado donde el verificador simbólico guía el aprendizaje del modelo, es posible superar la barrera de la escasez de datos y lograr una automatización efectiva de la verificación formal.