Classificando Invariantes de Laço Gerados por LLM para Verificação 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
Resumo
A síntese de invariantes indutivos de loop é fundamental para a automação da verificação de programas. Neste trabalho, observamos que os Modelos de Linguagem de Grande Escala (como gpt-3.5 ou gpt-4) são capazes de sintetizar invariantes de loop para uma classe de programas em um cenário de 0-shot, mas exigem várias amostras para gerar os invariantes corretos. Isso pode levar a um grande número de chamadas a um verificador de programas para estabelecer um invariante. Para resolver esse problema, propomos uma abordagem de {\it reordenamento} para os resultados gerados pelos LLMs. Projetamos um ordenador que pode distinguir entre invariantes indutivos corretos e tentativas incorretas com base na definição do problema. O ordenador é otimizado como um ordenador contrastivo. Resultados experimentais demonstram que esse mecanismo de reordenamento melhora significativamente a classificação dos invariantes corretos entre os candidatos gerados, levando a uma redução notável no número de chamadas a um 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.