Ranking LLM-Generated Loop Invariants for Program Verification
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910328203247616 |
|---|---|
| author | Chakraborty, Saikat Lahiri, Shuvendu K. Fakhoury, Sarah Musuvathi, Madanlal Lal, Akash Rastogi, Aseem Senthilnathan, Aditya Sharma, Rahul Swamy, Nikhil |
| author_facet | Chakraborty, Saikat Lahiri, Shuvendu K. Fakhoury, Sarah Musuvathi, Madanlal Lal, Akash Rastogi, Aseem Senthilnathan, Aditya Sharma, Rahul Swamy, Nikhil |
| contents | 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. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_09342 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Ranking LLM-Generated Loop Invariants for Program Verification Chakraborty, Saikat Lahiri, Shuvendu K. Fakhoury, Sarah Musuvathi, Madanlal Lal, Akash Rastogi, Aseem Senthilnathan, Aditya Sharma, Rahul Swamy, Nikhil Programming Languages Artificial Intelligence Computation and Language Software Engineering 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. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}. |
| title | Ranking LLM-Generated Loop Invariants for Program Verification |
| topic | Programming Languages Artificial Intelligence Computation and Language Software Engineering |
| url | https://arxiv.org/abs/2310.09342 |