Clasificación de Invariantes de Bucle Generados por LLM para la Verificación de Programas

Ranking LLM-Generated Loop Invariants for Program Verification

October 13, 2023

Autores: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy

cs.AI

Resumen

La síntesis de invariantes inductivos para bucles es fundamental para automatizar la verificación de programas. En este trabajo, observamos que los Modelos de Lenguaje de Gran Escala (como gpt-3.5 o gpt-4) son capaces de sintetizar invariantes de bucles para una clase de programas en un entorno de 0-shot, aunque requieren varias muestras para generar los invariantes correctos. Esto puede llevar a un gran número de llamadas a un verificador de programas para establecer un invariante. Para abordar este problema, proponemos un enfoque de {\it reordenación} para los resultados generados por los LLMs. Hemos diseñado un clasificador que puede distinguir entre invariantes inductivos correctos e intentos incorrectos basándose en la definición del problema. El clasificador está optimizado como un clasificador contrastivo. Los resultados experimentales demuestran que este mecanismo de reordenación mejora significativamente la clasificación de los invariantes correctos entre los candidatos generados, lo que conduce a una notable reducción en el número de llamadas a un verificador.

English

Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier.