Lemur: Integrating Large Language Models in Automated Program Verification
Authors: Haoze Wu
Clark Barrett
Nina Narodytska
Venue: ICLR 2024 poster (2024)
Keywords: Large Language Models
Formal verification
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We present a general methodology for combining LLMs and formal verifiers for automated program verification.

Abstract: The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.

Published as a conference paper at ICLR 2024
LEMUR: INTEGRATING LARGE LANGUAGE MODELS IN AUTOMATED PROGRAM VERIFICATION
Haoze Wu," Clark Barrett
Nina Narodytska VMware Research
Department of Computer Science Stanford University [haczewu, barrett barrett/estanford.t Jestaford.
VMware by Broadcom
n. ww.narodyyskkeegaillccom com
ABSTRACT
The demonstrated code-understanding capability of LLMS raises the question of whether they can be used for automated program verification, task that demands high-level abstract reasoning about program properties that is challenging for veri- fication tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally de- scribe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as sound automated verification procedure and demon- strate practical improvements on set of synthetic and competition benchmarks.
INTRODUCTION
Al-powered language models are being routinely used to help developers. Examples include pro- gram synthesis from natural language descriptions by GPT-4 (OpenAI, 2023) or Github Copi- lot (Chen et al., 2021; GitHub, 2021), and repairing code (White et al., 2019), among others. These models have shown impressive results in generating correct code in many programming languages.
An important research question is whether modern AI models are capable of understanding the logic behind the programs they analyze. Recently, several approaches have been proposed com- bine the strengths of formal verification and Large Language Models (LLMM) that demonstrate such capabilities. For example, Pei et al. (2023) made an important step this direction by investigat- ing whether LLMs can generate program properties, namely, program invariants, which remains crucial and challenging task for automated program verification (Clarke et al., 2018). The authors a set of synthetic Java
demonstrated that LLMs are effective in generating program invariants programs. Another example is the recent work by Charalambous et al. (2023), who demonstrated that LLM models can be used repair vulnerabilities in code, given examples of incorrect behav- ior. They provided compelling evidence of the complementary strengths of LLMs, which serve as a generator for code repair snippets, and formal techniques, which used check the correctness of the generated code. While these approaches show promise in program analysis tasks, they do not provide a formalization of the interaction between LLMs and formal verifiers, they require manual effort, or they are limited to the invariant generation process as stand-alone procedure.
In this work, we propose novel LLM-powered framework, LEMUR, for automated program veri- fication tasks. Our key idea is to combine LLMs' ability to perform abstract high-level reasoning and automated reasoners' ability to perform precise low-level reasoning. Specifically, LLMS are em- ployed to propose program invariants in the form of sub-goals, which are then checked by automated reasoners. This transforms the program verification tasks into a series of deductive steps suggested by LLMs and subsequently validated by automated reasoners. Our main contributions are:
a novel framework for combining L.MSs and automated reasoners for program verification;
a presentation LEMUR as proof system and a proof of soundness, which to the best of our knowledge, is the first formalization of such hybrid approach:
an instantiation of the LEMUR calculus that gives a sound and terminating algorithm; implementation of the proposed framework (using OpenAl's GPT models);
"This work mostly done during an internship VMware Research.

---

Published as a conference paper at ICLR 2024
experimental evaluation of LEMUR two sets of benchmarks that demonstrates its efficiency compared with both existing Al-powered and conventional verification tools.
We highlight that LEMUR is the first fully automated framework combining LLMs and reasoners.
DEFINITIONS
Given program P Prog, reachability property, or simply property, tuple p (Ø, where Φ Pred is a Boolean predicate of the program state and 1 N is a progrum line. The negation of p. denoted -p. is defined as {-Ø, 1). Next we introduce several useful definitions and their properties.
( is an invariant P, denoted Inv (nv(P,,) .p), iff y holds (i.e. always evaluates to true at line for all possible executions of the program P.
Definition 2.1. A property
Example 2.1. Consider the simple program in Figure 2 (the first frame, top row). instantiates an unsigned 32-bit integer variable x to 0 and increases its value by 4 on each loop iteration. A property p {Ó. 1) specified on the 4th line, so à = (x != 30) and for this property. is easy to see that p an invariant as x will never be divisible by 3, for example.
An assumption () is a condition that is assumed in a program.
Definition 2.2. An assumption q == (é.1) I) modifies a program as follows:
1. if holds at line during some execution of then P continues execution without changes; 2. @ does not hold at line l during some execution of then that execution terminates at We use p' ASmmmP .q denote the modification of P with the assumption q. An assumption can itself be an invariant. We now introduce a special notion of an implication.
Definition 2.3. Let P be a program, and q be properties on P. We say that implies p with respect to P, denoted q ?? p. ift p is an invariant Asm(P, (P,g). .)-
Example 2.2. Consider the program P in Figure 2 and an assumption q q= (á (x84==1),1 3), with P' Asm(P, P..) 9) (depicted in the first frame the bottom row of Figure 2). To see the difference between P and P', observe that the loop is executed only once in P This is because x=0 when entering the loop, so (x84) )) !=1, which is the formula & in q. does not hold, and therefore, P' terminates. If we consider the fourth frame at the bottom of Figure 2). we can see that its predicate & holds for all executions.
alternative assumption q' {ő (xx4==0),
3) (depicted in
Hence, o' is an invariant for P. Finally, we can see o' ?² P. where p is from Example 2.1.
The following propositions follow from the definitions above.
Proposition 2.1. Let P be program, and p. q be properties on P:
The property is an invariant on P if q is an invariant on P and implies p with respect to P. More formally, (Inv(P,g) q p) = Inv(P, .P)-
The property p is not an invariant on P if the property p not an invariant on P' Asm(P.g g). More formally, -Inv(P', p) + -Inv(P,p).
Proposition 2.2. For any property p on a program P. p.
p
Proposition 2.3. For any properties 1r r on program P, if - and q - then r. p
p Note that it is possible that neither a property p nor its negation -p is an invariant Example 2.3. Consider again our example from Example 2.1 and two properties at line 3:
program.
3). Neither p nor p' is an invariant P. On the first loop iteration, we have that x=0 before line 3, so o' holds and 6 does not at line 3. But on the second loop iteration, we have that x=4 before line so Φ holds and o' does not.
(ób = (x88==4), 3) and p' = (ø' = (xx8:=4)),
Definition 2.4. A property p (0.1) is stable for P, denoted S(P.p) p), if. for each execution of the program, either @ always evaluates to true at line or always evaluates to false at line l.
Example 2.4. Consider an example to illustrate the definition of stability.
Line 1: uint32_t x=rand ()
Line 2: assert (x==1);
The property in Line is stable, it always evaluates true or false within single execution.
2

