Classifica delle invarianti di ciclo generate da LLM per la verifica dei programmi

Ranking LLM-Generated Loop Invariants for Program Verification

October 13, 2023

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

cs.AI

Abstract

La sintesi di invarianti induttivi per cicli è fondamentale per automatizzare la verifica dei programmi. In questo lavoro, osserviamo che i Large Language Model (come gpt-3.5 o gpt-4) sono in grado di sintetizzare invarianti per cicli per una classe di programmi in un contesto zero-shot, ma richiedono diversi campioni per generare gli invarianti corretti. Ciò può portare a un numero elevato di chiamate a un verificatore di programmi per stabilire un invariante. Per affrontare questo problema, proponiamo un approccio di {\it riordinamento} per i risultati generati dai LLM. Abbiamo progettato un sistema di ordinamento in grado di distinguere tra invarianti induttivi corretti e tentativi errati basandosi sulla definizione del problema. Il sistema di ordinamento è ottimizzato come un ranker contrastivo. I risultati sperimentali dimostrano che questo meccanismo di riordinamento migliora significativamente la classificazione degli invarianti corretti tra i candidati generati, portando a una riduzione notevole del numero di chiamate a un verificatore.

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.