Classement des invariants de boucle générés par des modèles de langage pour la vérification de programmes
Ranking LLM-Generated Loop Invariants for Program Verification
October 13, 2023
Auteurs: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy
cs.AI
Résumé
La synthèse d'invariants de boucle inductifs est fondamentale pour l'automatisation de la vérification de programmes. Dans ce travail, nous observons que les modèles de langage de grande taille (tels que gpt-3.5 ou gpt-4) sont capables de synthétiser des invariants de boucle pour une classe de programmes dans un contexte zéro-shot, mais nécessitent plusieurs échantillons pour générer les invariants corrects. Cela peut entraîner un grand nombre d'appels à un vérificateur de programmes pour établir un invariant. Pour résoudre ce problème, nous proposons une approche de {\it reclassement} pour les résultats générés par les modèles de langage de grande taille. Nous avons conçu un classificateur capable de distinguer les invariants inductifs corrects des tentatives incorrectes en se basant sur la définition du problème. Le classificateur est optimisé en tant que classificateur contrastif. Les résultats expérimentaux démontrent que ce mécanisme de reclassement améliore significativement le classement des invariants corrects parmi les candidats générés, conduisant à une réduction notable du nombre d'appels à un vérificateur.
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.