Ranking LLM-Generated Loop Invariants for Program Verification
Authors: Saikat Chakraborty
Shuvendu K Lahiri
Sarah Fakhoury
Akash Lal
Madanlal Musuvathi
Aseem Rastogi
Aditya Senthilnathan
Rahul Sharma
Nikhil Swamy
Venue: EMNLP 2023 Findings (2023)
Keywords: Large Language Model
Loop Invariant Synthesis
Re-ranking
TL;DR: LLMs do generate verified Loop Invariant, but often after several unsuccessful trials; Re-ranking the LLMs' generation could save the cost of such unsuccessful trials.

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.

Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanial Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy
Microsoft Research
(saikatc, shuvendu, sfakhoury, madanm, akashl, aseemr, tyas, rahsha, nswamy)emiccroooft.. com
Abstract
foundational Al models that have revolutionized Language Processing applications. Though LLMs were originally proposed for natural languages, they have exhibited great success in formal lan- guages such as programming languages (Chen et al., 2021). In fact, with the increased size, mod- els have started to exhibit emergent properties. For example, modern LLMs such as gpt-3.5 (Ouyang et al., 2022), gpt-4 (OpenAI, 2023), PaLM (Chowd- hery al., 2022) are capable of reasoning about a given task with few-shot (Brown et al., 2020), or even zero-shot prompting (Kojima et al., 2022). Such an impressive footprint of LLM naturally raises the question: How well can LLMs automati- cally synthesize inductive loop invariants?
Synthesizing inductive loop invariants fun- damental automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capa- ble of synthesizing loop invariants for a class of programs in a O-shot setting, yet require several samples generate the correct invariants. This can lead to large number of calls to program verifier to establish an invariant. To address this issue, propose re-ranking approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct in- ductive invariants and incorrect attempts based on the problem definition. The ranker is op- timized contrastive ranker. Experimental results demonstrate that this re-ranking mecha- nism significantly improves the ranking of cor- invariants among the generated candidates, leading to notable reduction in the number of calls to verifier.
To this end, we employ two different state-of-the- art LLMs for synthesizing loop invariants. We ob- serve that these models can generate well-formed invariants, but finding the correct one often re- quires a large number of samples. A solution based on guess and check, with the aid of an au- tomated program verifier based on Z3 (De Moura and Bjørner, 2008), 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 re- trieval (Karpukhin et al., 2020), our approach, called iRank, transforms the problem and invariants to bring the correct solution closer in vector space while pushing away incorrect ones. Empirical re- sults 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 g.
1 Introduction
Program verification is a crucial step toward build- ing trustworthy software. Unfortunately, the prob- lem of verifying properties of programs contain- ing 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 syn- thesizing loop invariants for program verification through symbolic techniques (Cousot and Cousot, 1977; Colón et al., 2003; Graf and Saïdi, 1997: McMillan, 2003), and their use in verifying safety properties of real-world programs (Ball et al., 2001; Blanchet et al., 2003; Lahiri et al., 2009). More re- cently, there is growing interest in the application of machine learning towards invariant synthesis (Garg et al., 2016; Padhi al., 2016; Yao al., 2020; Si et al., 2018).
In summary, in this paper, we propose rerank the LLM-generated loop invariants reduce the cost of wasted verification effort. We have de- signed a ranker to contrast correct and incorrect invariants and show a significant reduction the
In recent years, Large Language Models (LLMs) (Radford et al., 2018) have emerged as

---

