Resumen Técnico: VeriContest

Enunciado del Problema

Aunque los Modelos de Lenguaje Grandes (LLM) han demostrado competencia en la generación de código ejecutable a partir de lenguaje natural, sus salidas carecen de garantías formales de corrección. Los enfoques basados en pruebas existentes solo muestrean el comportamiento del programa y no pueden garantizar la ausencia de errores funcionales o defectos de seguridad. La verificación formal ofrece una alternativa más sólida al exigir pruebas verificables por máquina de que el código satisface especificaciones formales. Sin embargo, el progreso en la "generación de código verificable", donde un modelo debe producir código, especificaciones formales y pruebas simultáneamente, se ve obstaculizado por la falta de puntos de referencia rigurosos. Los puntos de referencia actuales suelen ser pequeños, se centran en etapas aisladas del pipeline (por ejemplo, solo código o solo pruebas), carecen de pruebas de verdad fundamental o se dirigen a entornos de verificación desconectados del desarrollo de software convencional.

Metodología

Los autores presentan VeriContest, un punto de referencia compuesto por 946 problemas de programación competitiva obtenidos de LeetCode y Codeforces, diseñados específicamente para la generación de código verificable en Rust utilizando el marco de verificación Verus.

Pipeline de Construcción del Punto de Referencia

VeriContest se construye mediante un pipeline de tres fases para garantizar alta calidad y escala:

1. Fase I (Construcción Manual): Expertos construyeron manualmente 91 problemas "semilla". Para cada uno, redactaron especificaciones formales (precondiciones y postcondiciones), código Rust aceptado por el juez y pruebas verificadas por Verus. Estas especificaciones se validaron rigurosamente en cuanto a corrección (cualquier solución correcta satisface la especificación) y completitud (cualquier solución que satisface la especificación es correcta).
2. Fase II (Expansión Semiautomática): Un agente LLM (respaldado por GPT-5.3-Codex) expandió el punto de referencia a 946 problemas. Esta fase empleó un proceso de revisión con "humano en el bucle". El agente filtró problemas que requerían características de Rust no soportadas (por ejemplo, aritmética de punto flotante, estructuras de datos complejas) y generó especificaciones, código y pruebas. Expertos humanos verificaron la salida mediante aceptación en el juez en línea, revisión manual de especificaciones y verificación independiente con Verus.
3. Fase III (Generación y Validación de Casos de Prueba): Para validar la completitud de las postcondiciones, los autores generaron suites de pruebas positivas y negativas.
   • Pruebas Positivas: Generadas sintetizando programas generadores verificados por Verus que producen entradas válidas.
   • Pruebas Negativas: Generadas mediante pruebas de mutación (mutación semántica, sintáctica y de salida directa) para crear entradas emparejadas con salidas incorrectas.
   • Post2Exe: Una herramienta novedosa que convierte las postcondiciones de Verus soportadas en programas ejecutables en Rust. Estas se ejecutan contra casos de prueba negativos para detectar y señalar automáticamente postcondiciones incompletas (aquellas que aceptan salidas incorrectas), las cuales se envían de nuevo para su revisión.

Protocolo de Evaluación

VeriContest soporta evaluaciones aisladas y composicionales en cuatro tareas principales:

• SpecGen: Generación de especificaciones formales a partir de lenguaje natural.
• CodeGen: Generación de código ejecutable a partir de lenguaje natural, especificaciones o ambas.
• ProofGen: Generación de pruebas Verus dada una especificación y código.
• Extremo a Extremo: Generación del programa verificado completo (especificación, código y prueba) a partir de una descripción en lenguaje natural.

La evaluación mide la precisión pass@1, con métricas adicionales para la reparación de pruebas (repair@k) y el muestreo (pass@k).

Contribuciones Clave

