Resumen Técnico: Reducción de los Costos de Síntesis de Pruebas en Sistemas Rust Mediante la Ampliación de un Conjunto de Datos de Entrenamiento Semilla

1. Declaración del Problema

La corrección del código generado por Modelos de Lenguaje Grandes (LLM) sigue siendo un desafío significativo, especialmente para software de sistema crítico en términos de seguridad y fiabilidad. Aunque los LLM han demostrado capacidades sólidas de generación de código, con frecuencia producen código sintácticamente correcto que viola propiedades de seguridad, fiabilidad o funcionales. Un posible remedio es exigir a los LLM que generen pruebas de corrección formal junto con el código.

Sin embargo, generar pruebas formales para software de sistema (específicamente utilizando Verus, una herramienta de verificación de vanguardia para Rust) requiere capacidades de razonamiento significativamente mayores que la generación de código estándar. Además, el campo sufre de una escasez severa de datos. Los sistemas Rust verificados existentes son pocos, y los conjuntos de datos disponibles (por ejemplo, SAFE, AlphaVerus) tienen un alcance y una diversidad limitados. Trabajos anteriores han demostrado que solo modelos comerciales costosos y a gran escala (por ejemplo, Claude Sonnet 4.5) poseen la capacidad de generar tales pruebas de manera efectiva, mientras que los modelos más pequeños o económicos fallan. El problema central abordado por este artículo es: ¿Cómo podemos generar pruebas de código de manera efectiva a bajo costo sintetizando datos de entrenamiento de alta calidad y alto volumen para LLMs más pequeños?

2. Metodología: El Pipeline VeruSyn

Los autores proponen VeruSyn, un pipeline de síntesis de datos diseñado para crear el conjunto más grande de programas verificados con Verus hasta la fecha. El pipeline aborda tres limitaciones específicas de los esfuerzos de síntesis anteriores: escala limitada, cobertura de características estrecha y baja complejidad de razonamiento. VeruSyn integra tres enfoques de síntesis distintos de manera iterativa y coordinada:

2.1 Escalado del Número de Programas (Autosíntesis)

A diferencia de los métodos anteriores que dependen de la traducción de suites de referencia existentes (lo que limita el tamaño del conjunto de datos por la fuente), VeruSyn emplea una estrategia de autosíntesis.

• Proceso: Un LLM se ajusta fino para generar directamente programas Rust y sus especificaciones y pruebas Verus correspondientes desde cero, sin depender de programas fuente preexistentes.
• Iteración: El proceso comienza con un modelo base ajustado fino en el conjunto de datos SAFE. Este modelo genera programas iniciales. A medida que avanza la síntesis, el modelo se ajusta fino iterativamente sobre los datos recién generados, verificados y depurados para mejorar sus capacidades de generación.
• Terminación: La síntesis se detiene cuando la proporción de programas duplicados en un lote alcanza el 95%, asegurando la diversidad.

2.2 Escalado de la Cobertura de Características (Síntesis Basada en Tutoriales)

Para superar el sesgo de los conjuntos de datos anteriores hacia invariantes de bucle simples, VeruSyn utiliza el Tutorial de Verus como una fuente de conocimiento estructurada.

• Proceso: Expertos crean manualmente "programas semilla" que cubren puntos clave de conocimiento de cada capítulo del tutorial de Verus.
• Síntesis: Se solicita al modelo de generación de pruebas que genere miles de programas nuevos para cada semilla, guiados explícitamente por el capítulo correspondiente del tutorial.
• Objetivo: Esto asegura una cobertura sistemática de diversas características de Verus (por ejemplo, cuantificadores, aritmética no lineal, vectores de bits) que a menudo faltan en las referencias algorítmicas pero son esenciales para la verificación de sistemas del mundo real.

2.3 Escalado de la Complejidad del Razonamiento (Síntesis de Trayectorias de Agente)

Para manejar pruebas de sistemas complejos del mundo real que requieren cadenas largas de razonamiento, VeruSyn incorpora datos de Cadena de Pensamiento (CoT) derivados de trayectorias de agentes.

• Proceso: Un agente de codificación de vanguardia (potenciado por Claude Sonnet 4.5) tiene la tarea de escribir pruebas para un pequeño conjunto de problemas de verificación de sistemas del mundo real (provenientes de VeruSAGE-Bench).
• Recolección de Datos: Se recopila el registro completo del razonamiento del agente, las acciones (lectura de archivos, invocación de Verus, análisis de errores, edición de pruebas) y la trayectoria final exitosa.
• Integración: Estas trayectorias se convierten en datos de entrenamiento, proporcionando al modelo ejemplos de cómo depurar y razonar a través de errores de verificación complejos en múltiples pasos.

2.4 Anti-Trampas y Filtrado

Un componente crítico del pipeline es un proceso de filtrado riguroso para evitar el "engaño" (por ejemplo, modificar especificaciones para hacer las pruebas trivialmente verdaderas, agregar bucles infinitos para saltarse la verificación o usar declaraciones assume).

