Resumen Técnico: VeriScale: Escalado de Conjuntos de Pruebas Adversariales para la Generación de Código Verificable

Declaración del Problema

A medida que los Modelos de Lenguaje Grande (LLM) se implementan cada vez más en la ingeniería de software, evaluar su capacidad para generar no solo código funcional, sino también especificaciones y pruebas formalmente verificables, se ha vuelto crítico. Las puntuaciones existentes para la generación de código verificable, como VERINA y CLEVER, dependen en gran medida de la evaluación mediante conjuntos de pruebas para evaluar la Generación de Especificaciones (SpecGen) y la Generación de Código (CodeGen). Sin embargo, estas puntuaciones adolecen de una limitación fundamental: están restringidas por la escasez de casos de prueba de alta calidad, particularmente casos de prueba negativos (entradas inesperadas y salidas inesperadas).

Las puntuaciones actuales suelen proporcionar solo un número limitado de pares de entrada-salida positivos. En consecuencia, los modelos pueden lograr tasas de aprobación infladas al satisfacer estas pruebas escasas sin capturar verdaderamente la intención del programa ni garantizar la solidez y la completitud de sus especificaciones generadas. Esto conduce a una sobreestimación de las capacidades del modelo, donde implementaciones incorrectas o especificaciones no sólidas superan la evaluación simplemente porque el conjunto de pruebas no logra exponer fallos lógicos o violaciones de límites.

Metodología: El Marco VeriScale

Para abordar estas limitaciones, los autores proponen VeriScale, un marco novedoso impulsado por implementaciones adversariales para escalar y refinar sistemáticamente los conjuntos de pruebas para la generación de código verificable. El marco opera en dos etapas principales: Expansión del Conjunto de Pruebas y Reducción del Conjunto de Pruebas.

1. Expansión del Conjunto de Pruebas

El objetivo de esta etapa es construir un conjunto diverso y desafiante de casos de prueba, que incluya pares de entrada-salida esperados, entradas inesperadas y salidas inesperadas.

• Generación de Semillas y Mutación Consciente del Tipo: Inspirándose en EvalPlus, VeriScale utiliza LLMs para sintetizar entradas de semilla iniciales. Estas semillas se expanden mediante una estrategia de mutación iterativa y consciente del tipo. El marco formaliza la mutación como un proceso de quintupla ($M = (T, D, O, p, q)$) que preserva los tipos de entrada mientras introduce perturbaciones estructurales. Esto incluye reutilizar valores contextuales de un "pool de ingredientes" o aplicar heurísticas específicas del tipo para generar casos límite complejos.
• Clasificación de Entradas Guiada por Precondiciones: Las entradas candidatas se clasifican rigurosamente frente a precondiciones de verdad fundamental utilizando una tubería de verificación de dos etapas en Lean.
  • Filtro de Sintaxis: Asegura que las candidatas sean expresiones Lean sintácticamente válidas.
  • Verificación Bidireccional: Utiliza #guard decide y búsqueda de pruebas plausible para clasificar las entradas como "esperadas" (que satisfacen la precondición) o "inesperadas" (que la violan).
• Síntesis Adversarial de Salidas Inesperadas: Esta es la innovación central. En lugar de confiar en que los LLMs alucinen salidas incorrectas aleatorias, VeriScale sintetiza implementaciones adversariales.
  • Un modelo capaz actúa como un "equipo rojo", generando especificaciones formales para un problema.
  • Otro modelo (o el mismo en un rol diferente) intenta crear implementaciones adversariales diseñadas para explotar las debilidades de estas especificaciones.
  • Estas implementaciones se ejecutan en entradas esperadas. Si una implementación adversarial produce una salida que difiere de la verdad fundamental pero es falsamente aceptada por las postcondiciones generadas, esta salida se retiene como una "salida inesperada" de alta calidad. Este proceso asegura que los casos de prueba sean genuinamente informativos para exponer la falta de solidez de las especificaciones.

2. Reducción del Conjunto de Pruebas

Para gestionar el costo computacional de los conjuntos expandidos, VeriScale emplea estrategias de reducción para destilar el gran conjunto en conjuntos compactos pero discriminativos.

• Reducción que Preserva Límites (para Entradas Inesperadas): En lugar de muestreo aleatorio, esta estrategia prioriza entradas que corresponden a violaciones de límites comunes (por ejemplo, contenedores vacíos, valores cero, longitudes no coincidentes). Retiene ejemplos representativos de cubos de límites críticos para asegurar la cobertura de violaciones típicas de precondiciones.
• Reducción de Eliminación de Adversarios (para Entradas Esperadas): Esta estrategia reaprovecha las implementaciones adversariales sintetizadas en la fase de expansión. Cada par de entrada-salida esperado se evalúa en función de cuántas implementaciones "mutantes" (adversariales) puede "eliminar" (es decir, producir una salida diferente). La reducción se formula como un problema de cobertura de conjuntos, seleccionando de manera codiciosa pares que cubran el número máximo de mutantes previamente no eliminados. Esto asegura que el conjunto reducido mantenga la capacidad de distinguir especificaciones defectuosas.

