Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

1. El Problema

La verificación de programas busca garantizar formalmente que el software se comporta como se espera, lo cual es crucial en dominios de seguridad crítica. Un desafío fundamental y de larga data en este campo es la descubrimiento automático de invariantes de bucle.

• Naturaleza del desafío: Para verificar un bucle, se necesita un invariante (una condición que se mantiene antes y después de cada iteración). Sin embargo, no basta con que el invariante sea correcto; debe ser lo suficientemente fuerte para probar la aserción final del programa.
• Limitaciones de enfoques anteriores:
  • Los métodos tradicionales (resolución de restricciones, análisis dinámico) a menudo luchan con la complejidad o la decidibilidad.
  • Los trabajos previos que utilizan Modelos de Lenguaje Grande (LLMs) (como Pei et al., 2023) sufren de dos fallos principales:
    1. Solo evalúan la corrección del invariante, no si acelera la verificación.
    2. Utilizan herramientas de análisis dinámico (como Daikon) para validar, lo cual es insound (no formalmente seguro) y puede rechazar invariantes semánticamente equivalentes pero sintácticamente diferentes.
  • Otros enfoques basados en LLMs (como LaM4Inv, LEMUR, Loopy) tratan la salida del LLM como "material simbólico ruidoso" que requiere algoritmos complejos de post-procesamiento (filtrado, reensamblaje, reparación) antes de poder ser usado por un verificador.

2. Metodología: Quokka

El artículo introduce Quokka, un marco de trabajo orientado a la evaluación para la síntesis de invariantes basada en LLMs. Su diseño se centra en la simplicidad y la validación directa.

Enfoque Central

A diferencia de trabajos anteriores que intentan "arreglar" la salida del LLM, Quokka adopta una filosofía centrada en la evaluación:

1. Validación Directa: El sistema envía directamente el invariante propuesto por el LLM a un verificador formal para determinar dos cosas:
   • ¿Es el invariante correcto? (Se verifica si se mantiene en el bucle).
   • ¿Es útil? (Se verifica si, asumiendo que el invariante es cierto, se puede probar la aserción objetivo).
2. Consulta Paralela: Para cada candidato, se ejecutan dos consultas al verificador en paralelo:
   • da: Verifica si el invariante q es válido en el programa P.
   • db: Verifica si la propiedad objetivo p* se cumple en P bajo la suposición de q.
3. Lógica de Decisión:
   • Si db devuelve "Falso" (refutación), el objetivo es falso.
   • Si da es "Verdadero" y db es "Verdadero", el objetivo está probado.
   • Si alguna consulta no concluye (timeout o inconcluso), el resultado es inconcluso.
   • Este enfoque elimina la necesidad de algoritmos complejos de reparación o reensamblaje de predicados.

Generación de Datos y Entrenamiento

• Dataset de Evaluación: Se construyó un benchmark de 866 instancias derivadas de la competencia SV-COMP (2025). Es el conjunto de datos más grande y complejo hasta la fecha para verificadores basados en LLMs, incluyendo bucles múltiples, funciones, arrays y punteros.
• Dataset de Entrenamiento: Se generaron 3589 instancias sintéticas utilizando un enfoque de filtrado basado en verificadores (UAutomizer) para asegurar la calidad de los datos.
• Técnicas de Mejora:
  • Fine-Tuning Supervisado (SFT): Se aplicó LoRA a modelos como Qwen2.5-7B utilizando los invariantes generados por el verificador como "ground truth".
  • Muestreo Best-of-N: Se generan múltiples candidatos y se selecciona aquel que ofrece la mayor aceleración en la verificación (evaluando $2N$ consultas concurrentemente).

3. Contribuciones Clave

1. Marco de Evaluación Sound: Introducción de un algoritmo de evaluación basado en verificadores formales que garantiza la corrección y mide directamente la utilidad práctica (aceleración) de los invariantes generados por LLMs.
2. Benchmark de Gran Escala: Creación de un dataset de 866 instancias que supera en complejidad y tamaño a los conjuntos de datos utilizados en trabajos anteriores (LaM4Inv, Clause2Inv, LEMUR, Loopy).
3. Rendimiento State-of-the-Art: Demostración de que un diseño simple y centrado en la evaluación supera a sistemas complejos que dependen de algoritmos de reparación simbólica.
4. Análisis de Técnicas de Mejora: Evidencia empírica de que el fine-tuning y el Best-of-N sampling proporcionan mejoras medibles en la aceleración de la verificación.

4. Resultados Experimentales

El estudio evaluó 9 LLMs de última generación (incluyendo GPT-5, Claude 4, Qwen2.5, Llama-3.1) sobre el benchmark de Quokka.

• Rendimiento General:
  • Los modelos más grandes y recientes (ej. gpt-5.2, claude-opus-4.5) lograron los mejores resultados.
  • gpt-5.2 resolvió 710 de 866 instancias (con un tiempo promedio de 22.2s bajo un límite de 60s), superando significativamente al verificador base (UAutomizer) que no utilizaba LLMs.
  • Se observó una aceleración significativa en problemas de dificultad moderada, aunque los casos más difíciles aún presentan desafíos.
• Comparación con el Estado del Arte:
  • Quokka superó consistentemente a LEMUR, Clause2Inv, Loopy y LaM4Inv en todas las métricas de tiempo de espera (timeout) y número de instancias resueltas.
  • En un benchmark específico donde UAutomizer fallaba en 10 minutos, Quokka resolvió sustancialmente más instancias que LEMUR con tiempos de solución más bajos.
• Impacto del Fine-Tuning y Best-of-N:
  • El fine-tuning en Qwen2.5-7B aumentó ligeramente los invariantes correctos (de 419 a 431) y las instancias resueltas adicionales.
  • El muestreo Best-of-N mostró mejoras significativas hasta $N=8$, donde se alcanzó el rendimiento óptimo antes de que los costos de recursos compensaran las ganancias.

5. Significado e Implicaciones

El trabajo de Quokka representa un cambio de paradigma en la verificación de programas asistida por LLMs:

1. Simplicidad vs. Complejidad: Demuestra que a medida que los modelos de lenguaje se vuelven más capaces, no es necesario diseñar algoritmos simbólicos complejos para "rescatar" sus salidas. Un diseño simple que evalúa directamente la validez de la propuesta es más eficiente y robusto.
2. Validación Formal: Establece un nuevo estándar para la evaluación de LLMs en tareas de verificación, moviéndose más allá de la mera corrección sintáctica hacia la utilidad práctica en la aceleración de la prueba formal.
3. Escalabilidad: Al eliminar la sobrecarga de post-procesamiento y permitir consultas paralelas, Quokka ofrece una ruta escalable para integrar LLMs en flujos de trabajo de verificación industrial.

En resumen, Quokka demuestra que los LLMs pueden acelerar efectivamente la verificación de programas si se les evalúa mediante un marco sound y centrado en la utilidad, logrando un rendimiento superior al estado del arte actual con una arquitectura significativamente más simple.