• Mecanismos: El pipeline utiliza analizadores sintácticos tree-sitter para verificar la compatibilidad de las especificaciones, detecta palabras clave prohibidas (como assume) y hace cumplir las cláusulas decreases para la terminación.
• Depuración: Los programas no verificados se retroalimentan al modelo con informes de errores para su depuración; solo se conservan los pares verificados con éxito.

3. Contribuciones Clave

• Escala del Conjunto de Datos: La síntesis de 6.9 millones de programas Rust verificados con Verus, cada uno con una especificación formal y una prueba. Este es el conjunto de datos más grande de su tipo.
• Diversidad de Características: El conjunto de datos cubre 12 a 15 puntos de conocimiento distintos de Verus (de 20 puntos clave), superando significativamente a conjuntos de datos anteriores (SAFE y AlphaVerus) que cubrían solo 4–5 puntos de manera significativa.
• Integración de CoT: La inclusión de 4,557 instancias largas de CoT derivadas de trayectorias de agentes en tareas de sistemas del mundo real.
• Rendimiento del Modelo: Un modelo Qwen2.5-Coder-32B-Instruct ajustado fino que logra capacidades de síntesis de pruebas competitivas a una fracción del costo de los modelos comerciales.

4. Resultados de la Evaluación

Los autores evaluaron el modelo ajustado fino con VeruSyn en dos referencias: VerusBench (150 tareas algorítmicas) y VeruSAGE-Bench (849 tareas extraídas de sistemas Rust del mundo real, con 289 excluidas para evitar fugas de datos).

4.1 Precisión

• Pruebas de Sistemas (VeruSAGE-Bench): Sin depuración, el modelo VeruSyn logró una tasa de éxito del 39% (Accuracy@100), superando significativamente al modelo Qwen crudo (10%), a los modelos ajustados fino con SAFE (6%), a los modelos ajustados fino con AlphaVerus (11%) y al comercial o4-mini (15%).
• Con Depuración: Después de 5 rondas de depuración, el modelo VeruSyn alcanzó una precisión del 49%, en comparación con el 54% del costoso Claude Sonnet 4.5.
• Pruebas Algorítmicas (VerusBench): El modelo logró una precisión del 75% (sin depuración), superando ligeramente a Claude Sonnet 4.5 (72%).

4.2 Eficiencia de Costos

El artículo destaca una reducción dramática en los costos:

• Costo por Tarea: El modelo VeruSyn cuesta aproximadamente $0.17 por tarea (sin depuración) y $0.61 (con depuración).
• Comparación: Esto es aproximadamente 47 veces más barato que Claude Sonnet 4.5 ($8.04 sin depuración) y significativamente más barato que o4-mini ($3.39).
• Compensación: El modelo VeruSyn con 5 rondas de depuración ($0.61) logra una mayor precisión (49%) que Claude Sonnet 4.5 sin depuración (46%), representando una reducción de costos del 13x para un rendimiento superior.

4.3 Estudios de Ablación

• Componentes de Datos: Eliminar ya sea los datos de autosíntesis/tutorial (Parte 1) o los datos de CoT (Parte 2) degradó significativamente el rendimiento en tareas de sistemas del mundo real. La Parte 1 fue crucial para tareas algorítmicas, mientras que la Parte 2 fue esencial para pruebas de sistemas complejos.
• Modelo Docente: El uso de un modelo docente más fuerte (Claude Sonnet 4.5) para la generación de CoT resultó en un rendimiento aguas abajo significativamente mejor (39% frente a 15% al usar o4-mini como docente).

5. Significado y Afirmaciones

El artículo afirma que VeruSyn demuestra que los datos sintéticos de alta calidad y a gran escala pueden cerrar la brecha entre modelos de código abierto pequeños y rentables y modelos comerciales costosos en el dominio de la verificación formal.

• Compensación Costo-Prueba: El trabajo establece una nueva referencia para la eficiencia de costos, mostrando que un modelo de 32B de parámetros ajustado fino en datos sintetizados puede superar o igualar a modelos comerciales 4.5 veces más grandes a una fracción del costo de inferencia.
• Escalabilidad: La metodología demuestra que la autosíntesis y la síntesis guiada por tutoriales pueden escalar más allá de las limitaciones de las suites de referencia existentes, creando un suministro "ilimitado" de datos de entrenamiento para herramientas de verificación formal.
• Generalización: Los resultados sugieren que los datos sintetizados enseñan efectivamente a los modelos no solo la sintaxis, sino también los patrones de razonamiento complejos requeridos para verificar software de sistema del mundo real, una capacidad que anteriormente se pensaba exclusiva de los modelos más grandes.

Los autores concluyen que su conjunto de datos de entrenamiento está disponible en HuggingFace, con el objetivo de reducir la barrera de entrada para la verificación formal en el desarrollo de software de sistema.