Ranking LLM -Generated Loop Invariants for Program Verification (2023)

Abstract: 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 a calls to a program verifier to establish an invariant. To address this issue, we propose a 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.

## introduction program verification is a crucial step toward building trustworthy software. unfortunately, the problem of verifying properties of programs containing loops is undecidable. verifying properties of programs containing loops boils down to inferring loop invariants, which are facts that hold for any iteration of the loop, and also ensure the desired property. there is a rich body of prior work on synthesizing loop invariants for program verification through symbolic techniques @xcite @xcite , and their use in verifying safety properties of real-world programs @xcite @xcite . more recently, there is a growing interest in the application of machine learning towards invariant synthesis @xcite @xcite . in recent years, large language models (llms) @xcite have emerged as foundational ai models that have revolutionized language processing applications. though llms were originally proposed for natural languages, they have exhibited great success in formal languages such as programming languages @xcite . in fact, with the increased size, models have started to exhibit emergent properties. for example, modern llms such as gpt-3.5 @xcite , gpt-4 (openai, 2023), palm @xcite are capable of reasoning about a given task with few-shot @xcite , or even zero-shot prompting @xcite . such an impressive footprint of llm naturally raises the question: how well can llms automatically synthesize inductive loop invariants? to this end, we employ two different state-of-theart llms for synthesizing loop invariants. we observe that these models can generate well-formed invariants, but finding the correct one often requires a large number of samples. a solution based on guess and check, with the aid of an automated program verifier based on z3 @xcite , can be computationally very expensive due to several invocations on incorrect invariants. to minimize such costs, we propose reranking the generated invariants based on their likelihood of successful verification. inspired by the use of contrastive learning in information retrieval @xcite , our approach, called irank, transforms the problem and invariants to bring the correct solution closer in vector space while pushing away incorrect ones. empirical results show that such re-ranking moves the median rank of the verified invariant to 4 in contrast to the expected median rank of 31 for the generations from gpt-3.5. in summary, in this paper, we propose to rerank the llm-generated loop invariants to reduce the cost of wasted verification effort. we have designed a ranker to contrast correct and incorrect invariants and show a significant reduction in the 1 9164 invariant checking effort compared to raw llm generations. ## related work prior works on loop invariant generation can be broadly grouped into symbolic or machine learning based. symbolic approaches either construct invariants that are correct by construction @xcite , or leverage satisfiability-modulo-theories (smt) solvers such as z3 @xcite to enumerate and check candidate invariants over a space of pre-defined predicates @xcite @xcite @xcite or predicates constructed through variants of craig's interpolants @xcite @xcite . on the other hand, recent techniques leverage machine learning to synthesize candidate invariants that are checked for correctness using an smt-based program verifier. techniques range from incorporating the feedback from a verifier using active learning over decision trees @xcite , learning from counter examples @xcite , reinforcement learning over graph neural networks @xcite and the use of continuous logic networks @xcite . unlike these techniques, our approach leverages an llm for generation and ranks using a purely neural model and does not require a program verifier at the inference time. this is important for scenarios where the verifier is semiautomated, as is the case of most real-world program verification tools such as dafny @xcite and f* @xcite . finally, @xcite predict program invariants using llms, but they do not aim at generating inductive invariants that are sufficient for formal program verification. ## irank: methodology the main intuition behind irank is learning to pull the likely correct invariants to the front of a ranked list. figure 1 shows a high-level overview of the ranker. we rely on a dataset, @xmath0, i + , i -)}, containing loop invariant generation problem, p, a set of verified loop invariants, i + = {i + | i + ⊢ p}, and a set of wrong loop invariant, i -= {i -| i -⊬ p} for each of the problems, to build irank. our goal is to learn a function between a problem definition p and invariant i, i.e., σ(p, i), which should satisfy the following constraint contrastive ranking. to learn σ, we first ex-tract the embedding of problem definitions and the invariants with an embedder, φ, i.e., @xmath1, and @xmath2, where x and y are the embeddings of problem definition p, and invariant i, respectively. we learn a transformation function, ψ(x|θ), which applies non-linear transformation on input vector x with learnable parameter θ. we then transform problem embedding x to x ′ = ψ(x|θ), and transform invariant embedding y to y ′ = ψ(y|θ). now our target is to maximize the similarity between x ′ and y ′ , when y ′ corresponds to a correct invariant, minimize the similarity otherwise. we use the absolute cosine similarity as the measurement. use of such allows us to set the maximum similarity to 1 (in the case of correct invariant) and the minimum to 0 (in the case of wrong invariant). we optimize the mean squared error loss to learn the parameters in ψ. we experimented with two different embedding models based on llms, i.e.,text-embedding-ada-002 and davinci-similarity. appendix a presents further details of irank's working procedure. ## conclusion we presented a novel approach, irank, to rank the loop invariants generated by llms based on their likelihood of being correct. our ranker leverages a contrastive learning technique to discriminate between correct and incorrect invariants. our evaluation demonstrates that our approach significantly reduces the invariant checking effort compared to the original llm outputs.