invariant checking effort compared raw LLM generations.
5
skip 8: | b then S ebe
true false a a a |
<bbbbb
2 Related Work
In its simplest form, the goal of program verifica- tion is to verify that program fragment satisfies its specifications denoted by the Hoare-triple (Hoare, 1969) {pre) while do S {post). Given a pro- gram p and a pair of Boolean expressions (denoted by in the grammar) Φ and y/ denoting the precon- dition and postcondition of a program the Hoare- triple {ø} p { denotes that every terminating execution of that starts in an pre-state satisfying the predicate & ends up in a post-state that satisfies the predicate vh. Since loops can execute an un- bounded number of iterations, verifying programs with a loop requires loop invariant that satisfies the following conditions:
Prior works on loop invariant generation can be broadly grouped into symbolic or machine learn- ing based. Symbolic approaches either construct invariants that are correct by construction (Cousot and Cousot, 1977; Colón et al., 2003), or leverage Satisfiability-Modoe -ocuruo-T--ooscccs (SMT) solvers such as Z3 (De Moura and Bjørner, 2008) to enumer- ate and check candidate invariants over a space of pre-defined predicates (Flanagan and Leino, 2001: Flanagan and Qadeer, 2002; Lahiri and Bryant, 2007: Gulwani et al., 2009; Fedyukovich and Bodík, 2018) or predicates constructed through variants of Craig 's interpolants (McMillan, 2003; Henzinger et al., 2004; Dillig et al., 2013). On the other hand, recent techniques leverage machine learning to synthesize candidate invariants that are checked for correctness using an SM'--based pro- gram verifier. Techniques range from incorporating the feedback from verifier using active learning over decision trees (Garg al., 2016), learning from counter examples (Sharma and Aiken, 2016; Padhi et al., 2016), reinforcement learning over graph neural networks (Si et al., 2018) and the use of continuous logic networks (Yao et al., 2020; Ryan et al., 2020). Unlike these techniques, our ap- proach 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 semi- automated, as is the case most real-world pro- gram verification tools such as Dafny (Leino, 2010) and F* (Swamy et al., 2011). Finally, Pei et al. (2023) predict program invariants using LLMs, but they do not aim at generating inductive invariants that are sufficient for formal program verification.
(pre) skip {4)
(A
(I)
(KA -b] skip [port)
The conditions respectively denote that the loop invariant i holds on loop-entry, is preserved by an arbitrary iteration of the loop and implies the post condition on exit. The problem of loop invariant inference is to infer an that satisfies the three checks above, and denoted i + p.
Furthermore, for the loop-free statements $ in the grammar above, checking the Hoare-triple { S {Ø} can reduced to (decidable) logi- cal formulas in the Satisfiabiltyy-Moduuo--hho (SMT) using standard techniques in program ver- ification (Leino, 2010). One can use a predicate transformer called weakest precondition WP to con- vert the Hoare-triple to decidable SMT formula that can be checked by Z3.
WP(S, +)
{+) 8 (d)
The WP is defined inductively on the structure of statements follows:
WP(x == +)
d(a/4)
WP(skip.or
3 Background & Motivation
WP(Si: Sa.
WP(S., WP(
WP(.S o1)
WP(If 6s then St else Sa. R)
3.1 Background: Loop Invariant Inference
WP(52. o1)
3.2 Motivation and Problem Formulations
In this section. recall the problem of loop in- variant generation in program verification. First, let us define grammar for program statements S. integral expressions and Boolean expressions operating on scalar variables. Most statements and expressions are self-explanatory.
Given problem definition p that consists of pre- conditions pre, loop while do S, and postcon- ditions post, we can query LLMs to generate an invariant that satisfies the conditions specified in Equation (1). Although we have observed that
2

---

Minnng Inwerim
Anotone coomple from tnasting
Enbecdry
Transfored Enberdrr (und fortingg conting
Frebion
Trity Eneudding (preblen definiio))
Decreoss Distercs
Medel
Verified Ttvorion
Tritil Eebedding (corrct mnriaan)
Trastforatton
(3 layer fully conneched Whib))
iRank during Training
Inartant SpREs, Confirenfon
Sitilaity (Dot Products)
(arobler erbh and condisate tne anb)
Enbxadinng
Corddere
Conditon Envandnts
Intid Embeddingg
Transformed Embeddings
iRank during Ranking
Figure I: LLM for Loop Invariant synthesis.
LLMs are capable of producing loop invariants without syntax errors, they often require numerous samples before generating a correct invariant (we refer to Appendix for a details). This results in- efficient resource utilization during the verification process, particularly when dealing with complex problem instances. More importantly, for a more practical scenario where generated invariants are used as part of an interactive verification system such as Dafny//F*, an incorrect invariant would take up valuable user time to perform a manual failed verification effort. Consequently, we propose the utilization of iRank to prioritize the generated in- variants based on their likelihood of being correct, Figure provides a high-level overview of the en- visioned invariant generation-ranking system.
tract the embedding of problem definitions and the invariants with an embedder, b, i.e., x <p)). and y = =(i), where and y are the embeddings of problem definition p. and invariant i, respec- tively. We learn a transformation function, (x/0),, which applies non-linear transformation on input vector x with learnable parameter B. We then trans- form problem embedding to x' (x] and transform invariant embedding y y' (y)()). Now our target is maximize the similarity be- tween x' and y/ when y' corresponds a cor- rect invariant, minimize the similarity otherwise. We use the absolute cosine similarity as the mea- surement. Use of such allows us to set the max- imum similarity to I (in the case of correct in- variant) and the minimum to O (in the case of wrong invariant), We optimize the mean squared error loss to learn the parameters in v. We ex- perimented with two different embedding models based on LLMs, text tebbeddddn ada and davinci-similarity Appendix A presents further details of iRank's working procedure.
4 iRank: Methodology
The main intuition behind iRank is learning pull the likely correct invariants the front of a ranked list. Figure 1 shows a high-level overview of the ranker. We rely on a dataset, containing Loop Invariant generation problem, p, a set of verified loop invariants, _ = {i+ it | p}. and a set of wrong loop invariant, -- (i- i- K p} for each of the problems, to
{pp, [-)}
Experimental Design and Results
5.1 Experimental Setup
Benchmarks. We use Loop Invariant Synthesis benchmarks assimilated by Padhi et al. (2016) constituting set 940 challenge problems in Sy-
build iRank. Our goal is to learn function be- tween a problem definition p and invariant i, i.e.,
(p, i). which should satisfy the following con-
straint ( (o(p, i+) > (p,
https:: http:/ggghuuu..coossssttaaaaaeee http//aawwataaahhhlooooonneee hete/maatter/eencaarss
Contrastive Ranking, To learn σ, we first ex-
3

---

Gus (Alur al.. 2013) format, with a SMT for- mula for the pre-condition, post-condition, and the transfer-function for the loop. We chose a SMT representation for our problem description p to be agnostic to different encoding of C programs into logic. Among these problems, 541 were in the scope of LLM due the context window size. We set the maximum context size as 4096 (with 3584 for prompt, 512 for generation).
ranks
Vek (%)
Experiment
Mean
Median
K-1
K=5
k=10
LLM-ranks
189,78
62.00
5.2
11.6
18.4
Expected ranks
95.35
31.02
8.0
19.2
25.2
TF-DF
103.45
24.00
17.6
32.0
38.8
Ada
115.89
31.50
11.2
21.6
30.0
Emh.
Davinci
120.02
Ada
38.78
5.00
28.0
51.2
60.8
Davinci
34.48
4.00
29.2
52.8
62.8
(a) Invariants generated by gpt turbo.
Gathering L.LM-generated Invariants. We con- ducted experiments involving two distinct language models: gpt-3.5 5-turbo and gpt-4. Our objec- tive was to assess the capabilities of these language models out-of-the-box, and thus employed zero-shot prompting approach. This involved pro- viding problem description and an appropriate task explanation as a prompt (refer to Appendix C for an example). For each problem, we allowed both the models to generate invariants for maxi- mum duration of 10 minutes until verified in- variant was found, whichever occurred first, result- ing in solving 250 problems by 3.tt-3.5-uurb. and 188 problems for gpt-42, It is important to clarify that the purpose of this paper not to con- duct a comparative analysis of these language mod- els in relation to this specific problem. Instead, our objective is to propose a method to orthogo- nally augment LLM capabilities by reranking LLM generated invariants.
Experiment
i ranks
Mean
Median
K=1
K=5
k=10
LLM ranks
39.20
9.00
17.6
40.4
51.6
Expected ranlss
20.23
4.96
31.9
52,1
65.4
TF IDF
24.16
3.00
32,00
45.6
53.6
20.60
51.1
Emb.
Davinci
23,56
5.00
21.7
52.1
63.3
iRank
Ada
13.18
2,00
44.7
74.4
81.4
Davinci
(b) Invariants generated gpt-4.
Table Comparison between different ranking strategies for re-ranking the invariants generated by different LLMs.
Baselines. (a) LLM-ranks. We take the invariants, in the order generated by the LLMs, ranklist. (b) Expected-ranks. We estimate the expected val- ues of the evaluated metrics in this paper by ran- domly permuting the LLM- -egerrted list of invari- ants (see Appendix D for more details). (c) Em- beddings. We use the raw embeddings from LLM- based embedding models to calculate similarity without training. (d) TF-IDF, We use the textual similarity between the problem description and the candidate invariants for ranking.
Training Data. We create the training dataset for iRank (D = (p, /+ )} by combining invari- ants generated from different sources, such as dif- ferent generations from LLMs, and invariants gen- erated by LoopInvGen (Padhi et al., 2017). We divided the problems into five folds and trained 5 different rankers, one for each fold. During the evaluation, we select and load the trained model based on the problem under evaluation. Detailed statistics of data is available in Appendix A.3.
Research Questions. In this paper, we studied two research questions. (i) How effective are LLM- based embeddings for ranking invariants? and (ii) Can trained iRank help reduce the verification cost?
5.2 Results
Evaluation Metric. We then sequentially attempt check invariants from ranked list. We evaluate three metrics - (i) it ranks rank of the correct invariant in the list, (ii) V@K the percentage of problems where the verified invariant is found in top K invariants from the re-ranked list, and (iii) Number of Z3 calls the total number of z3 calls before finding and reporting correct invariant, higher number of z3 calls indicate a high waste of computational resources.
Table shows the quantitative evaluation of iRank. If we consider LLM--gnerated list invariants as is, we observe that LLMs are able to generate a ver- ified invariant after a significant number of wasted trials. For example, on average, gpt-3.5-tum found an invariant after ~99 failed attempt at generation. gpt-4 does much better, in compar- ison, with the mean rank of verified invariants be- ing 39.20. The expected rank of the verified in- variant from I...M-geerrations is 95.35 and 20.23, for 3.tt3.5-turbb and gpt-4, respectively. The use of LLLM embeddings (without any train-
NNte that the rate limit for gpt-4 4 was an order lower than gpt-3.5 in our usage resulting in an order less samples.
4

---

of the wort/eo (110/311
Paiebbe of22 -185
1.000
220
100
150
300
200
8
120
100
Park AAb
LAN 331t2
Cart--aandd
Ranks
Expected Runta
TT-DF
Derrre oTth
Eaparenna
Experimatia
Exper mena
Experiment
Rank
# Z3 calls
Rank
calls
(a) 3pt-3.5- 3.--3.--tubb
gpt-4.
Figure Detailed results comparing ranks of the correct invariants number calls.
Ronis
Alo unb
LEM Rolls
enb. Rark-ics
ference between text-embedding-adde ada-2200 and Devinci-similane models, the performance differences are not different with statistical sig- nificance (with p-value > 0.1). In both models' cases, there is no statistically significant difference between the expected rank and embedding- based ranking. Note that, similar to the existing works (Ryan et al., 2020), we use z3 call mea- sure resource wastage. However, depending on the system the experiments are carried on, the time saved from reranking with iRank could be different. We report our experimental results of wall clock time in Appendix B (Table 2).
Speccs Ranks
Ranc-te Ranc Buiis
Eaoecied taika
17. Dr
17:27
Dadiic enis
Purcerage hostere
60
(a) gpt-3. 3-
(b) gpt-4
Figure 3: Percentage of prohlems solved w.r.t. number of
invariants from the (re-)ranked list.
Figure 3 shows the percentage of problems veri- fied after trying invariants (V@K). We observe that the iRank curves are very steep the begin- ning of the curves compared to the baseline, sig- nifying that it could rank the verified invariants in significantly higher positions than baselines.
ing) such from text-embedding- ada-002 or davinci-similan results the mean rank of the verified invariant to be 115.89 and 120.02, respectively for 3pt-3.5-turbo and 20.69 and 23.56, respectively for gpt-4. While such result looks like significant improvement over LLM- ranks, it slightly worse than expected ranks.
Contrastive training in iRank brings the veri- fied invariant closer to the problem while pushing the wrong ones resulting in significant reduc- tion in the verification cost.
/ LLM--bsedd embeddings standalone may not serve well for reranking verified invariants.
The training procedure in iRank significantly contributes improving the ranking of verified invariants by transforming the embeddings. The median rank of the verified invariant 32 when using the embedding from embeddings. With the contrastive training in iRank, the median rank is brought down to 4, showing significant improvement. Such trend persists across different embedding models and generations from different LLMs. Figure 2a, and Figure 2b shows the detailed results invari- ants generated by gpt-3.5-turbo and gpt-4. both trained and raw embeddings, the dif-
Conclusion
sineii-smmllaiii ty
We presented a novel approach, iRank, to rank the loop invariants generated by LLMs based on their likelihood of being correct. Our ranker leverages contrastive learning technique discriminate between correct and incorrect invariants. Our eval- uation demonstrates that our approach significantly reduces the invariant checking effort compared the original LLM outputs.
5

---

Limitations
Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. 2001. Automatic predicate ab- straction of C programs. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation ( (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pages 203-213. ACM.
Assumptions of LLM inference cost. In this paper, we assumed the cost of calling LLMs is neg- ligible compared to the cost of calling the verifier for checking an invariant. Current access to LLMs (at least the one studied in the paper) is avail- able through the rest API, which can be scaled up by the API vendor with distributed processing of LLM. However, with the increase in the problem complexity, i.e., non-linean invariants, high number variables, the check for correctness of an invari- ant become exponentially more expensive. In the case where call to LLM is much more expensive than LLM, iRank will reduce the number of Z3 calls, but may not contribute to actual cost savings.
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A static analyzer for large safety-critice software. Proceedings of the ACM SIGPLAN 2003 Conference on Program- ming Language Design and Implementation, PL,DI '03, page 196-207, New York, NY, USA. Association for Computing Machinery.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam. Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. Advances in neural information processing systems, 33:1877-1901.
Comparison with state-of-the-ar (SOTA) invari- ant synthesis. The goal of this paper is not to establish SOTA for loop invariant synthesis. In con- trast, we investigate LLMs' capacity generate Loop invariant relying on their emergent behav- ior. iRank is proposed as an orthogonal tool and evaluated to rank LLM generations in this paper. However, in theory, iRank should be able to rerank invariants generated by any generator. Neverthe- less, the design of the SOTA technique of Loop Invariant Synthesis with LLM (perhaps with other tools) remain open problem, which we leave for future research.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto. Jared Ka- plan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. 2021. Evaluating large language models trained code. arXiv preprint wrXiv:2107.03374
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung. Charles Sutton, Sebastian Gehrmann, et al. 2022. Palm: Scaling language modeling with pathways. arXiv preprint arXiv:2204.023711
Michael A. Colón, Sriram Sankaranarayanan, and Henny B. Sipma. 2003. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification, pages 420-432, Berlin, Heidel- berg. Springer Berlin Heidelberg.
Stability of LLM predictions. Due to the stochastic (and nondeterministic 9) nature of the LLM, especially in higher temp, we observe un- stable generation from the LLM. Nevertheless, we evaluated the results from one sample run from gpt-3. 3.t-3..-turb and one from gpt-4 as case stud- ies. While we acknowledge the possibility of un- stable behavior, similarity in the performance trend (ie.. iRank's 's performance improvement over LLM and expected ranks, also over embeddings) give us confidence about the impact of iRank.
Patrick Cousot and Radhia Cousot. 1977. Abstract inter- pretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT- SIGPLAN Symposium on Principles of Programming Languages, POPL '77, page 238-252, New York, NY, USA. Association for Computing Machinery.
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3:
An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems: 14th ternational Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hun- gary March 29-April 6, 2008. Proceedings 14, pages 337-340. Springer.
References
Rajeev Alur, Rastislay Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh. Armando Solar-Lezama, Emina Tor- lak, and Abhishek Udupa. 2013. Syntax-guided syn- thesis. IEEF
Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMil- lan. 2013. Inductive invariant generation via abduc- tive inference. Acm Sigplan Notices, 48(10)443- 456.
'https: //tlat/olllaooom openai. http://csss/ddd///deeeeeeeeeeeee why-are-mont model- wwtpots--iineetee inconsistent
6

---

Grigory Fedyukovich and Rastislav Bodík. 2018. Accel- erating syntax-guided invariant synthesis. In Tools and Algorithms for the Construction and Analysis of Systems, pages 251-269, Cham. Springer Interna- tional Publishing.
Shuvendu K. Lahiri, Shaz Qadeer. Juan P. Galeotti, Jan W. Voung, and Thomas Wies. 2009. Intra-module inference. In Computer Aided Verification, 21 Inter- national Conference, CAV 2009, Grenoble, France, June 26- July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 493-508. Springer.
Cormac Flanagan and K. Rustan M. Leino. 2001. Hou- dini, annotation assistant for esc/java. In FME 2001: Formal Methods for Increasing Software Pro- ductivity, International Symposium of Formal Meth- ods Europe, Berlin, Germany, March 12-16, 2001, Proceedings, volume 2021 of Lecture Notes in Com- puter Science, pages 500-517. Springer.
K Rustan M Leino. 2010. Dafny: An automatic pro- gram verifier for functional correctness. Logic for Programming. Artificial Intelligence, and Reason- ing: 16th International Conference, I.PAR-16, Dakar, Senegal, April 25- 2010, Revised Selected Papers 16, pages 348-31283 148-370. Springer.
Cormac Flanagan and Shaz Qadeer. 2002. Predicate abstraction for software verification. SIGPLAN Not., 17(1):191-202.
Shang- Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, and Henri Hansen. 2017. Fib: Squeez- ing loop invariants by interpolation between for- ward/backward predicate transformers. 2017 32nd JEEF/ACM International Conference on Automated Software Engineering (AST)), pages 793-803. IEEE.
Pranav Garg. Daniel Neider, P. Madhusudan, and Dan Roth. 2016. Learning invariants using decision trees and implication counterexamples. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Sym- posium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20- 22, 2016, pages 499-512 ACM.
Kenneth L. McMillan. 2003. Interpolation and sat- based model checking. In Computer Aided Verifi- cation, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 1-13. Springer.
Susanne Graf and Hassen Saidi. 1997. Construction of abstract state graphs with PVS. In Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25. 1997, Proceedings, volume 1254 of Lecture Notes in Computer Science, pages 72-83. Springer.
OpenAL 2023. Gpt-4 technical report.
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. 2022. Training language models to follow instruc- tions with human feedback. Advances in Neural Information Processing Systems, 35:27730-27744.
Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. 2009. Constraint-based invariant in- ference over predicate abstraction. In Verification, Model Checking, and Abstract Interpretation, pages 120-135, Berlin, Heidelberg. Springer Berlin Heidel- berg.
Saswat Padhi, Rahul Sharma, and Todd Millstein. 2017. Loopinvgen: loop invariant generator based on precondition inference. arXiv preprint 170.:0277.
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16. 2004, pages 232 22-244..44 ACM.
Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-driven precondition inference with learned features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Bar- bara, CA, USA, June 13-17, 2016, pages 42-56.
Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-58)
Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023. Can large language mod- els reason about program invariants?
Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. 2020. Dense passage retrieval for open-domain question answering. arXiv preprint arXiv:2004.04906
Alec Radford, Karthik Narasimhan, Tim Salimans, llya Sutskever, et al. 2018. Improving language under- standing by generative pre-training.
Gabriel Ryan, Justin Wong. Jianan Yao, Ronghui Gu, and Suman Jana. 2020. Cln2inv: Learning loop in- variants with continuous logic networks. In Interna- tional Conference on Learning Representations.
Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yu- taka Matsuo, and Yusuke Iwasawa. 2022. Large lan- guage models are zero-shot reasoners. arXiv preprint 1rXiv:2205.11916.
Rahul Sharma and Alex Aiken, 2016. From invariant checking to invariant inference using randomized search. Formal Methods in System Design, 48:235- 256.
Shuvendu K. Lahiri and Randal E. Bryant, 2007. Predi- cate abstraction with indexed predicates, ACM Trans. Comput. Logic, 91):4-es.
7

---

Experiment
Mean
i
ranks
Median
K-1
vēk (%)
K-5
lc-10
Eimbed
Ranking
Timels) (Mean/Median)
Veriflication
Total
LLM-ranks
189.78
62.00
5.2
11.6
184
0/0
0/0
7.33
7.35/2.25
Expected ranks
95.35
31.02
8.0
19.2
25.2
0/0
0/0
1.12/1122
3.67 /.12
TF-IF
103:45
24.00
17.6
32.0
38.8
0/0
0.05
/0.02
3,83
3.88 /
Ada
21.6
30.0
1.29/0.42
0.05
4,43/1.22
Emih
Davinci
120.02
32.00
10.4
20.8
33.6
9.17 /.02
0.45/0.15
4.79/ 1,20
14.41 /4.4
iRook
Davinci
Ada
38.77 78
34,48
5,00
4.00
29.2
28.0
51.2
52.8
60.8
62.8
1.29 0042
9.17/3.02
0.06/0.02
0.48/0.15
1.64/0.19
1.28
10.93 3.68
2.98
(a) Invariants generated by gpt-3. 10tt-3.5 3.5 S-turbo...
Experiment
ranks
Time(s) (Menn/Median)
Mean
Median
K=1
K=5
k=10
Eanbed
Ranking
Verilication
Total
LLM-ranks
39.20
9.00
17.6
40.4
51.6
070
0/0
1.61/0.2
1.61 00.24
Expocted ranks
20.23
4,96
31.9
52.1
63.4
0/0
0/0
0.83/0.19
0.83/
THIDF
24.16
3.00
52,00
45.6
53.6
0/0
0.1
70,006
0.80/0.11
0.81 /0.12
Emb.
Ada
20.69
5,50
26.6
51.1
64.9
0.23/
0.1 70.004
/017
0.26
1.3
0.75/0.16
Ada
13.18
2,00
44.7
74.4
81.4
0.25 0.006
0.02 /0.004
0.44/0.06
0.71 0.16
Davinci
11.96
2.00
44.7
71.8
81.9
1.93 0.48
0..03
0.74/0.06
2.80
(b) Invariants generated by gpt-4.
Table 2: Comparison between different ranking strategies for re-ranking the invariants generated by different LLMs.
Xujie Si, Hanjun Dai. Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning loop invariants for program verification. Advances Neural Infor- mation Processing Systems, 31.
Experiment
i ranks
V@K (%)
Mean
Median
K=1
K=5
k-10
Original
95.35
31,02
8.0
19.2
25.2
Expocted ranks
Deduplicated
65.24
24.07
8.4
22.8
31.2
Original
38.78
5.00
28.0
51.2
60.8
iRank-ada
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre- Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value- dependent types. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 11,, page 266-278, New York, NY, USA. Association for Computing Machinery.
Deduplicated
18.79
4.00
28.4
56.0
65.6
(a) Invariants generated by gpt- 3.t-3.55 turbo
i" ranks
V@K (%)
Experiment
Mean
Median
K=5
k=10
Expocted ranks
Original
20.23
4.96
31.9
52.1
65.4
Deduplicated
13.99
4.89
31.4
53.7
72.8
Original
13.18
2,00
44.7
74.4
81.4
iRank-uda
Deduplicated
8.73
2,00
46.8
77.1
86.7
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop in- variants with gated continuous logic networks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementa- tion, pages 106-120.
(b) Invariants generated by gpt-4-turis turbo
Table 3: Ranking result of correct invariant by de-duplicating semantic equivalent candidates
davinci-similate to acquire initial embed- dings for both the problems and candidate solutions. These initial embeddings undergo transformation via a three-layered fully connected feedforward network to yield transformed embeddings. The training objective is twofold: minimize the dis- tance between the transformed embedding of the problem and the corresponding correct solutions, while maximizing the distance from incorrect ones. Once this model is trained, it is employed to rank the candidate invariants generated by the LLM any other generator.
A Further Details of iRank
In this section, present comprehensive overview of the operational workflow of iRank, as visualized in Figure 1.
A.1 Training iRank
As elucidated in Section 4, the training of iRank necessitates a dataset containing invariant synthesis problems, akin to those illustrated in Figure 4. Each problem in the training dataset requires at least one of incorrect invariants,
correct invariant and all expressed in the SyGus format (refer Figure for an example). We employ the specified embed- ding model, namely text text-eembed ad2-002 or
A.2 Ranking with iRank
Upon successful training of the transformation network within iRank, it is used for ranking pur-
8

---

Problem Statistics
Number of Layers
Total Problems
5-1
Hidden
1536 (tootetterbbediing ada-2ez)
12288 (davinci wwwiincciiinnnerrre
Problem Types Statisties
Optimizer
Adam
Integer
(91,88%)
Training Epochs
Noa-Lingar Inieger (NIA)
27 (4, 9999)
Arra Linear Integer (AL
(3.33%)
Weight
0.001
Problem Semantics Statistics
Max Gradient Norm
1.0
Number of functions
3,
Learning Rate
+ 10
Number of Variables
Min 2, Max
Scheduler Type
Lincur
Integer 80.31
Warmup Steps
500
Variable types
Boolean 19.31%
Table 5: Hyperparameter for Model and Training
Arry|Integerr = 0.36%
Amay|Banlean = 0.03%
Operator Statistics (of the correct invariants)
Conjactions
(of all operators) 1.12 (avg. per example)
used in this study.
Disjuncrions
20% (of all operators)
0.53 (avg. per example)
B Detailed Results
Negations
57% (of all operators)
0.96 (avg. per example)
SubiiionSSuraaicon
43% (of all operators)
In addition to comparing the number of Z3 calls, we compared the wall clock time. Table 2 shows comparison of time (as an extension of Table 1), We conducted all the experiments in 24 cores AMD Epyc 7V13 Linux server running Linux Ubuntu 20.04 LTS with 220 GB RAM, and a sin- gle NVIDIA A A100-PCIE-80GE GPU, For LLM- Ranks, Expected ranks there no embedding and ranking, thus the verification time is the bottleneck. For TF-ID, while there is no embedding time, the is little bit of ranking time.
0.5 (avg. per example)
Multiplication/Dinn
3.1% (of operators)
0.18 (avg. per example)
38.5% (of all operatoes)
Logical Comparison
5.25 (avg. per example
Length Statistics
88 (T)
Problem Length
Mox = 2752 (N), 3146 (T)
Mean 740 (N), 922
Mia = 18 (N), (T)
Invariani Length (gpt-3.5-turbo)
(N), 506
Mean = 110 125 (T)
Mia (N), 15 (T)
Invariant I ength (gme-4)
Mox 513 (N), 488 (T)
Mean
102
The Ada embedding time in iRank was very small compared to the Davinci embedding, thus, in the case of iRank-ada, embedding and ranking time was offset by the time iRank reduced in the verification effort. In contrast, the Davinci embed- ding in iRank is more expensive than the reduc- tion in the verification time, resulting in a worse wall clock time performance than the LLM ranks. We conjecture that the text--mbbedding-adde ada-002 (embedding dim = 1536) is a smaller model com- pared to seviini-ssime larity (embedding dim = 12188), thus requiring significantly longer time to embed an input sequence (problem description invariant).
Tokenized with NLTK = Tokenized with TiKToken
Table 4: Stattistics of the experimental data
poses. To rank the candidate invariants, iRank initially extracts the initial embedding of the problem and list of solutions, using the same embedding model davinci-similare
or employed during train- ing. The trained transformation network is then used transform these embeddings. These trans- formed embeddings serve as vectors for the re- ranking process, where iRank calculates the cosine similarity between the transformed embedding of the problem and each of the candidate solutions. The candidate solutions are then sorted and re- turned based on their similarity with the problem.
It is important to note here that, this experiment is only meant for an illustration of potential threats to iRank, and dependent on lot of variables, including, but not limited to OpenAl subscription maximum rate limit, network latency for initial embeddings, etc.
A.3
Data Details and Training Hyperparameters
In addition, we analyzed the generated invariant candidates from LLMss, and removed any semantic duplicates. Given two invariant candidates ia and i, parameterized by set of variables {vi,-- 2
Table 4 shows the statistics of the data we used to experimentally evaluate iRank. Table shows the hyperparameters for the models and training we
9

---

we define semantic equivalence as,
Synthesize necessary and sufficient Invariant.
Start invariant with "ndefine- fun iny_ fun ((S Int) (n Int) (a Int) (b Int)) Bool (" and end with 1)*.
, On da (.,,..... vn) < (6(0....... vn)
For comparing equivalence of two candidate invari- ants, we make one call to the z3. Such seman- tic deduplication requires comparison of newly generated candidate invariant with all previous can- didates, necessitating (n²)) z3 calls, just to dedu- plicate. Table 3 shows the results deduplicated candidates comparison with the original list of invariants. As expected, after deduplicating, the expected ranks improves. Interestingly, even in the list of candidates where all candidates are se- mantically unique, iRank improves the rank of the correct invariant, resulting in higher V@k.
Surround only the invariant with <code> and </code2. You don't need to explain the Invariant, just synthesize it.
The gpt-3. 3-turbbo model generated invariant shown in Figure after 144 unsuccessful attempts.
(define-fun fun ((1 Int) (n Int) (a Int) Int))
Bool (ar
(and (<= 1 n) (= (+ b) (* 1)))
(> n) (+ (* n)))
Figure Correct invariant generated by got-3, 5-turbo.
Illustrative example
As an illustration of our proposed approach, we present an example from FiB (Lin et al., 2017) benchmark 4 The problem is represented in SyGus format as shown in Figure 4.
The gpt-4 model generated the invariant shown
in Figure after unsuccessful attempts.
(define-fun iny fun ((i Int) (n Int) (a Int) (b Int))
Bool
(<= n) (= a) (* 3)))
(set-logic LTA)
(synth-inv inv_ fun Int) Int) (a Int) Int)))
(define-Fun fue_ ((1 Int) Int) (a Int) Intt) Bool (and
(= (=
(>e 8)
Figure 6: Correct invariant generated by gpt-4.
(deFine-Fun trans_ Fun ((1 Int) (n Int) (a Int) Int)
iRank trained based on text-embedding- at 8th posi-
(i) Int) (n! Int) (a! Int) (b! Int)) Bool (ar
002 repositioned the tion in the list and the gpt-4 generated correct invariant in position 2. Note that we show this example only for illustration purposes.
(and
(c1
100 (- a+a
b1 23) (=
(and
(c1n) (- (1) (- 2)) (I 1)) (+
D Experiment on Expected re-ranking
(and
(> ii (a (1 (+ m)
The list of invariants generated by LLM as ranked list could be unstable and susceptible to variations in performance across different experiments. Thus, as described in Section 5.1, we estimate the ex- pected ranks by randomly permutating the list. Ide- ally, to get perfect estimation, we should consider all possible permutations of the list, which can be very expensive (exponential order on the number of elements in the list). Figure 7 shows ablation of mean rank w.r.f. the number of random permuta- tions. As we can see, with gradual increase in the number of permutations, the variance in the met- rics gradually reduces, i.e., the metrics converges. Throughout the paper, we set the number of permu- tations to be 100 for estimating the expected rank metrics.
(define-fun fust_fun ((1 Int) (n Int) (a Int) (b Intt) Bool (>> (not (c n)) b) (r. (+ n) m))))
(dnv-constraint fun_fun pro_fun trans_fun fun post_fun)
(check-synth)
Figure 4: Invariant synthesis problem in FiB-8.sl
We create the following prompt call LLMs.
Hare: is loop invariant synthesis problem in SyBus fornat.
<<<eThe problen definition from above>>>>>
'https: httpas///ggthuub..mm/eeeeeeee wwtp://c///peceiiiooo/////o 2se2017-results trrresulss-nneee and wttp://ooooooooooee///eeeeeeeeie benchmarks
10

---

132.5
133.
27.5
23.0
87.5
Number Random Permaaaions
(a) 5tt-b.
Newn Bank
19
10
gpt-4
Figure 7: Result stabilization with increasing number of random permutations
E
Visualization of the impact of training iRank
Figure 8 show t-SNE plot of the raw LLM em- beddings and the transformed embeddings for few example problems. For the first three exam- ples(Figures Sa, 8b, 8c, respectively), iRank brings the correct invariant closer to the problem than any other invariants. For the example presented in Fig- ure 8d, iRank could not make the correct invariant as the closest to the problem. While there are cases where iRank's 's transformation fails to bring the cor- rect invariant in the closest proximity, in most cases, it bring correct invariants closer to the trans- formed problem embedding, as corroborated by the results in Appendix B

---

x
x
x
x
x
X
x
W/O training
With training
(a) Example
Problem
Conrect Invarinn
x
Incorrect invoriant
Problem
Correct Invarintt
Incorrect Invorfan:
x
Xx
X
x
x
x
x
X
X
X
x
x
W/O training
With training
(b) Example 2
Problem
Correct Invariant
Incerrect Invvrient
Problem
Correct Inverant
Incernect invwitntt
x
XX
Xx
x00x
%
306
W/O training
With training
(c) Example 3
Problam
Connect Inmariant
Incomeet Invrian:
Problem
Correct Invariant
Incorrect Inseiinn.
X
x
X
*
x
x
x
x
X
x
x
x
x
x
X
X
X
x
X
X
W/O training
With training
(d) Example 4
Figure L-SNE plots of embeddings with and without training for few example problems. The number of incorrect invariants is downsampled for better visualization clarity.
12


Reviews:
[{"review_id": "ehcYZSrbK8", "reviewer": "Reviewer_ZsSr", "summary": "", "questions": "- Are there straight-forward human heuristics to test your approach against?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 4, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for thoughtful and valuable feedback and suggestions. Following the suggestion from the reviewer, we conducted several experiments. Here are the details. \n\n1. **Other baselines**\n\n    - We implemented a trivial similarity-based (TF-IDF) ranker, where the invariant exhibiting higher similarity with the input problem goes to higher ranks. Since the problem definition contains the SMT formula for the `precondition` `transfer-function` and `postcondition`. This experiment tests a hypothesis _an invariant that takes most of its ingredients (i.e., SMT clauses) from the input problem has a higher chance of being successful_. We find that TF_IDF does better than LLM-ranks and even better than the raw embedding from OpenAI embedding models. Nevertheless, iRank performance is still better than all other baselines. For ranking `gpt-3.5-turbo` generated invariant candidates, $V@1$ for TF_IDF is 17.6, which is higher than expected ranks from LLM ($V@1 = 8.8$). However, $V@1$ is $28.0$ and $29.2$, for $iRank-ada$, and for $iRank-davinci$, respectively. For ranking `gpt-4` generated invariant candidates, $V@1$ for TF_IDF is $32.0$, which is higher than expected ranks from LLM ($V@1 = 23.6$). However, $V@1$ is $33.6$  and $33.5$, for $iRank-ada$, and for $iRank-davinci$, respectively.\n    - Further, we experimented on a symbolic heuristic where we retained semantically unique invariants generated by the LLMs. We evaluate whether two invariant $i_1$ and $i_2$ semantic equivalent by evaluating the following SMT formula with z3, $\\forall{v_1, v_2, …, v_n}(i_1(v_1, v_2, …, v_n) \\Leftrightarrow i_2(v_1, v_2, …, v_n))$. We find that GPT3.5 generated $9.29$% semantically duplicate invariants, and GPT-4 generated $4.70$% semantically duplicate invariants. We calculate the expected ranks of such a deduplicated dataset. Below is the result when ranking the invariant candidates generated by `gpt-3.5-turbo`. \n        | Experiment                   | Mean $i^+$ rank|  Median $i^+$ rank | $V@1$ |  $V@5$ |  $V@10$ |\n        |------------------------------|------------------|---------|---------|------|-------|\n        | LLM-Ranks                    | $189.78$           | $62.00$   | $5.2$     | $11.6$ | $18.4$  |\n        | Expected LLM Ranks           | $95.35$            | $31.02$   | $8.0$    | $19.2$ | $25.2$  |\n        | Expected after Deduplication | $65.24$            | $24.07$   | $8.4$     | $22.8$ | $31.2$  |\n        | iRank-ada                    | $38.78$            | $5.00$    | $28.0$    | $51.2$ | $60.8$  |\n        | iRank-davinci                | $34.48$            | $4.00$    | $29.2$    | $52.8$ | $62.8$  |\n        \n        In the case of  invariant candidates generated by `gpt-4`, we find the following results,\n        | Experiment                   | Mean $i^+$ ranks | Median $i^+$ ranks | $V@1$ | $V@5$ | $V@10$ |\n        |------------------------------|------------------|--------------------|-------|-------|--------|\n        | LLM-Ranks                    | $39.20$            | $9.00$               | $17.6$  | $40.4$  | $51.6$   |\n        | Expected LLM Ranks           | $20.23$            | $4.96$               | $31.9$  | $52.1$  | $65.4$   |\n        | Expected after Deduplication | $13.99$            | $4.89$               | $31.4$  | $53.7$  | $72.8 $  |\n        | iRank-ada                    | $13.18$            | $2.00$               | $44.7$  | $74.4$  | $81.4$   |\n        | iRank-davinci                | $11.96$            | $2.00$               | $44.7$  | $71.8$  | $81.9$   |\n\n        For the `gpt-3.5-turbo` generated invariant, the mean and median expected ranks of the correct invariant are $65.24$ and $24.07$, respectively. In contrast, the expected rank in the original generation (without deduplication) were $95.35$ and $31.02$ (mean and median). For the case of `gpt-4`, the mean expected rank reduced from $20.23$ to $13.99$, and the median reduced from $4.96$ to $4.89$. So, we do see some improvements in ranks with semantic heuristics. However, such deduplication is very expensive, since we must compute $n*n$ equivalence check queries to Z3. For our experiment, it took more than $23$ hours just to deduplicate. Given the resource expense, we conjecture that such deduplication-based ranking is not feasible for real-world applications. In addition, we evaluated $iRank$ on this semantically deduplicated candidate invariant set and found that $iRank$  improves the rank of correct invariants, even when semantic duplicates are eliminated - supporting that $iRank$ is not learning any trivial semantic patterns. \n\n2. **Complexity of the problems:** We evaluate iRank on the SyGus benchmark, which includes the loop invariant synthesis problem from several different sources, including different verification challenges. The problems include _Linear Integer Arithmetic_ ($91.68$%, $496$ out of $541$), _Array Linear Integer Arithmetic_ ($3.33$%, $18$ out of $541$) and _Non-linear Integer Arithmetic_ ($4.99$%, $27$ out of $541$) problems. Here are more detailed statistics of the problems in the dataset. \n\n    | Problem Type Statistics         |                |\n    |---------------------------------|----------------|\n    | Linear Integer Arithmetic       | $496$ ($91.68$%) |\n    | Non-Linear Intehger Arithmetic  | $29$ ($4.99$%)   |\n    | Array Linear Integer Arithmetic | $18$ ($3.33$%)   |\n\n    | Problem Semantics Statistics |                          |\n    |------------------------------|--------------------------|\n    | Number of functions          | Min = $3$, Max = $9$     |\n    | Number of variables          | Min = $2$, Max = $90$    |\n    | Variable Types               | Integer = $80.31$%       |\n    |                              | Boolean = $19.31$%       |\n    |                              | Array[Integer] = $0.36$% |\n    |                              | Array[Boolean] = $0.03$% |\n\n    | Operator Statistics (of correct invariants)        | % of all operators | Avg. # per examples |\n    |----------------------------------------------------|--------------------|--------------------------|\n    | Conjuctions                                        | $43$                 | $1.12$                     |\n    | Disjunctions                                       | $20$                 | $0.53 $                    |\n    | Negations                                          | $37$                 | $0.96$                     |\n    | Addition/Subraction                                | $43$                 | $0.5$                      |\n    | Multiplication/Division                            | $3.1$                | $0.18$                     |\n    | Logical Comparison                                 | $88.5$               | $2.25$                     |\n    | Examples with quantifiers ($\\forall$ or $\\exists$) | $7$                  |  \n\n    | Length Statistics           | Min | Max  | Avg |\n    |-----------------------------|-----|------|-----|\n    | Problem Length (NLTK)       | $92$  | $2732$ | $740$ |\n    | Problem Length (TokToken)   | $88$  | $3146$ | $922$ |\n    | Invariant Length (NLTK)     | $18$  | $605$  | $110$ |\n    | Invariant Length (TikToken) | $15$  | $506$  | $125$ |\n\nWe appreciate the valuable review and the feedback. We will incorporate our responses to the feedback to the camera-ready version of the paper.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- Important and aspiring research direction to use LLMs for verification tasks\n- Their approach is a significant contribution, a perfect-size short paper\n- Their dataset is interesting and can be used for interesting future research\n- The experimental results are showing a significant performance compared to not using a ranking", "reasons_to_reject": "- A more interesting baseline is missing, for example, some trivial rankings based on human-created or symbolic heuristics for ranking\n- It is not immediately clear how challenging and interesting the verification problems are from reading the paper", "questions_to_authors": "- Are there straight-forward human heuristics to test your approach against?", "paper_topic_and_main_contributions": "In this submission, the authors consider the generation of loop invariants, which are essential in deductive program verification. They propose a re-ranking for LLM-generated loop variants. Although finding correct loop invariants can be done by guessing and checking, they argue that ranking the generated invariants is important to minimize the computational cost. Their approach called iRank, uses ideas from contrastive ranking: The basic idea (page 3) is to transform the problem embedding x to x′ = Ψ(x|θ), and transform invariant embedding y to y′ = Ψ(y|θ) and then maximize and minimize the similarity between x ′ and y ′ respectively. They create a training dataset and evaluate their ranking methodology, which results in a significant improvement in “V@K” (verified after trying k invariants).\n", "excitement": 4, "reproducibility": 4, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "dkVtUXjCQf", "reviewer": "Reviewer_P8En", "summary": "", "questions": "See weaknesses section above.", "limitations": "", "rating": 3, "confidence": 3, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their insightful comments and suggestions. Here are the answers to the reviewer’s questions. \n\n1. **Contribution of the paper:** The main contributions in the paper are, \n    1. In this paper we studied the feasibility of LLMs such as (`gpt-3.5-turbo`, and `gpt-4`) for generating loop invariants in SMT-2 (SyGus) format in a language independent manner. Our study shows that with simple prompts LLMs are able to generate correct invariant in upto 46% of the cases ($250$ out of $541$ problems). \n    2. Based on our observation that the correct invariant is generated after lots of failed attempt resulting in a lot of wasted calls to the Z3-solver, we propose an invariant ranker (iRank) based on the LLM-based embedding models (i.e., `text-embedding-ada-002`, and `davinci-similarity`) and contrastive learning.  We empirically show that after generating a set of invariants with LLM, if we reranked them using $iRank$, the number of Z3 calls are significantly reduced. \n    3. We create a ranking dataset, containing the invariant synthesis problem, LLM-generate invariant candidates, all the SMT-2 (SyGus) format.\n    4. We open source our dataset, code, and trained model for future research. \nWe will add a subsection at the end of the introduction to summarize these contributions. \n\n2. **Clarification of Figure1b:** Thanks for the suggestion. Here is the figure we will add to the camera-ready version to articulate iRank’s architecture. We have uploaded the redrawn image [in this anonymous link](https://figshare.com/ndownloader/files/42163257/preview/42163257/preview.jpg). \n\n    For the embedding transformation, we use a 3-layered fully connected feedforward ANN. The hidden dimension of the embedding transformation model depends on the initial embedding model. For instance, when we use embeddings from `text-embedding-ada-002` model, the hidden dimension is $1536$. For `davinci-similarity` model, the hidden dimension is $12288$. Also note that, since we are extracting initial embeddings through OpenAI API, the only learnable parameters in $iRank$ are in the Embedding Transformation module. \n3. **Training Details:** Apologies for the confusion. We use two different OpenAI embedding models (`text-embedding-ada-002` and `davinci-similarity`) to extract the initial embeddings for both the problem definition and the invariant candidates using the iRank architecture described above. We optimize iRank to bring the transformed embedding of the problem closer to the correct invariant and further away from the incorrect invariant from the training set. To optimize, we use the `MSELoss` where the expected similarity of the problem and correct invariant is $1$, and with incorrect invariants, it is $0$. Here are the training details. \n    ```json\n    {\n        \"optimizer\": \"Adam\",\n        \"learning_rate\": 5e-05,\n        \"num_train_epochs\": 20, \n        \"weight_decay\": 0.001,\n        \"max_grad_norm\": 1.0,\n        \"lr_scheduler_type\": \"linear\", \n        \"warmup_steps\": 500,\n        ...\n    }\n    ```\n    We pass the training parameters as a user input and pass these parameters as a json configuration to the training. We release the default configuration (including these values mentioned above) as part of our artifact release.  We evaluate iRank based on a $5$-fold cross validation. In each of these $5$ experiments, the set of problems used in training and in evaluation are completely separate. \n\n4. **Complexity Analysis:**\n    1. We agree with the reviewer that the dataset is small (we have only 541 problems ). However, our results demonstrate that, even with such a small dataset, the ranker learns the semantics of the invariant synthesis problem, i.e., iRank can place the correct invariant on top of majority of the incorrect invariants. We believe with additional problems (and corresponding correct and incorrect invariants) added to the training data, performance of iRank will increase. \n    2. For training $iRank$, the maximum training epoch is set to $20$. On average, it takes iRank training $9$ epochs to reach maximum validation metric (which in our case is $V@1$). This shows, even with this small data, iRank is not learning any trivial ranking knowledge (our hypothesis is that if $iRank$ was learning trivial ranking knowledge, the maximum validation metric would’ve been reached very soon after the start of the training). We performed another experiment with TF-IDF based reranker, and the performance of such is very poor compared to iRank. For ranking `gpt-3.5-turbo` generated invariant candidates, $V@1$ for TF_IDF is $17.6$, which is higher than expected ranks from LLM ($V@1 = 8.8$). However, $V@1$ is $28.0$ and $29.2$, for $iRank-ada$, and for $iRank-davinci$, respectively. For ranking `gpt-4` generated invariant candidates, $V@1$ for TF_IDF is $32.0$, which is higher than expected ranks from LLM ($V@1 = 23.6$). However, $V@1$ is $33.6$  and $33.5$, for $iRank-ada$, and for $iRank-davinci$, respectively.\n    3. During ranking, iRank computes the dot product of the problem embedding and all the candidate invariant embeddings. If the number of candidate invariants is $O(n)$ and the embedding dimension is $d$, the complexity of reranking is $O(n*d) + \\Theta(nlgn)$ (for sorting).  \n\nWe really hope these answers clarify any confusion. Once again, we thank you for the review and the comment. We will add these in the camera-ready version of the paper.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- The literature review seems comprehensive to identify prior work in synthesizing loop invariants for program verification, as well as providing a background in recent LLM models. Authors also motivate their problem setting by identifying limitations with the existing work and with the Background & Motivation section.", "reasons_to_reject": "- It would help if the authors could more concretely list out their contributions as a section/subsection so it would be easier to follow. \n- Figure 1b for iRank’s architecture seems somewhat abstract and not that help to follow for understanding the architecture. Can the authors include more model details in this figure? \n- Further, the model details are too ambiguous to be able to reproduce the paper. For example, it is simply mentioned that an embedding model is used to extract the embedding of problem definitions and the invariants, but no details provided about the embedding model. Furthermore, it is just mentioned that a Transformation function is applied but no details regarding it. As a result, it is also difficult to determine the contribution and novelty of the proposed method with these important elements missing.\n- The datasets seem to be very small in the range of hundreds or thousand questions. What is the scalability of the proposed model? Can the authors provide some complexity analysis?", "questions_to_authors": "See weaknesses section above.", "paper_topic_and_main_contributions": "This paper proposes a re-ranker model for LLMs, with the goal of distinguishing between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized using contrastive loss. The authors conduct various experimental results showing that their model leads to a reduction in the number of calls to a verifier.", "excitement": 3, "reproducibility": 3, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "58sH0ZAL9I", "reviewer": "Reviewer_p5MA", "summary": "", "questions": "A - Could you give an analysis of wall-clock time? For example, what is the average time needed to find the correct invariant (including LLM generation time, ranking time, checking time) in the Emb. and iRank scenarios in Table 1?\n\nB - Could you give more details on how iRank was trained? What is the architecture on top of the un-trained embeddings? How many epochs was it trained over? What was the optimizer? How are the data folds different, and how much data was there?\n\nC - There has been a long line of work prior to yours from the PL literature on synthesizing loop invariants. How do you envision combining your method with some of these existing techniques?", "limitations": "", "rating": 3, "confidence": 4, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their insightful comments and suggestions. Here are the answers to the reviewer’s questions. \n\n1. **Comparison of Time:** Following the reviewer’s suggestion, we performed an experiment, where the metric is time. In particular, we measure the verification time without the ranking (i.e., following the LLM-rank). When we do rank (either based on raw embeddings, or based on trained embedding), we calculate the time to embed, rank, and verification time until a correct invariant is found. Below are our analysis results. \n\n    Below are the results for ranking candidate invariants generated by `gpt-3.5-turbo`.\n\n    | Experiment | Mean $i^+$ rank | $V@1$ | $V@10$ | Embedding Time | Ranking Time | Verification Time | Total Time |\n    |------------------|----------------|-------|--------|----------------|--------------|-------------------|------------|\n    | LLM-Ranks  | $189.78$ | $5.2$ | $18.4$ | $0$ | $0$ | $7.33$ | $7.33$ |\n    | Expected Ranks | $95.33$ | $8.0$ | $25.2$ | $0$ | $0$ | $3.67$ | $3.67$ |   \n    | Emb. Ada  | $115.89$ | $11.2$  \t| $30.0$   \t| $1.29$           \t| $0.05$         \t| $4.43$              \t| $5.78$       \t|\n    | Emb. Davinci | $120.02$          \t| $10.4$  \t| $33.6$   \t| $9.17$           \t| $0.45$         \t| $4.79$              \t| $14.41$      \t|\n    | $iRank$-ada | $38.78$           \t| $28.0$  \t| $60.8$   \t| $1.29$           \t| $0.06$         \t| $1.64$              \t| $2.98$       \t|\n    | $iRank$-davinci | $34.48$           \t| $29.2$  \t| $62.8$   \t| $9.17$           \t| $0.48$         \t| $1.28$              \t| $10.93$      \t|\n\n    Below are the results for ranking candidate invariants generated by `gpt-4`.\n\n    | Experiment | Mean $i^+$ rank | $V@1$ | $V@10$ | Embedding Time | Ranking Time | Verification Time | Total Time |\n    |------------------|-----------------|-------|--------|----------------|--------------|-------------------|------------|\n    | LLM-Ranks | $39.20$           \t| $17.6$  \t| $51.6$   \t| $0$              \t| $0$            \t| $1.61$              \t| $1.61$       \t|\n    | Expected Ranks | $20.23$           \t| $31.9$  \t| $65.4$   \t| $0$              \t| $0$            \t| $0.83$              \t| $0.83$       \t|\n    | Emb. Ada | $20.69$           \t| $26.6$  \t| $64.9$   \t| $0.23$           \t| $0.01$         \t| $0.67$              \t| $0.94$       \t|\n    | Emb. Davinci | $23.56$           \t| $27.7$  \t| $63.3$   \t| $1.93$           \t| $0.12$         \t| $0.75$              \t| $2.80$       \t|\n    | $iRank$-ada | $13.18$           \t| $44.7$  \t| $81.4$   \t| $0.23$           \t| $0.02$         \t| $0.44$              \t| $0.72$       \t|\n    | $iRank$-davinci | $11.96$           \t| $44.7$  \t| $81.9$   \t| $1.93$           \t| $0.13$         \t| $0.74$              \t| $2.80 $      \t|\n\n    As suggested by the reviewer, we augmented the Table-1 with wall clock time. As we can see from the table, without any ranking (as generated by the `gpt-3.5`), the mean time to find a correct invariant if $7.33s$, all of which are accounted for the calls to Z3 for verifying correctness of candidate invariants. With iRank, there is an overhead of embedding and ranking. For $iRank-ada$, median time to find the correct invariant is $2.98$, significantly lower than the time needed from LLM-ranks. However, we observe that, for $iRank-davinci$, the time is more than that of LLM-ranks. Investigating further, we observe that while iRank-davinci does improve the verification time, embedding time for `davinci-similarity` is significantly higher. There could be several explanations behind such behavior. Unfortunately, since we used OpenAI API for getting the embedding, we can only conjecture the explanation. Nevertheless, we believe `davinci-similarity` (embedding dimension = $12288$) embedding model is a much bigger model than `text-embedding-ada-002` (embedding dimension = $1536$). In addition, network latency, rate limit of the OpenAI subscription plans could be issues. Due to these factors beyond our control, we report the number of z3 calls. In this paper, we show that while LLM can be used to generate invariant, a simple ranker could save a lot of wasted verification effort. We do hope this research will augment future research on generate and validate based invariant synthesis.  \n\n2. **Quality of the LLM-generated invariants:** To understand LLM-generated invariants qualitatively, we ought to investigate how semantically diverse invariants are generated by the LLMs. Identifying semantic diversity is a non-trivial task - to simplify the problem, we identify semantically duplicate invariants from the candidate invariants generated by the LLMs.  We evaluate whether two invariant $i_1$ and $i_2$ semantic equivalent by evaluating the following SMT formula with Z3, $\\forall{v_1, v_2, …, v_n}(i_1(v_1, v_2, …, v_n) \\Leftrightarrow i_2(v_1, v_2, …, v_n))$. We find that `gpt-3.5-turbo` generated $9.29$% semantically duplicate invariants, and `gpt-4` generated $4.70$% semantically duplicate invariant – showing that LLMs generate diverse set of invariant candidates. \n\n3. **Details about the model and training:** We apologize for the missing details. We have uploaded the redrawn image articulating more details about the $iRank$ architecture and training/ranking method [in this anonymous link](https://figshare.com/ndownloader/files/42163257/preview/42163257/preview.jpg). For the embedding transformation, we use a 3-layered fully connected feedforward ANN. The hidden dimension of the embedding transformation model depends on the initial embedding model. For instance, when we use embeddings from `text-embedding-ada-002` model, the hidden dimension is $1536$. Also note that, since we are extracting initial embeddings through OpenAI API, the only learnable parameters in iRank are in the Embedding Transformation module. After we extract the initial embeddings for both the problem definition and the invariant candidates from OpenAI embedding models using their API, we transform them using the $iRank$ embedding transformation module . We optimize $iRank$ to bring the transformed embedding of the problem closer to the correct invariant and further away from the incorrect invariant from the training set. To optimize we use the `MSELoss` where the expected similarity of the problem and correct invariant is 1 and with incorrect invariants, it is 0. Here are the training details. \n    ```json\n    {\n        \"optimizer\": \"Adam\",\n        \"learning_rate\": 5e-05,\n        \"num_train_epochs\": 20, \n        \"weight_decay\": 0.001,\n        \"max_grad_norm\": 1.0,\n        \"lr_scheduler_type\": \"linear\", \n        \"warmup_steps\": 500,\n        ...\n    }\n    ```\n    We pass the training parameters as a user input and pass these parameters as a json configuration to the training. We release the default configuration (including these values mentioned above) as part of our artifact release.  We evaluate iRank based on a 5-fold cross validation. In each of these 5 experiments, the set of problems used in training and in evaluation are completely separate. \n\n4. **Details about the dataset:**\nWe evaluate iRank on the SyGus benchmark, which includes the loop invariant synthesis problem from several different sources, including different verification challenges. The problems include _Linear Integer Arithmetic_ (91.68%, 496 out of 541), _Array Linear Integer Arithmetic_ (3.33%, 18 out of 541) and _Non-linear Integer Arithmetic_ (4.99%, 27 out of 541) problems. Here are more detailed statistics of the problems in the dataset. \n\n    | Problem Type Statistics         |                |\n    |---------------------------------|----------------|\n    | Linear Integer Arithmetic       | $496$ ($91.68$%) |\n    | Non-Linear Intehger Arithmetic  | $29$ ($4.99$%)   |\n    | Array Linear Integer Arithmetic | $18$ ($3.33$%)   |\n\n    | Problem Semantics Statistics |                          |\n    |------------------------------|--------------------------|\n    | Number of functions          | Min = $3$, Max = $9$     |\n    | Number of variables          | Min = $2$, Max = $90$    |\n    | Variable Types               | Integer = $80.31$%       |\n    |                              | Boolean = $19.31$%       |\n    |                              | Array[Integer] = $0.36$% |\n    |                              | Array[Boolean] = $0.03$% |\n\n    | Operator Statistics (of correct invariants)        | % of all operators | Avg. # per examples |\n    |----------------------------------------------------|--------------------|--------------------------|\n    | Conjuctions                                        | $43$                 | $1.12$                     |\n    | Disjunctions                                       | $20$                 | $0.53$                    |\n    | Negations                                          | $37$                 | $0.96$                     |\n    | Addition/Subraction                                | $43$                 | $0.5$                      |\n    | Multiplication/Division                            | $3.1$                | $0.18$                     |\n    | Logical Comparison                                 | $88.5$               | $2.25$                     |\n    | Examples with quantifiers ($\\forall$ or $\\exists$) | $7$                  |  \n\n    | Length Statistics           | Min | Max  | Avg |\n    |-----------------------------|-----|------|-----|\n    | Problem Length (NLTK)       | $92$  | $2732$ | $740$ |\n    | Problem Length (TokToken)   | $88$  | $3146$ | $922$ |\n    | Invariant Length (NLTK)     | $18$  | $605$  | $110$ |\n    | Invariant Length (TikToken) | $15$  | $506$  | $125$ |\n\n\n5. **Integration of iRank with Symbolic technique and Future direction:** There is long line of work with symbolic heuristics for synthesizing Loop Invariants falling into mostly two broad categories (a) generate and validate (G&V) based, and (b) abstract interpretation based. We envision our technique augmenting the generate and validate line of work in invariant synthesis. iRank could be an orthogonal addition to the generation in the G&V approach, where after generation, iRank reorders for effectively reducing the cost of validation. \n\nOnce again, we thank the reviewer for the thoughtful comments and reviews. We hope our answers clarifies the reviewer's questions. We will incorporate these changes in te camera ready version.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. To my knowledge, this is the first work that tackles the problem of generating loop invariants in the SMT format automatically with LLMs. The closest to this is a previous work on generating loop invariants (Pei et al) and only considers Java.\n2. The authors introduce a training and evaluation set for this task that would allow for future advancements in this direction.\n3. The authors propose an interesting contrastive learning training framework that pulls correct invariants closer to the embedding of the problem and incorrect invariants further. It is simple and intuitive.\n4. The evaluation is sound and shows that the framework in 3) improves the ability to identify correct invariants.", "reasons_to_reject": "1. One of the main claims made by the paper is that iRank can lead to a significant reduction in the verification cost. The authors cite the number of Z3 calls as evidence of this, but there are additional dimensions of wall-clock time and monetary cost. Calling a LLM would certainly lead to increased monetary cost, and there is no analysis of wall-clock time reported.\n2. There is no qualitative analysis, so it is hard to understand the effect of iRank in depth. For example, does the LLM generates many obviously incorrect solutions that even simple heuristics could filter out a majority of the incorrect ones? Perhaps iRank is very effective for a certain class of invariants but not for others, but there is no way to tell that from what is presented here.\n3. The data details, architecture details, and training details of iRank are unclear.\n4. From my perspective, one of the main contributions of the paper (aside from ranking) is the introduction of this task for SMT invariant synthesis. The authors do curate a dataset, but do not give any details analyzing this dataset (e.g. a taxonomy of problems that are included in the dataset, difficulty of problems, histogram of lengths, etc.)", "questions_to_authors": "A - Could you give an analysis of wall-clock time? For example, what is the average time needed to find the correct invariant (including LLM generation time, ranking time, checking time) in the Emb. and iRank scenarios in Table 1?\n\nB - Could you give more details on how iRank was trained? What is the architecture on top of the un-trained embeddings? How many epochs was it trained over? What was the optimizer? How are the data folds different, and how much data was there?\n\nC - There has been a long line of work prior to yours from the PL literature on synthesizing loop invariants. How do you envision combining your method with some of these existing techniques?", "paper_topic_and_main_contributions": "The paper is about improving a LLM's ability to generate loop invariants for programs. The authors:\n1) use existing loop invariant synthesis benchmarks to curate a training set of invariants\n2) use contrastive learning to train a ranking model to compare various generated invariants\n3) show that the ranker can improve the ability to choose the correct invariant by measuring a) the mean rank of the correct invariant among a list, and b) the percentage of problems where the invariant is found among the top-K invariants.", "excitement": 3, "reproducibility": 4, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"Missing_References": "References are great!", "Typos_Grammar_Style_and_Presentation_Improvements": "It would be great if Figure 1 included the architecture details of the embedding model."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors propose a new method for synthesizing inductive loop invariants in program verification, as well as an accompanying dataset for future advancements in this direction. Reviewers agree the approach offers new speed ups and analysis will be useful to practitioners facing this problem. Listed limitations/concerns from the reviewers mainly concentrate around discussion of how this work's contributions differ/advance prior work, and qualitative analysis of iRank.
Decision: Accept-Findings