Contribuciones Clave

1. Marco VeriScale: Los autores proponen un marco general que aprovecha las implementaciones adversariales para impulsar tanto la expansión sistemática como la reducción de conjuntos de pruebas para la generación de código verificable.
2. VERINAPLUS y VERINALITE: El marco se instancia en la puntuación VERINA para crear dos nuevos conjuntos de datos:
   • VERINAPLUS: Una puntuación expandida con conjuntos de pruebas escalados en más de 83× (específicamente 62.83× para entradas esperadas, 87.79× para salidas inesperadas y 183.08× para entradas inesperadas).
   • VERINALITE: Una variante ligera escalada en 14×, optimizada mediante estrategias de reducción para mantener el poder discriminativo con menores costos de evaluación.
3. Validación Empírica: El documento demuestra que las puntuaciones originales sobreestiman significativamente las capacidades del modelo. Las puntuaciones mejoradas revelan debilidades sustanciales en los LLMs más avanzados que anteriormente permanecían ocultas.

Resultados Experimentales

Los autores evaluaron ocho LLMs de última generación (incluyendo GPT-5.5, Claude-Sonnet-4.6 y DeepSeek-V4-Pro) en VERINA, VERINAPLUS y VERINALITE.

• Exposición de Debilidades del Modelo: Las puntuaciones aumentadas provocaron caídas bruscas en el rendimiento. Por ejemplo, GPT-5.5 vio su puntuación de SpecGen desplomarse del 68.78% en VERINA al 44.44% en VERINAPLUS, y su puntuación de CodeGen cayó del 96.83% al 86.24%. Esto indica que los casos de prueba escasos de la puntuación original permitían que los modelos pasaran sin una comprensión real.
• Reducción de la Incertidumbre de Evaluación: Los conjuntos de pruebas expandidos redujeron significativamente las barras de error en la evaluación de SpecGen. En la puntuación original, los resultados de verificación indeterminados creaban brechas amplias entre los límites superior e inferior (por ejemplo, una brecha del 13.23% para Claude-Opus-4.7). En VERINAPLUS, esta ambigüedad se resolvió, reduciendo la brecha al 4.76%, proporcionando una evaluación estadísticamente más fiable.
• Brecha de Robustez: Los resultados destacan una disparidad fundamental: los modelos son significativamente más proficientes en CodeGen que en SpecGen. Mientras que las puntuaciones de CodeGen experimentaron descensos moderados, las puntuaciones de SpecGen sufrieron caídas precipitosas, lo que sugiere que sintetizar especificaciones formales sólidas y completas sigue siendo un cuello de botella importante para los LLMs actuales.
• Eficiencia de la Reducción: VERINALITE logró perfiles de degradación de rendimiento casi idénticos a VERINAPLUS, pero con una sobrecarga computacional significativamente reducida. El tiempo de evaluación para VERINALITE fue solo 1.38× (SpecGen) y 1.05× (CodeGen) de la línea base, en comparación con 1.80× y 1.50× para el conjunto completo de VERINAPLUS.

Significado y Afirmaciones

El documento afirma que VeriScale proporciona un estándar crucial y altamente fiable para avanzar en la generación de código verificable basada en LLM. Al ir más allá de las pruebas positivas escasas para incluir casos negativos sintetizados adversarialmente, el marco ofrece una evaluación más rigurosa que previene la sobreestimación de las capacidades del modelo.

Los autores posicionan a VeriScale como complementario a los esfuerzos existentes; en lugar de introducir nuevas tareas, fortalece las puntuaciones existentes al escalar la calidad y la cantidad de señales de prueba. El trabajo subraya la necesidad del escalado adversarial de pruebas para exponer la fragilidad de los modelos actuales en tareas de razonamiento formal.

Limitaciones Reconocidas:
Los autores señalan que VeriScale depende de la disponibilidad de precondiciones de verdad fundamental e implementaciones de referencia. Además, la calidad de las salidas inesperadas sintetizadas está limitada por las capacidades de razonamiento del LLM que actúa como "equipo rojo". Finalmente, la fase de construcción sigue siendo intensiva en cómputo, requiriendo muestreo masivo de LLM y ejecuciones de Lean.

Trabajo Futuro:
Los autores proponen evolucionar VeriScale hacia un sistema de reparación de bucle cerrado para guiar a los modelos en la corrección de especificaciones defectuosas. También planean utilizar VeriScale como un motor de datos adversarial para sintetizar corpus de entrenamiento para modelos de autoformalización dedicados y generalizar el marco a otros motores de verificación como Dafny.