title: Ranking LLM-Generated Loop Invariants for Program Verification
summary: 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.
paper_authors._id: 652de4f884595aeba19e3475
paper_authors.name: Saikat Chakraborty
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2023-10-17T08:08:37.691Z
paper_authors._id: 61eb45548ae3ccab3b3da983
paper_authors.avatarUrl: /avatars/168a758c4b856b6cdb3c65dd772a549f.svg
paper_authors.fullname: Saikat Chakraborty
paper_authors.type: user
paper_authors.user: saikatc
paper_authors._id: 652de4f884595aeba19e3476
paper_authors.name: Shuvendu K. Lahiri
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2023-10-17T15:11:46.294Z
paper_authors._id: 652e4f747f4b8bd6774c627f
paper_authors.avatarUrl: /avatars/fba113932a392da63d58151c66adc42d.svg
paper_authors.fullname: Shuvendu K. Lahiri
paper_authors.type: user
paper_authors.user: Shuvendu-lahiri
paper_authors._id: 652de4f884595aeba19e3477
paper_authors.name: Sarah Fakhoury
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2023-11-06T10:57:27.555Z
paper_authors._id: 65486006b8ac1a89ff27544a
paper_authors.avatarUrl: /avatars/6d3817537b36cfd33afb9d9bba4265ef.svg
paper_authors.fullname: Sarah Fakhoury
paper_authors.type: user
paper_authors.user: sfakhoury
paper_authors._id: 652de4f884595aeba19e3478
paper_authors.name: Madanlal Musuvathi
paper_authors._id: 652de4f884595aeba19e3479
paper_authors.name: Akash Lal
paper_authors._id: 652de4f884595aeba19e347a
paper_authors.name: Aseem Rastogi
paper_authors._id: 652de4f884595aeba19e347b
paper_authors.name: Aditya Senthilnathan
paper_authors._id: 652de4f884595aeba19e347c
paper_authors.name: Rahul Sharma
paper_authors._id: 652de4f884595aeba19e347d
paper_authors.name: Nikhil Swamy
paper_title: Ranking LLM-Generated Loop Invariants for Program Verification
paper_summary: 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.
paper_ai_summary: A re-ranking approach using a contrastive ranker improves the accuracy of synthesized loop invariants from LLMs, reducing the need for program verifier calls.
paper_ai_keywords: Large Language Models (LLMs) synthesize inductive loop invariants re-ranking contrastive ranker