Aprovechamiento de Modelos de Lenguaje a Gran Escala para la Síntesis Automatizada de Pruebas en Rust
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
Autores: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
Resumen
La verificación formal puede garantizar de manera demostrable la corrección del software crítico de sistemas, pero la alta carga de pruebas ha obstaculizado durante mucho tiempo su adopción generalizada. Recientemente, los Modelos de Lenguaje de Gran Escala (LLMs, por sus siglas en inglés) han mostrado éxito en el análisis y síntesis de código. En este artículo, presentamos una combinación de LLMs y análisis estático para sintetizar invariantes, aserciones y otras estructuras de prueba para un marco de verificación formal basado en Rust llamado Verus. En un entorno de pocos ejemplos, los LLMs demuestran una impresionante capacidad lógica para generar postcondiciones e invariantes de bucle, especialmente al analizar fragmentos de código cortos. Sin embargo, los LLMs carecen de la capacidad para retener y propagar información de contexto, una fortaleza del análisis estático tradicional. Basándonos en estas observaciones, desarrollamos un prototipo basado en el modelo GPT-4 de OpenAI. Nuestro prototipo descompone la tarea de verificación en múltiples subtareas más pequeñas, consulta iterativamente a GPT-4 y combina su salida con un análisis estático ligero. Evaluamos el prototipo con un desarrollador en el bucle de automatización en 20 programas que manipulan vectores. Los resultados demuestran que reduce significativamente el esfuerzo humano en la escritura de código de prueba de nivel básico.
English
Formal verification can provably guarantee the correctness of critical system
software, but the high proof burden has long hindered its wide adoption.
Recently, Large Language Models (LLMs) have shown success in code analysis and
synthesis. In this paper, we present a combination of LLMs and static analysis
to synthesize invariants, assertions, and other proof structures for a
Rust-based formal verification framework called Verus. In a few-shot setting,
LLMs demonstrate impressive logical ability in generating postconditions and
loop invariants, especially when analyzing short code snippets. However, LLMs
lack the ability to retain and propagate context information, a strength of
traditional static analysis. Based on these observations, we developed a
prototype based on OpenAI's GPT-4 model. Our prototype decomposes the
verification task into multiple smaller ones, iteratively queries GPT-4, and
combines its output with lightweight static analysis. We evaluated the
prototype with a developer in the automation loop on 20 vector-manipulating
programs. The results demonstrate that it significantly reduces human effort in
writing entry-level proof code.