Resumen Técnico: Diversificar para Verificar

Planteamiento del Problema

Si bien los Modelos de Lenguaje de Gran Escala (LLMs) se han vuelto efectivos para sintetizar código ejecutable a partir de lenguaje natural, la generación de software formalmente verificado sigue siendo un desafío significativo. En los marcos de verificación deductiva como Why3, la corrección no se establece simplemente mediante el paso de casos de prueba; requiere una especificación semántica formal (contratos, precondiciones, postcondiciones) y una guía de prueba suficiente (invariantes, variantes, lemas) para satisfacer a un demostrador de teoremas automatizado.

El problema central abordado es que la estructura de implementación de un programa —específicamente su representación de datos (p. ej., arreglos frente a listas) y su flujo de control (p. ej., recursivo frente a imperativo)— puede afectar drásticamente su verificabilidad automatizada. Una sola semántica de nivel de tarea puede ser satisfecha por múltiples implementaciones, pero algunas estructuras pueden generar condiciones de verificación intratables para los solvers SMT actuales, mientras que otras son fácilmente demostrables. Los enfoques existentes suelen tratar la generación de código como una tarea de un solo paso, fallando al no aprovechar el potencial de la diversidad de implementación para encontrar artefactos "amigables para la verificación".

Metodología: Diversify2Verify

Los autores introducen Diversify2Verify, un pipeline basado en LLM de etapas sucesivas diseñado para generar y verificar artefactos de Why3. El pipeline descompone el proceso de generación en tres etapas distintas, imponiendo límites estrictos para asegurar que el éxito de la verificación no se logre debilitando la especificación o alterando la semántica fundamental de la tarea.

1. Arquitectura del Pipeline

• Etapa 1: Generación de Contratos.
  • Entrada: Tarea en lenguaje natural, firma objetivo, ejemplos concretos y una representación objetivo (arreglo o lista).
  • Proceso: El LLM infiere un contrato formal específico de la representación (precondiciones, postcondiciones, predicados auxiliares).
  • Validación: El contrato es verificado por tipos en Why3, y se intenta demostrar los "lemas de prueba" derivados de los ejemplos concretos.
  • Política: Una vez que un contrato pasa la validación, este queda congelado. Sirve como el objetivo semántico inmutable para las etapas posteriores. La reparación está permitida solo antes de la congelación para corregir sintaxis, tipos o inconsistencias semánticas con los ejemplos.
• Etapa 2: Generación de Implementación.
  • Proceso: El pipeline genera candidatos de WhyML ejecutables para el mismo contrato congelado.
  • Estrategia de Diversidad: Para cada tarea, se generan cuatro familias de implementación distintas:
    1. Arreglo-Recursivo
    2. Arreglo-Imperativo
    3. Lista-Recursiva
    4. Lista-Imperativa
  • Validación: Los candidatos son filtrados por verificación de tipos y por pasar un subconjunto de pruebas ejecutables.
  • Política: La reparación es limitada (5 intentos) y restringida a la misma representación y familia de estructura de control (por ejemplo, un candidato de arreglo-imperativo no puede ser reparado para convertirse en uno de lista-recursiva).
• Etapa 3: Verificación Completa y Reparación.
  • Proceso: El contrato congelado y una implementación probada se combinan. El LLM añade las anotaciones de prueba necesarias (invariantes de bucle, variantes, código fantasma, aserciones) para conectar el estado local del programa con el contrato global.
  • Verificación: Why3 (con solvers SMT como Z3, Alt-Ergo, CVC4) intenta descargar todas las condiciones de verificación.
  • Política de Reparación: Si la verificación falla, se realiza una reparación limitada (2 intentos). Las reparaciones son estrictamente orientadas a la prueba (fortalecimiento de invariantes, adición de lemas) y deben preservar el contrato congelado y la familia de implementación.

2. Construcción del Benchmark

Los autores construyeron un benchmark orientado a la verificación derivado de LeetCodeDataset:

• Alcance: 73 tareas que involucran enteros, arreglos y listas.
• Criterios de Selección: Las tareas fueron filtradas para asegurar que admiten contratos formales, soportan múltiples implementaciones plausibles y son adecuadas para el razonamiento respaldado por SMT.
• Escala: El benchmark produce 292 variantes de implementación (4 por tarea).
• Nota: El benchmark está intencionalmente sesgado hacia tipos de datos amigables para SMT para aislar el efecto de la representación y la estructura de control en la verificabilidad.