---

Published as a conference paper at ICLR 2024
An invariant must be stable, but property that is not invariant might still be stable. For example, any property on a program without loops is stable. If p is stable, then -p is also stable. Lemma 2.1 exploits stable invariants (see proof in the extended version of the paper (Wu et al., 2023)).
Lemma 2.1. Consider a program P. two properties p. on P. and a program P' - -Asm( (P.g). The property p is an invariant on P if: (i) q is stable for P: (ii) q implies p with respect to P; and (iti) qq implies with respect to P. More formally: S(P, ((P.g) () A (q - p) A (-g - p) = Inv(P.P). Assume we have verifier V Prog xP(Prop) x Prop + (TRUE, FALSE, FALSE, ÜNKNOWN). which takes as inputs a program P. a set of assumptions A and a property
and checks whether A implies p. More precisely, given set of assumptions A = {qI,..., Ir we construct a new program p' = Asm( (aan(Ass((...... Asm(P, 91 91)), (n)-)) gn) and the verifier checks if p is an invariant on this program. Hence, a statement that A implies p on P means that p is an invariant on P', We further assume that V is sound, meaning if V returns TRUE, then A implies p. and if V returns FALSE, then A does not imply p. Note that A can be empty, in which case the verifier just checks whether is an invariant. When the verifier V returns TRUE, we say p is proven; and when V returns FALSE, say the property is falsified. V is incomplete, meaning that V can return UNKNOWN.
In practice, V can be instantiated with an automated program verifier such as CBMC (Kroening & Tautschnig, 2014), ESBMC (Gadelha et al., 2018), or UAUTOMIZER (Heizmann et al., 2013). We provide an overview of the main techniques employed by these tools in the extended version of the paper (Wu et al., 2023) and note here that a crucial challenge shared across existing verifiers is the automatic decomposition of verification task into smaller, more manageable sub-tasks. This decomposition requires high-level reasoning that is difficult to automate using conventional formal methods, but plausibly could be performed by LLMs, with their documented code-understanding ca- pability. However, it is crucial to preserve soundness when LLMss are used to automatically perform this high-level reasoning in program verification tasks.
LEMUR: INTEGRATING LLMS IN PROGRAM VERIFICATION
We present LEMUR, proof calculus that combines LLMs and automated reasoners to prove proper- ties of programs. The calculus operates over a configuration, which is either one of the distinguished symbols (SUCCESS, F or a tuple (P. A, MM, where P is a program, A is either Ø or a singleton representing the assumption, and M is list of properties referred to as proof goals. M itself is referred to as trail. The last element of M represents the current property to prove. We use the notation :: to denote a concatenation of two lists. In particular, .M = M' p means that M is concatenation of trail M' and a property p, where p is the last element of M. The rules describe the conditions under which a certain configuration
transform into another configuration. In this calculus, deciding whether Inv (av,P, p) holds reduces to finding a sequence of valid rule applications from the starting configuration (P, Ø, [p] to either SUCCESS FAII..
Our calculus performs oracle calls to LLMs to propose new properties and revise them. The oracle O propose Prog Prop + P(Prop) proposes new properties, given program and the current proof goal as inputs. A key hypothesis here is that LLMs are capable of generating new properties that likely to (i) be invariants, and (ii) imply the proof goal given in prompt. We will discuss strategies to generate prompts in Section 4. Importantly, properties generated by an LLM are treated as assumptions until we can prove that they are invariants of the original program. The oracle Oeepair revises previously proposed properties, c.g., if we determine that a property previously produced by Opropuse does not hold or does not imply the current proof goal. In this case, we request an LLM to repair q. We have Orepair Prog x Prop x Prop x (FALSE, UNKNOWN] + P(Prop), whose inputs comprise a program, two properties, and a solver return value. The first property is the current proof goal, and the second property q is an assumption previously proposed by oracles. The output of Oropair is a new set of properties. In practice, we implement it with a prompt to an LLM to either correct strengthen g (see Section 4). Finally, the calculus performs external call to verifier y to check whether a property holds.
The proof rules of LEMUR are shown in Fig. 1. Each rule defines a set of conditions that must hold for the rule to be applicable. Note again that these conditions permit invocations of LLMs and/or verifiers. The rules within the calculus can be partitioned into four groups.
The first group contains rules that are responsible for generating new proof goals for specific con- figurations. These rules are Propose, Repair 1, and Repair 2. The Propose rule states that if the
3

---

Published as a conference paper at ICLR 2024
M=M' up V(P, A, p) UNKNOWN 9 E Opmeose (P, p)
(Propose)
P,A, M - M
A= (q) M=
V(P,A, = TRUE
(Decide)
P,A,M = P;
= Mp V(P,A, 9) + TRUE of E Opuppse (P, p) (Backtrack)
P.A.M P. P/). M:P:p
A= (1) M V(P.A, UNKNOWN g' E Oxsair (P, P. UNKNOWN)
(Repair 1)
P.A.M MMMMPP P. (4), ::P:
A= M VIP.A. 9) FALSE o' E Oxpoir (P, p.q: FALSE)
(Repair 2)
P.A.M M = P,(8'). M' ::
A= M M :: V(P.A, p) TRUE
(Success 1)
P,A,M SUCCESS
A= M M' :p::4 S(P,4) ((P.(-4) p) -RUEE
(Success 2)
P,A,M SUCCESS
M= jp
V(P.A.)) = FALSE
(Fail)
P.A,M- =
FAIL
Figure I: Deductive rules of the LEMUR calculus.
verifier is unable to prove or disprove the current proof goal p. we can invoke the O propose oracle to obtain property q and update A to be {g}. The Repair 1 rule can be applied when the current assumption q is not sufficient for the verifier to prove the current proof goal p. In this case, we can use the oracle repair to propose ways to strengthen q and choose one of them, T', as the new assumption. The Repair 2 rule can also be applied when q is already in the trail but is falsified by the verifier V. In this case, we can use Orepair to repair and update A accordingly.
The second group contains only the Decide rule. This rule allows an assumption q to become a new goal (i.e., be appended to MM) if the verifier V is able to prove that q implies the current goal.
The third group allows LEMUR to recover from faulty assumptions. The Backtrack rule applicable when there at least two elements in the trail and the verifier cannot prove the current proof goal. allows LEMUR to revert to the previous proof goal (the second to last property in the trail M) and pick different assumption suggested by O proppsse- Note that Backtrack might not be the only applicable rule. For example, Repair or Repair 2 could also be applicable. In practice, we use a strategy decide between multiple applicable rules. This is discussed in Sec. 4.
The final group specifies three termination conditions for the calculus. The Success rule states that whenever the assumption is empty and the verifier is able to prove the current proof goal (i.e., the last property p in the trail .M). we can transition into the SUCCESS state. Note that if the verifier can prove the original property, then this rule can be directly applied the starting configuration reach SUCCESS, Success states that if the last two elements of the trail A are and g, the current proof goal = (ó. 1) is stable (as defined Sec. 2), and the verifier also able to also prove p under the assumption (-0. 1). then p is an invariant (as consequence of Lemma 2.1), and we can transition to SUCCESS. The Success 2 rule constitutes a way to utilize an incorrect sub-goal y proposed by the LLM-based oracles to decompose the verification task: we separately reason about the cases when q holds and when it does not hold. Finally, the verifier V proves that the original property is not an invariant, whether under an assumption or not, then we transition to the FAIL state using Fail.
Note that the program P remains unchanged in every rule. We keep it as part of the state for two reasons. First, is convenient for keeping the calculus self-contained, as P is input the verifiers and the oracles. Second, in the future, it might be possible to augment the calculus with rules that update P. by, for example, rewriting the program using LLMs in an invariant- prrereivt-rreevvingg manner.
We state the following soundness propertics about LEMUR. The proof is presented in the extended version of the paper (Wu et al., 2023).
4

---

Published as a conference paper at ICLR 2024
UNKNOWN
V: TRUE
V: UNKNOWN
TRUE
3int x=0;
uint 2 x=0, while (rand
Oxpui
while Irand
32_t x=0;
vint x= while (rand assert (X34--1)) x+=43
while ()))
xt-4;
Propose
assume (x52-=0);
Rep.
aszume 0x x+mdy
Decide
Suce.
assert (x:=33))
x+=0;
assect (x1=
susert bx1-30);
Propose
x4mdr
sesert (x!330);
V: TRUE
V: FALSE
V: TRUF
List invariants that prove the aesertion. Your answer should look 1ike
uint 32_t x=0;
(1and
32_t x=0;
Opepon Backtrack
while (rand (3)
Lint x=0;
while ()and()) 1
aagume (xY4--11;
Decide
assect 1x81-=117 xt-4;
assume (XS4- x+=d;
assert (...) //Line number
x+=0;
ausect (xl -301
aesert (x113037
sesert (x 0); //Line
sssert (X 4 -- 11; //line
Figure 2: A running example of executing the LEMUR calculus.
Theorem 3.1 (Soundness). Given property Po and program P, if SUCCESS is reached by sequence of valid rule upplications from (P, Ø, (pol). then p is an invariant on P.
Theorem 3.2 (Soundness 2). Given property Pu and program P. if FAIL is reached by sequence of valid rule applications starting from (P, Ø [po]), then p is not an invariant on P.
Example 3.1. To provide more intuition about the proof system and to motivate the design choices when instantiating LEMUR, we consider again our running example. Figure 2 illustrates how LEMUR can be used to verify properties in practice. In Figure 2 each frame represents a state of the program. Transitions between states are depicted by arrows, with each arrow marked with the rule applied to execute this transition. In this example, our goal is to prove the property x x!=30 in a while loop that keeps adding 4 to an unsigned 32-bil integer variable x. We note that this partic- ular verification task is adapted from similar one in the SV-COMP competition." While seemingly trivial, during the competition, 19 out of the 24 participating tools (including the overall winner of the competition UAUTOMIZER) were not able to solve this benchmark.
The initial configuration is (P, Ø, (p))). where P is the given program and p = (x,33),3), Sup- pose the verifier V is unable to solve this problem and returns UNKNOWN. In this case, we need to generate a new proof goal, so the only rule we can apply is Propose. To do so, we invoke the LLM- based oracle O Propose obtain set of new properties that are potentially themselves invariants and might help prove the property. An example prompt is given in the bottom left of Figure 2. Note that this is not the exact prompt we found most useful, but we defer a full discussion of prompts and prompting strategies to Sec. 4. Suppose the oracle returns two potential predicates, both of which should hold at the beginning of the while loop (line 3); x and x----1. The Propose rule allows us to make one of them the current assumption.
Case (x$2==0); The top row illustrates what happens when we transition to (P, (x82==0,3) (p))- While is indeed an invariant, it does not help to prove the assertion, and still returns UNKNOWN. This means that the Repair rule is applicable, which invokes the oracle O repair to strengthen q. Suppose in this case, the oracle suggests the predicate q' x x84==0, which clearly implies the original property x !=30. Now, suppose VPP, (4),p) returns TRUE We can apply the Decide rule and transition to (P, Ø, (p, q'l), making q' the current proof goal. Proving q' is arguably easier because x84--0 is inductive (i.e., if holds in one iteration, then it will hold in the next iteration), making conventional automated reasoning techniques such as k-induction appli- cable. Now, V(P, 2, d') = TRUE, we can apply Success I and transition to the SUCCESS state, thus completing the proof.
We discuss the case x84==1 in the extended version of the paper (Wu et al., 2023).
httpp:: //vta/op/////...oooo//o/o//o sosy- 1ab http.//a.ooorre////aa/aaaaaaaaaa
wwteeeerrrfiee/ee Fied/META_ ue (jain_5-2))
Rea ceayffffety.... table e html F t/table? oeffiteer -eteeedrddaan (va lue
23 is the line number (in the snippet) where the predicate is asserted.
5

---

Published as a conference paper at ICLR 2024
Algorithm The LEMUR procedure
1: Input: A program P. a property p.
Output: SUCCESS only if [nv(P,p): FAIL only -Inv(P, p):
UNKNOWN inconclusive.
3: Parameters: Verifier V, oracles Orropse and Orepir (which satisfy Condition 1), number of proposals k
4: function lemur check(P,
5: d + V(P, p)
6: if FALSE then return FAIL
b Fail Success
7: else if = TRUE then return SUCCESS
8: else
9:
i, Q + 0, propose (P,p)
10:
while i < k k [Q]
do
1
12:
++ QQ)
13:
- V(P, (1)
b Propose/Backtrace
14:
if FAI.SE then return FAIL
Fail
15:
else if e TRUE then
16:
f ^ Seemur_check(( (P.,)
Decide
17:
if f = SUCCESS then return SUCCESS
Success I
18:
else if S(P, A (V(P,(-q)
= TRUE) then return SUCCESS
b Success 2
19:
else if FAIL then Q + jQin(Q, Oreaar (P, P. q. FALSE))
Repair 2
20:
else continue
21:
else Q + join(Q, Oropirr (P, ,P... UNKNOWN))
Repair 1
22:
return UNKNOWN
4
INSTANTIATING THE LEMUR CALCULUS
In this section, we present strategies for instantiating LEMUR as automated procedure. While showed that the LEMUR calculus is sound, there are no guarantees that it terminates. Here, we will discuss two sources of non-termination.
The first one corresponds to an unbounded sequence of suggestions for new sub-goals. Concretely, when trying to prove a particular proof goal p. we could get stuck if V(P, {)).p) UNKNOWN or V(P, Ø, g) = FALSE for each proposed assumption q. This could occur as result of limitations in either the LLM or the verifier. One way avoid this type of non-termmiatton by putting an upper bound on the number of proposed assumptions for each proof goal. That is, for any proof goal we require that VPP (4) p) invoked for at most k different values of q.
The second source of non-termination is the potentially unbounded depth of the trail M. Concretely, is possible to construct an infinite sequence of Propose and Decide transitions, where: (i) the verifier returns UNKNOWN not invariant but implies the current proof goal; (iii) the verifier proves the implication; (iv) the assumption becomes the new proof goal; and (v) this process repeats. This can be avoided by adding a side condition to the rules requiring that properties proposed by oracles (g = (e), (')) must contain smaller program line number than the one in the current proof goal (p (1), 1)), that is,
the current proof goal; (ii) the oracle proposes an assumption that
(v,1") E (..
(Condition 1)
Based on these strategies, terminating (by Thm. 4.1 at the end of this section) and sound (by Thm. 3.1) algorithm for checking whether a property p is an invariant on a program P is presented in Alg. 1. Alg. 1 is recursive procedure lemur check. It takes a program P and property p as inputs. If cemur_check returns SUCCESS, then the property is an invariant. If lemur check returns FAIL,, then the property is not an invariant. The function is inconclusive. At a high level, Alg. 1 searches for potential subgoal that implies the current goal p (lines 9-21). If such a q is identified in line 13, recurse prove q (line 16). The while loop starting at line 10 ensures that at most & attempts can be utilized to generate new subgoal for p. The comments in Alg. indicate which lines correspond to specific proof rules. The algorithm is sound as it only applies the rules of the calculus. A full description of Alg 1, including a proof of termination can be found in the extended version of the paper (Wu et al., 2023).
also return UNKNOWN if the analysis
Theorem 4.1 (Termination), Given a program P, and property on the program, Alg. terminates with either SUCCESS, FAIL, UNKNOWN.

---

Published as a conference paper at ICLR 2024
Note that, Alg. 1 is one of many possible instantiations of the LEMUR calculus. One can develop alternative strategies to apply the rules, e.g., by changing the frequency of the repair rules and the Propose rules to balance the cost of LLM oracle calls. We evaluate one of the alternatives in the extended version of the paper (Wu et al., 2023).
5 EXPERIMENTS
We have presented the LEMUR calculus and described a sound and terminating algorithm based on LEMUR. In this section, we investigate the following questions:
Can we develop a practical automated verification procedure based on Alg 1? [Yes]
Is LEMUR competitive with existing end-to-end learning-based verification approaches? [Yes]
Can LEMUR already prove hard benchmarks that are beyond the reach of state-of-the-art conven- tional program verifiers? [In several cases]
5.1 BUILDING AN LLM-BASED PROGRAM VERIFIER
We report on several practical considerations when building prototype of Alg. 1. There two types of external calls that Alg. depends on. The first type is calls to V. We use off-the-shelf verifiers in our framework that are extensively tested by the community (described in later para- graphs), so we have some expectations about their reliability and performance. On the other hand, the second type of calls, calls to LLM oracles, introduces more uncertainty, L.MSS newer and are treated as black boxes. In our framework, the oracles O propose and O Orepair automatically prompt GPT-family model through the OpenAI API and parse the output. We found that while GPT has great potential for generating sensible loop invariants, it still has practical limitations. We report several tactics that we found useful in practice.
Formatting the output: While investigating whether chain-of-thouge (CoT) (Wei et al., 2022) reasoning is useful when seeking new properties for P and p. We found that GPT's outputs, even when containing useful information, were verbose and often contained irrelevant or incorrect statements, making it difficult to extract invariants. To address this, we use in-context learning to encourage the LLM to format the output in specific way. For example, adding Your output should be "assert :); /// Line number" to the prompt is sufficient for GPT to consistently generate outputs of exactly this format, without providing verbose explanations.
Inserting markers in the program: We found that GPT is not good at counting program lines. Often, the generated predicate otherwise correct, but the line number slightly off. Unfortu- nately, an invariant at wrong position is of no use to the verifier. To mitigate this challenge, we insert placeholder lines of the form /// Line A", /// Line B" and prompt GPT to gener- ate invariants of the form assert ()..);// Line name (for those specific locations). As simple practical heuristic, we insert placeholders right before loops and at the beginning of loops.
Ordering the proposal: The output of an oracle call is non-deterministic for given prompt, depending on the hyper-parameete of the call. Moreover, the oracles produce a set of properties and we need good heuristics to choose the order of trying those properties. A heuristic we found useful is to prompt GPT multiple times and order the properties by the frequency with which they are proposed (breaking ties by preferring shorter expressions). Moreover, instead of relying on string matching, we treat two proposals the same if their abstract syntax trees are equivalent.
The exact prompts are described in the extended version of the paper (Wu et al., 2023). For V. consider two state-of-thed thetthe-tt-tttt art formal tools for C program verification, ESBMC (Gadelha et al., 2018) and UAUTOMIZER (Heizmann et al., 2013). The former is based on k-induction and the latter is based predicate abstraction. ESBMC and UAUTOMIZER were the top performing non-portfolio solvers in the reachability track of the most recent edition of the software verification competition (SV-COMP (Beyer, 2023)). Furthermore, UAUTOMIZER was the overall winner. By default, we impose 30-second time limit for each invocation of the verifier. That is, if the verifier does not terminate within 30 seconds, then the verifier returns UNKNOWN.
The source code and the henchmarks are publicly available at https: / / thub. www..ccoo/cocc...ccoooooo....ttt waao/// lemur- wwwrrrr-rrrrmmoom f cation.
7

---

Published as a conference paper at ICLR 2024
Configurations Solved Time (s) proposal
Configurations Solved Time (s) # proposals
Code2Inv
92
UAUTOMIZER
824.3
ESBMC
68
0.34
ESBMC
1
675.7
LEMUR(GPT3)
103
35.6
8.6
LEMUR(GPTS)
14
162.2
8.5
LEMUR(GPT4)
107
24.9
4.7
LEMUR(GPP4)
25
234.5
7.2
(a) The Code2Inv benchmarks.
(b) The SV-COMP benchmarks.
Table I: Solved instances by ESBMC, LEMUR, and Code2Inv (Ia) or UAUTOMIZER (Ib) on two benchmark sets. We also report the average time and number of proposals for solved instances.
5.2 LOOP INVARIANT GENERATION BENCHMARKS
A prominent approach in learning-basee end-to-end program verification is Code2Inv (Si et al., 2020), which uses reinforcement learning to train an invariant synthesizer to propose loop invariants. At high level, to infer a loop invariant for a given program, Code2Inv learns generative neural network whose goal is to repeatedly propose candidate invariants until automated reasoning tool determines that the candidate correct. Throughout this process, the generator fine-tuned using the feedback from the automated reasoning tool. In this section, we study how LEMUR compares with this approach on the same benchmark set considered in the original Code2Inv work. The benchmark set contains 133 benchmarks, each containing C program and a property expressed as an assert statement the program. Each program contains a single loop and each loop can have nested if-then-else blocks (without nested loops). The assertion to check is always after the loop. Cnde2Inv is designed to generate invariants at the beginning of the while loop. We prompt the oracles generate invariants at the same location.
We use the k-induction- based verifier, ESBMC, to check the implication (line 13 in Alg. 1) which aligns with the verification procedure used in Codc2Inv. We report the number of solved instances as well as the number of failed suggestions (either the suggestion itself cannot be verified or ESBMC times out on the implication check). As point of comparison, we report the statisties from the original Code2Inv approach. Code2Inv was given one-hour timeout. In addition, we also report ESBMC'S performance on this set of benchmarks. The result shown Table la (the Time column shows the average time in seconds to solve a benchmark).
With a 10-minute timeout, ESBMC alone can solve 68 problems. On the other hand, LEMUR) can solve 107 problems within the same time limit. Surprisingly, this approach solves more in- stances than Code2Inv, which is specifically designed for invariant synthesis tasks. For problems unsolved by ESBMC but solved by LEMUR(GPT4), histogram of the values of Logz of the number of proposals is shown in Fig. 3. While in most cases, Alg. can produce the correct proposals within attempts, there are bench- marks for which LEMUR(GPT4) requires many iterations to find the desired loop invariant, e.g., one of the benchmarks took 177 pro- posals. In addition, we experimented with the GPT-3.5 turbo LLM model, denoted SEEUU(GPPT)) LEMUR(GPT3) solved four fewer benchmarks and required more time and more calls to the GPT-3.5 turbo oracle.
18
18
Frequency
Proposals (Log 2)
Figure 3: Nb. of proposals for LEMUR(GPT4) to solve Code2Inv benchmark.
shown Table a Note that
5.3 SOLVING HARD SV-COMP BENCHMARKS
Next, we study LEMUR'S ability to solve hard benchmarks from the 2003 edition of SV- COMP (Beyer, 2023). We focus benchmarks with less than 150 tokens (after removing com- ments and unnecessary headers, and after applying flang-formattin). We select 47 benchmarks that ESBMC and UAUTOMIZER unable to solve within 10 minutes. The property is expected hold in all benchmarks. We use a 15-minute per-instance timeout.
The results are shown in Table 1b. Impressively, with the guidance of the proof goals suggested by the LLM, JEMUR)GPT4) is able to solve 25 of the 47 SV-COMP benchmarks. While ESBMC and UAUTOMIZER each solve only benchmark. Upon closer examination, 8 of the solved
8

---

Published as a conference paper at ICLR 2024
instances contain two loops and 5 contain three or more loops. This suggests that LEMUR is capable of (i) handling programs with more than one loop: and (ii) boosting the performance of state-of-the- art conventional C program verifiers.
The average number of proposals before solving a problem is higher compared to the Code2Inv benchmarks (7.2 vs. 4.7). Fig. 4 sheds more light on the behavior of LEMUR GPPT4). We observe that 12 of the 26 solved instances require least 5 proposals in total.
10
Frequeency
We found that LLM oracles can produce surprisingly insightful loop invariants which are difficult for conventional formal methods synthesize. While generate predicates that involve only the operators and values in the program and follow a particular template, LLMs are not constrained by these limitations. For example, for the program in Fig. 2, GPT-4 can consistently generate x84==0 as the loop invariant although the modulo operator is not present in the program. In another ex- ample, the LLM correctly understands the range of an unsigned char and suggests variable bounds as the assumption, which ends up being the key to proving the property. This example is shown in the extended version of the paper (Wu et al., 2023). There also several cases where the I.LM generates disjunctive invariants that precisely characterize the behavior of the loops.
based techniques typically
Proposals
Figure 4: Nb. of proposals for LEMUR(GPT4) to solve SV-COMP benchmark.
Finally, we observe that LEMUR(GPT4) significantly outperforms LEMUR(GPT3) across all met- rics. This suggests that the choice of oracle is also crucial for performance. Additional experiments are presented in the extended version of the paper (Wu et al., 2023). They include running the base- line solvers with a 12 hour timeout, using a configuration in which repair rules are not employed in Alg. I, and running LEMUR multiple times to account for the stochasticity of the oracles.
6 DISCUSSION OF LIMITATIONS AND EXTENSIONS
In this work, we propose novel framework, LEMUR, which combines automated reasoning and LLMs. To the best of our knowledge, LEMUR is the first framework to provide a theoretical founda- tion for such an integration via a formal calculus. We also implemented LEMUR as fully automated framework and demonstrated its efficiency on standard benchmark sets. We conclude by discussing the current limitations of LEMUR, which also point to future research directions.
As mentioned above, the practical performance of LEMUR depends on two types of external calls: the verifiers and the LLMs. Any improvements in these tools should translate into LEMUR im- provements. Currently, modern verifiers are capable of handling only relatively small programs (see SV-COMP'23 (Beyer, (023),, Interestingly, even when provided with strong invariant, they some- times cannot solve the verification problem. One research direction that we envision is to customize LEMUR a particular back-end verifier obtain better performance and solve larger programs.
We also note that LEMUR primarily focuses on imperative languages. Extending it to functional languages is a direction for future research.
While our experience with LLMs was largely positive (see Section 5.1 for a discussion of limitations that have already been least partially addressed), there are more interesting challenges to tackle. First, current LLMs have token limits, and many practical programs exceed those limits. Second, it is sometimes challenging for LLMs to generate complex logical formulas such as those with nested if-then-else expressions. We believe that to overcome this limitation, we need to (i) develop prompting language for LLM invariant generation, and (ii) fine-tune LLMs for invariant generation tasks using this language. Third, reasoning about programs with multiple loops remains challenging for LLMs. We believe fine-tuning could help address this challenge. Fourth, we observed that the performance of LEMUR may vary depending the LLM oracle. For example, our experiments demonstrate that GPT-4 is superior to GPT-3.5 turbo on tested benchmarks. Finally, due to the limitations of L.Mss and automated reasoners, framework does not yet offer significant boost for complex properties of real-world C libraries. However, a modular approach, where large parts of the program are abstracted and summarized in the form of pre- and post-conditions, can benefit from frameworks like LEMUR.

---

Published as a conference paper at ICLR 2024
REFERENCES
Dirk Beyer. Competition on software verification and witness validation: Sv-comp 2023, In Sriram Sankaranarayanan and Natasha Sharygina (eds.), Tools and Algorithms for the Construction and Analysis of Systems, pp. 495-522, Cham, 2023. Springer Nature Switzerland. ISBN 978-3-031
30820-8.
Yiannis Charalambous, Norbert Tihanyi, Ridhi Jain, Youcheng Sun, Mohamed Amine Ferrag, and Lucas C. Cordeiro. A new in software security: Towards self-healing software via large language models and formal verification, 2023.
Mark Chen, Jerry Tworck, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavar- ian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plap- pert, Fotios Chantzis, Elizabeth Barnes, Ariel Horbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji. Shantanu Jain, William Saunders. Christopher Hesse, Andrew N. Car,, Jan Leike. Joshua Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Pe- ter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojeiech Zaremba. Evaluating large language models trained code. CoRR, abs/2107.03374, 2021. URL https:://////. /ttt://rxxii /arxiv..ivv.. org/ abss/bb1// 03374.
Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem, et al. Handbook of model checking, volume 10. Springer, 2018.
Mikhail R Gadelha, Felipe R Monteiro, Jeremy Morse, Lucas C Cordeiro, Bernd Fischer, and De- nis Nicole. Esbme 5.0: an industrial-strength model checker. In Proceedings of the 33rd ACM/IEE International Conference on Automated Software Engineering, pp. 888-891, 2018.
Inc. GitHub. GitHub Copilot. https::/copplcer http://coopo..t.........moo///// com/ Accessed: September 2023.
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lin- denmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. Ultimate automizer with smtinterpol: (competition contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 641-643 Springer, 2013.
Daniel Kroening and Michael Tautschnig. Cbmc-c bounded model checker: (competition contribu- tion). In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Prac- tice of Software, ETAPS 2014, Grenoble, France, 5-13, 2014. Proceedings 20, pp. 389-391. Springer, 2014.
OpenAl. Gpt-4 technical report, 2023.
Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (eds.), Proceedings of the 40th International Conference on Machine Learning, volume 202 of Proceedings of Machine Learning Research, pp.
PMLR, 23-29 Jul 2023. URL https: http:////cccc/eceeeee/ee mmr. press/v202 http/eee233a html.
Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2inv: deep learning frame- work for program verification. In Shuvendu K. Lahiri and Chao Wang (eds.), Computer Aided Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I1, volume 12225 of Lecture Notes in Computer Science, pp. 151-164. Springer, 2020. doi:
00177788---00-329999 9. URL https: ///////doo/// meriiorg//00
778-3-030-5329
10

---

Published as a conference paper at ICLR 2024
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoe V Le, Denny Zhou, et al. ohain-of-thought prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems, 35:24824-24855 2022.
Martin White, Michele Tufano, Matias Martinez, Martin Monperrus, and Denys Poshyvanyk. Sort- ing and transforming program repair ingredients via deep learning code similarities. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, feb 2019. doi: 10.1 200.1009/aaeer221..86888/000 2asaner. 2019. 8668433
URL https://dci. wtw.eei.....oooooooe 1tt.///.1..../11111111....
Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating large language models in automated program verification. arXiv preprint arXiv:2310.04877 2023.


Reviews:
[{"review_id": "r1KgNecjeF", "reviewer": "Reviewer_2ahy", "summary": "This paper presents an interesting way to use LLMs and automated program verification tools synergistically to prove properties of programs that may otherwise be difficult to prove by the verification tools themselves.  The core idea consists of using an LLM to generate potential assumptions that may help an automated program verifier discharge the proof goal.  Once such assumptions are found, the effort of the program verification tool is directed to proving the assumptions themselves.  The authors present a set of sound rules to transform \"configurations\" of the proof process involving LLM calls and program verifier calls.  The authors also present some heuristics for LLM prompt generation, and for deciding how to prioritize multiples responses that may be provided by the LLM.  Finally, the authors present experimental results that show the promise of the proposed technique vis-a-vis state of the art program verification tools.", "questions": "1.  What actual value does the set of rules provide to this work?  Wouldn't it have sufficed to have Algorithm 1 directly, along with an explanation of the steps?\n2.  SV-COMP contains many, many more benchmarks.  How does LEMUR compare with UAutomizer or other tools on the other benchmarks?  Why are so few benchmarks chosen for comparison?\n3.  For what kinds of <program, property> combinations do LLMs fare badly as far as suggesting assumptions is concerned?  In some sense, this ought to depend on what kinds of data it has been trained on.   I didn't see any discussion in this regard -- I would tend to think that there are <program, property> combinations for which LLMs will have a very difficult time generating good assumptions.\n4. An LLM like GPT-4 makes use of immense computational power at the server end to come up with proposals/suggestions fast.  How do you propose to factor this in your comparisons for an apples-to-apples comparison.  Neither ESBMC not UAutomizer were provided access to such computational power; so how is the comparison fair?\n5. What are the assumptions on the training of the LLM that are being used?  Will the proposed method work with one's privately trained LLM?", "limitations": "", "rating": 5, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 2, "strengths": "The paper is clearly written, modulo some typos.  This helps in taking the reader along with the flow of the presentation.  The core ideas are illustrated with a running example -- this helped me follow the ideas without much difficulty. The idea of using an LLM to propose assumptions that can then be used to simplify a verification task is promising and the experiments demonstrate this.  Being able to out-perform the winning entries in SV-COMP is a significant achievement, and I believe this sufficiently demonstrates the promise of the approach.", "weaknesses": "The set of rules formulated by the authors doesn't add much value to the paper.  Algorithm 1 could itself have been presented directly, with explanations for the different steps.  In my opinion, the rules are kind of a force-fit to the paper.\nIt is good that the authors try to show that the proof rules are sound; however the soundness proofs are simple and not very insightful.  Indeed, finding a sound set of rules for simplifying/decomposing program verification is often not the difficult part of the process.  The more technically challenging part is to have completeness results for some subclass of programs/properties.  Unfortunately, the authors don't even try to do this.\nSince there are practical limits to prompt lengths for an LLM like GPT or GPT-4, this sets limits to how large a program can be verified using the proposed technique.  This is highly undesirable.  It would have been better if the authors attempted decomposition of the problem (perhaps guided by an LLM) and then applied the proposed technique to each decomposed part, and then stitched the results back together.  Unfortunately, the authors completely avoid any such attempt/discussion.\nSV-COMP has several tracks for verification.  The total count of programs in SV-COMP is significantly larger than that reported by the authors. It is not clear whether some cherry-picking was done in selecting the examples.\nAn LLM like GPT-4 makes use of immense computational power at the server end to come up with proposals/suggestions quickly.  It is not fair to discount this computational effort completely when comparing with the performance of other solvers that do not make LLM calls.  As a consequence, I believe the time comparison is not fair.\nA method like the one proposed, without any considerations of how the LLM is trained, may give dramatically different results based on what LLM is being used.  Therefore, a discussion on training the LLM should have been included.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "R9iz9PBTtx", "reviewer": "Reviewer_YmWA", "summary": "The paper describes a system for program verification that queries CHATGp4 for axioms.\nThe idea is interesting and the results excellent,  \nThe main problem of the paper is that it is written in a way that is much more suitable fior a CAV venue  than fior ICLR. The authors carefully and fomally describe the program  analysis framework, but they take a loose approach about GPt", "questions": "A small point: there is another lemur system in LLMs\n\n\"An important research question is whether modern AI models are capable of understanding .\" .. indeed, but can you claim you do that?\n\nAre you the first to ask LLMs to propose sub-goals?\n\nI'd much prefer a better survey that would make your contributions clear, and a graphical descriotion of the system that would allow me to position the different componrrntd\n\nI understand the process is fully automated?\n\n \"  -Finally, if the verifier V proves that the original property is not an invariant\" -> is the verifier cmplete?\n\nArguabythe prompts are what makes everything else worthwhile. Yet, they are in appendix?", "limitations": "", "rating": 5, "confidence": 3, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "The main strength of the paper are the results in Section 5\\\n\n.", "weaknesses": "Presentation\n\nOnly good results are shown? How likely is the fail case? ChatGPT seems a magic box, Above al, the way you present your work makes it unnecessarily hard to understand ypur ideas.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "jcLqjgbfJm", "reviewer": "Reviewer_ERFy", "summary": "This paper proposes an approach to reachability verification, dubbed Lemur, which combines the invariance generation capabilities of LLMs with standard verification tools. The resulting procedure, which is sound albeit incomplete, comes with theoretical guarantees.\nLemur equipped with GPT4 can solve benchmarks that are currently out of reach of state-of-the-art standard reachability verification tools.", "questions": "- How much is Lemur performance reliant on the invariant generator quality?\n- How does Lemur fare without GPT4 as an invariant generator? \n- Can Lemur be used with non-LLM invariant generators such as Code2Inv?\n\n--------\nMinors:\n\nThe derivation rules in Fig.1 are not 100% clear to me. What is the semantic of operator \": :\"?\n\nFigures 3 and 4 should have different (and self-explanatory) captions, i.e. explicitly mention the referred benchmarks.", "limitations": "", "rating": 5, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "- Clear presentation\n- Reachability is a pivotal problem in program verification\n- Promising preliminary results\n- (To the best of my understanding) Lemur's calculus and template algorithm can accomodate different combinations of invariant generators and verifiers", "weaknesses": "My main concerns are related to the empirical evaluation of Lemur. \nThe combination of LLMs and standard verification procedures is indeed promising, but I am left wondering how much the results are reliant on the specific LLM GPT4. \n\nThis is particularly important considering the economic cost of reproducing the experiment, which can be prohibitive for some.\n\nIf I understand correctly, Lemur is a template algorithm. I would then expect to see results for LEMUR(X, Y), where X = {GPT4, other free LLMs, other invariant generation techniques (Code2INV maybe?), and Y = {UAUTOMIZER, ESBMC}.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SGybkF6N0J", "reviewer": "Reviewer_mzY5", "summary": "The paper presents a principled approach for combining LLMs with automated reasoning tools to perform automated program verification. Automated program verification typically proceeds by breaking down the overall proof goal into simpler proof sub-goals---each sub-goal establishes some invariant of the program which can help in proving/disproving the overall program assertion. The proposed technique uses LLMs to suggest candidate invariants as proof sub-goals; whether the suggested invariants hold or not is posed as a query to existing automated program reasoning tools. While the general paradigm of guessing and then checking invariants is well-known in the program verification literature, the paper presents a proof calculus that cleanly formalizes this style of reasoning and develops an algorithm based on this calculus. The calculus is proven sound and the algorithm is shown to be terminating under suitable conditions. Most importantly, the presented algorithm outperforms state-of-the-art automated program verification tools on standard benchmarks.", "questions": "1. For the benchmark of difficult programs from SV-COMP, where are the placeholder lines added? Is it after every line in the program? If not, doesn't the location of the placeholder leak information, potentially aiding Lemur?\n\n2. It seems like the text and the formal expression for the second bullet point of Proposition 2.1 do not line up. Shouldn't the implication in the formal expression go the other way?\n\n3. I don't think the last line on Page 2 is correct. A program without loops can have an unstable property because the program can still have multiple paths due to branches. Also, how can a property that is not an invariant be stable? Is this the case where stability is due to the property always being false?\n\n4. Is the time in Table 1 in seconds? When you say timeout of 1 hr or 10 minutes, is that the timeout for the entire dataset or each program?\n\n5. Does each bar in Figure 4 correspond to a single value for the number of proposals or a set of values? It seems like it is the latter case. It would help to clarify the figure.", "limitations": "", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "1. This is a very well-written paper and presents a nice, clean formalization of the guess-and-check style of program reasoning via the Lemur calculus.\n\n2. The algorithm that operationalizes the calculus is elegant and easy to understand.\n\n3. Use of LLMs to suggest candidate program invariants is an obvious idea but it has been very well manifested into practice, both mathematically and algorithmically,  by this work.\n\n4. Some of the prompting tricks used to get the invariants from the LLM, such as placeholder lines, are interesting in their own right.\n\n5. Most importantly, the empirical results are very promising and suggest that LLMs and verification tools can be fruitfully combined.", "weaknesses": "1. This is a relatively minor comment but the formalization and the algorithm seem geared towards imperative languages where the notion of associating a property/invariant with a line number makes natural sense. It would be helpful to acknowledge that the proposed calculus might not necessarily be applicable to all programming languages.\n\n2. There has a large body of literature on data-driven techniques for learning loop invariants [1,2]. Unlike Code2Inv and Lemur, these past works use dynamic values of loop variables. Adding references to this body of work would help paint a fuller picture about this area.\n\n[1] Garg, P., Neider, D., Madhusudan, P., & Roth, D. (2016). Learning invariants using decision trees and implication counterexamples. ACM Sigplan Notices, 51(1), 499-512.\n\n[2] Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., & Nori, A. V. (2013). A data driven approach for algebraic loop invariants. In Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 22 (pp. 574-592). Springer Berlin Heidelberg.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)