Investigadores de la Universidad de Purdue en EE.UU. han presentado SynVer, un marco innovador de síntesis y verificación para programas en C, diseñado para optimizar la validación automática mediante Modelos de Lenguaje Grande (LLM). Este sistema busca automatizar la generación de programas que cumplan con especificaciones predefinidas, al tiempo que introduce un sesgo sintáctico y semántico que facilita su verificación. La herramienta se construye sobre la base del Verified Software Toolchain para fortalecer el proceso de verificación automatizada.
El estudio, que involucró varios conjuntos de pruebas provenientes de la comunidad de síntesis de programas deductivos, demostró que este enfoque es tanto escalable como extensible. Las especificaciones incluyeron ejemplos básicos de codificación, aseveraciones basadas en la lógica de separación, y especificaciones de API. El objetivo central de la síntesis de programas es generar automáticamente un programa que satisfaga una especificación dada, que puede estar en forma de ejemplos, lenguaje natural o formulaciones matemáticas rigurosas. Tradicionalmente, la síntesis de programas aplica técnicas deductivas para derivar un programa correcto a partir de una especificación, pero este proceso suele ser costoso en términos de tiempo y recursos debido a la amplia variedad de candidatos potenciales y la dificultad de verificación.
SynVer adopta una estrategia diferente utilizando un LLM para generar una solución que sea verificable automáticamente. A pesar de que los LLM se presentan como herramientas poderosas para la generación de programas gracias a sus habilidades de procesamiento de lenguaje, existe un desafío debido a que el modelo es una “caja negra” y la salida del programa no es correcta por construcción. Por tanto, se requiere un esfuerzo considerable para verificar su corrección conforme a especificaciones lógicas ricas.
Para abordar estas restricciones, el equipo desarrolló una herramienta de verificación de especificaciones novedosa, que se integra al Verified Software Toolchain, capaz de manejar programas sintetizados de acuerdo con el sesgo impuesto y procediendo a su verificación automatizada en tres dominios problemáticos distintos.
El artículo detalla cómo se identificaron dos principales cuellos de botella que obstaculizan la verificación mediante estudios formativos, además de describir tácticas específicas que usan para resolver dichas barreras. El marco SynVer también aborda cómo establecer límites en el espacio de búsqueda utilizando restricciones que simplifiquen la verificación, incluyendo el uso restringido de funciones auxiliares y el soporte para la recursión sobre los bucles, con la finalidad de facilitar la inferencia de invariantes de bucles.