Bewertung von LLM-generierten Schleifeninvarianten für die Programmverifikation

Ranking LLM-Generated Loop Invariants for Program Verification

October 13, 2023

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

cs.AI

Zusammenfassung

Die Synthese induktiver Schleifeninvarianten ist grundlegend für die Automatisierung der Programmverifikation. In dieser Arbeit beobachten wir, dass Large Language Models (wie gpt-3.5 oder gpt-4) in der Lage sind, Schleifeninvarianten für eine Klasse von Programmen in einem 0-Shot-Setting zu synthetisieren, jedoch mehrere Proben benötigen, um die korrekten Invarianten zu generieren. Dies kann zu einer großen Anzahl von Aufrufen eines Programmverifizierers führen, um eine Invariante zu etablieren. Um dieses Problem zu lösen, schlagen wir einen {\it Re-Ranking}-Ansatz für die generierten Ergebnisse von LLMs vor. Wir haben einen Ranker entworfen, der korrekte induktive Invarianten von fehlerhaften Versuchen basierend auf der Problemdefinition unterscheiden kann. Der Ranker wird als kontrastiver Ranker optimiert. Experimentelle Ergebnisse zeigen, dass dieser Re-Ranking-Mechanismus die Platzierung korrekter Invarianten unter den generierten Kandidaten signifikant verbessert, was zu einer deutlichen Reduzierung der Anzahl der Aufrufe eines Verifizierers führt.

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.