2023
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu K Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi +3
EMNLP 2023short findings
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…