Rangschikking van door LLM gegenereerde lusinvarianten voor programmaverificatie

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

Samenvatting

Het synthetiseren van inductieve lusinvarianten is fundamenteel voor het automatiseren van programmaverificatie. In dit werk observeren we dat Large Language Models (zoals gpt-3.5 of gpt-4) in staat zijn om lusinvarianten te synthetiseren voor een klasse van programma's in een 0-shot setting, maar wel meerdere samples nodig hebben om de correcte invarianten te genereren. Dit kan leiden tot een groot aantal aanroepen van een programmaverificateur om een invariant vast te stellen. Om dit probleem aan te pakken, stellen we een {\it herrangschikkings}-benadering voor voor de gegenereerde resultaten van LLMs. We hebben een rangschikker ontworpen die onderscheid kan maken tussen correcte inductieve invarianten en incorrecte pogingen op basis van de probleemdefinitie. De rangschikker is geoptimaliseerd als een contrastieve rangschikker. Experimentele resultaten tonen aan dat dit herrangschikkingsmechanisme de rangschikking van correcte invarianten onder de gegenereerde kandidaten aanzienlijk verbetert, wat leidt tot een opmerkelijke vermindering van het aantal aanroepen naar een verificateur.

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.