Contribuciones Clave

1. Pipeline Diversify2Verify: Un pipeline de LLM por etapas que separa la inferencia de contratos, la generación de implementación y la anotación de pruebas, imponiendo una disciplina de "contrato congelado" para evitar la deriva de la especificación durante la reparación.
2. Generación de Implementación Diversa: Un enfoque sistemático para generar variantes recursivas e imperativas sobre tanto representaciones de arreglos como de listas, permitiendo la comparación directa de programas estructuralmente diferentes contra un mismo objetivo semántico.
3. Benchmark Orientado a la Verificación: Un conjunto curado de 73 tareas con 292 artefactos generados, que incluye contratos aceptados, implementaciones en WhyML y registros de verificación, publicado de forma abierta.
4. Estudio Empírico de la Verificabilidad: Un análisis que cuantifica cómo el éxito de la verificación varía según la representación y el estilo de implementación, y mide las ganancias obtenidas de la generación de múltiples variantes.

Resultados

La evaluación demuestra que la diversidad de implementación mejora significamente la tasa de éxito de la verificación automatizada:

• Verificación a Nivel de Artefacto:
  • Inicial: 96 de 292 artefactos (32.9%) se verificaron sin reparación.
  • Después de la Reparación: 154 de 292 artefactos (52.7%) se verificaron tras dos pasadas de reparación.
  • Impacto de la Reparación: La reparación fue responsable de verificar 58 artefactos adicionales, siendo la primera pasada la que produjo la mayor ganancia.
• Verificación a Nivel de Tarea:
  • Al menos una variante se verificó para 49 de las 73 tareas, logrando una tasa de éxito del 67.1% a nivel de tarea.
  • La familia individual más fuerte (Arreglo-Recursivo) verificó 44 tareas.
  • Esto indica que la diversidad proporciona un aumento medible en la cobertura de tareas; depender de un único estilo de implementación omitiría muchas tareas que son resolubles.
• Diferencias Estructurales:
  • Recursivo vs. Imperativo: Las variantes recursivas se verificaron con más frecuencia (60.3% para arreglos, 54.8% para listas) que las variantes imperativas (47.9% para ambos). Esto se atribuye a que las implementaciones recursivas suelen alinearse mejor con las especificaciones recursivas, mientras que las implementaciones imperativas requieren invariantes de bucle complejos para resumir el estado mutable.
  • Arreglo vs. Lista: Las tasas de verificación agregadas para arreglos y listas fueron similares, lo que sugiere que la elección de la estructura de control (recursivo vs. imperativo) tiene un efecto más pronunciado que la elección de la representación de datos en este contexto.
• Análisis de Fallos:
  • La mayoría de los artefactos no verificados (138 restantes) tenían muy pocas obligaciones de prueba pendientes (promedio de 2.5 objetivos raíz), lo que sugiere que los fallos se debieron a la falta de andamiaje de prueba (p. ej., invariantes específicos) más que a implementaciones fundamentalmente incorrectas.
  • Una auditoría manual confirmó que el pipeline preservó exitosamente los contratos congelados en 291 de 292 casos, habiéndose encontrado solo un caso donde el LLM añadió precondiciones no presentes en el contrato original.

Significancia y Reivindicaciones

El artículo sostiene que las implementaciones equivalentes a una tarea pueden diferir sustancialmente en su verificabilidad. La hipótesis central es respaldada: generar variantes diversas aumenta la probabilidad de encontrar una implementación cuya estructura sea propicia para la verificación deductiva automatizada.

Los autores enfatizan que este enfoque no depende de una única generación "perfecta", sino de la diversidad como una herramienta práctica para navegar el espacio de búsqueda de las condiciones de verificación. Al desacoplar la generación de la especificación de la generación de la implementación y aplicar límites estrictos durante la reparación, el sistema asegura que el éxito de la verificación no se logre mediante el debilitamiento de la especificación o el cambio de la semántica de la tarea.

El trabajo sugiere que, para la programación verificada asistida por LLM, la diversidad de implementación es un mecanismo poderoso para mejorar la cobertura de tareas, particularmente cuando se combina con una reparación guiada por el verificador y de alcance limitado. Los autores señalan que estos hallazgos son específicos al contexto de tareas de enteros y secuencias usando Why3, y sugieren que trabajos futuros deberían explorar estructuras de datos más ricas y otros marcos de verificación.