1. Punto de Referencia VeriContest: Un conjunto de datos a gran escala de 946 problemas de programación competitiva que incluye especificaciones Verus validadas por expertos, código Rust aceptado por el juez, pruebas Verus de verdad fundamental y suites de pruebas positivas/negativas completas.
2. Pipeline de Construcción: Una metodología escalable de tres fases que combina la creación manual de semillas, la expansión semiautomática con revisión humana y la validación automatizada basada en pruebas de la completitud de las postcondiciones mediante Post2Exe.
3. Marco de Evaluación Modular: Un protocolo que aísla la generación de especificaciones, código y pruebas, al tiempo que evalúa la síntesis de extremo a extremo, permitiendo un análisis granular de los cuellos de botella.
4. Análisis Empírico: Una evaluación de diez LLMs de última generación (incluyendo GPT-5.5, Claude Opus 4.7 y DeepSeek V4) que revela brechas significativas de rendimiento entre la codificación estándar y la generación de código verificable.

Resultados

La evaluación de diez modelos de última generación en VeriContest revela una caída pronunciada en el rendimiento a medida que la complejidad de la tarea aumenta desde la generación de código hasta la verificación completa:

• Generación de Código (CodeGen): Los modelos se desempeñan relativamente bien. El modelo más fuerte, GPT-5.5, alcanza una precisión del 92.18% en la generación de código a partir de lenguaje natural. Sin embargo, el rendimiento disminuye significativamente cuando la entrada es una especificación formal únicamente (67.65%), lo que sugiere una discrepancia en la distribución de entrenamiento donde los modelos están más familiarizados con enunciados de problemas en lenguaje natural que con restricciones lógicas formales.
• Generación de Especificaciones (SpecGen): El rendimiento cae bruscamente. GPT-5.5 alcanza solo el 48.31% en la generación de especificaciones a partir de lenguaje natural, y los modelos de código abierto se desempeñan significativamente peor (por ejemplo, Qwen 3.6 con 0.32%). Esto indica que los LLMs están mucho menos familiarizados con la sintaxis y semántica de las especificaciones formales que con el código.
• Generación de Pruebas (ProofGen): Esto se identifica como el principal cuello de botella. Incluso con especificaciones y código de verdad fundamental proporcionados, GPT-5.5 alcanza solo una precisión del 13.95%. La mayoría de los modelos permanecen por debajo del 8%.
• Extremo a Extremo: La tasa de éxito para generar un programa completamente verificado desde cero es extremadamente baja. GPT-5.5 alcanza solo el 5.29%. Los autores señalan que el éxito de extremo a extremo requiere que la especificación, el código y la prueba se alineen perfectamente; un fallo en cualquier componente individual provoca que todo el pipeline falle.

Análisis de Errores:

• CodeGen: Los errores están dominados por salidas incorrectas para modelos fuertes, pero cambian a errores de sintaxis cuando se involucran especificaciones formales.
• ProofGen: El modo de fallo dominante es el Fallo de Verificación (la prueba no satisface al verificador) y la Modificación de Especificación/Código (modelos que alteran el código/especificación proporcionados en lugar de simplemente agregar pruebas).
• SpecGen: Los errores están fuertemente dominados por errores de sintaxis en Verus, seguidos de discrepancias en las pre/postcondiciones.

Significado y Afirmaciones

El artículo afirma que VeriContest establece una plataforma rigurosa para medir y entrenar sistemas futuros capaces de generar código con corrección verificable por máquina. Los autores afirman que:

• La generación de pruebas y especificaciones son los cuellos de botella centrales para los LLMs actuales en el pipeline de generación de código verificable.
• Existe una brecha sustancial entre la capacidad de un modelo para escribir código y su capacidad para verificarlo formalmente.
• El éxito de extremo a extremo está limitado actualmente no solo por la generación de código, sino por la dificultad de alinear especificaciones, código y pruebas en un todo consistente.
• El punto de referencia sirve como fuente de supervisión para entrenar modelos en la generación de código verificable, avanzando más allá de la simple corrección funcional hacia garantías formales.

Los autores mantienen modestia respecto al alcance, reconociendo que VeriContest se limita a Rust/Verus y problemas de programación competitiva, y aún no cubre código de sistemas, protocolos distribuidos u otros marcos de verificación como Dafny o Lean. Sugieren que el trabajo futuro debería expandirse a más lenguajes y dominios a medida que mejoren las herramientas y las capacidades de los modelos.