Compositional Loop Invariant Inference for Multiphase Programs via Structured Neurosymbolic Reasoning

AUTHOR MANUSCRIPT

1

Compositional Loop Invariant Inference for Multiphase Programs via Structured Neurosymbolic Reasoning

arXiv:2611.07882v1 [cs.SE] 5 Nov 2026

Mingxiu Wang, Jiawei Wang, Shuangxiang Kan, Angela Huo, Yuekang Li, Xi Zheng, and Xiao Cheng* Abstract—Loop invariants are essential for deductive program verification, yet automatically inferring them for multiphase programs, whose loops contain conditional branches that induce multiple execution phases with distinct behaviors, remains an open problem. Existing LLM-based methods either reason about loops as a whole or use explicit branch information to generate atomic assertions jointly across branches, without maintaining complete candidate sub-invariants for independent generation and targeted repair. We present C LOVER, a structured neurosymbolic reasoning framework for multiphase invariant inference built on two interlinked mechanisms. First, compositional inference: C LOVER statically decomposes a loop into symbolic loop branch sequences, conjunctions of the loop guard and branch conditions that characterize distinct execution scenarios, and guides the LLM to generate candidate sub-invariants for each one independently, so that each LLM query focuses on a single execution scenario rather than the entire loop. Second, counterexample-guided localized refinement: when SMT verification rejects a composed disjunctive invariant, C LOVER traces the counterexample back through the branch structure to identify which specific loop branch sequence caused the failure and repairs only that sub-invariant, preserving all correct components. Both mechanisms are unified by a shared symbolic structure derived from the loop’s branch semantics, which guides what the LLM generates, how candidates are composed, and where refinement is directed. We evaluate C LOVER on 316 linear arithmetic, 50 nonlinear arithmetic, and 54 multiphase benchmarks. C LOVER solves 35 of 54 multiphase benchmarks, outperforming the best LLM-based baseline (29) by 20.7% and the best traditional method (22) by 59.1%. On linear/nonlinear benchmarks, C LOVER remains competitive, solving 355 of 366 programs overall. Index Terms—Loop invariant inference, program verification, multiphase programs, large language models, neurosymbolic reasoning.

✦

1

I NTRODUCTION

Loop invariants [1], [2] are central to deductive program verification [3], enabling formal reasoning about loop correctness via Hoare logic [4]. Large language models (LLMs) have recently emerged as a promising approach to automatic invariant inference, overcoming the scalability limitations of traditional symbolic methods [5], [6], [7], [8], [9], [10] and the generalization difficulties of earlier learningbased methods [11], [12], [13], [14]. Recent LLM-based approaches [15], [16], [17], [18] follow a guess-and-check paradigm: the LLM guesses candidate invariants or clauses, an SMT solver checks them, and counterexample feedback guides the next round of guessing. These methods show good performance on standard linear/non-linear benchmarks. However, real-world loops often contain conditional branches that cause different iterations to follow different execution paths, each updating variables in its own way. Such programs are called multiphase programs [19] and arise naturally whenever loop variables cross domain boundaries •

M. Wang, X. Zheng, and X. Cheng are with Macquarie University, Sydney, NSW, Australia. E-mail: mingxiu.wang@students.mq.edu.au, xiao.cheng@mq.edu.au, james.zheng@mq.edu.au. • J. Wang and Y. Li are with the University of New South Wales, Sydney, Australia. E-mail: jiawei.wang6@unsw.edu.au, yuekang.li@unsw.edu.au. • S. Kan is with Singapore Management University, Singapore. E-mail: shuangxiangkan@outlook.com. • A. Huo is with the University of Technology Sydney, Sydney, Australia. E-mail: huan.huo@uts.edu.au. * Corresponding author: Xiao Cheng (e-mail: xiao.cheng@mq.edu.au).

that activate different branches (e.g., a loop that increments a counter i and executes one branch while i < n but switches to another once i ≥ n, so that the invariant must capture both phases). Generating correct invariants for multiphase programs is a recognized challenge [20], [21]: the correct invariant is inherently a disjunction of phase-specific invariants, one per execution phase, whose complexity grows combinatorially with the number of branches. Despite longstanding interest, multiphase programs expose a critical blind spot in current LLM-based loop invariant inference techniques. Many LLM-based methods struggle on multiphase loops because they are blind to the structure of the guess space: in a multiphase loop, the program’s branch structure induces a natural decomposition of the guess space into separate dimensions, one per execution phase, and the correct invariant is a disjunction of phase-specific clauses, one drawn from each dimension. These methods ignore this structure and collapse the multi-dimensional guess space into a flat, unstructured one, prompting the LLM with the entire program and producing candidates without distinguishing which dimension each belongs to. The resulting clauses are then combined without branch awareness: LaM4Inv [15] combines clauses exclusively via conjunction, unable to represent disjunctive invariants, while Clause2Inv [16] enumerates both conjunctions and disjunctions, causing the candidate pool to grow exponentially with the number of phases. When verification fails, the counterexample feedback is exploited only coarsely at program level, unable to localize

AUTHOR MANUSCRIPT

which phase dimension caused the failure. Even approaches that improve feedback quality, such as LORIS [18], which detects local reasoning errors in the LLM’s proof steps, still operate on the loop as a whole and cannot attribute failures to specific phases. PAL2Inv [22] is a recent path-sensitive exception. It applies abstract interpretation to obtain initial invariants, prompts an LLM to generate atomic assertions for every enumerated loop path, and uses counterexample-guided clause combination to assemble disjunctions of path-level conjunctions. This design makes path information explicit, but its generation step still asks the LLM to reason about all paths in one request, and its search state consists of path-indexed pools of atomic clauses rather than multiple alternative, complete sub-invariants for each path. Refinement therefore enriches and recombines clause pools instead of maintaining competing global compositions in which one selected phase component can be replaced while all other choices remain fixed. Thus, path sensitivity alone does not eliminate the simultaneous-reasoning and candidatecomposition burdens of multiphase invariant inference. These failures point to two core challenges. First, the LLM must reason about all phases simultaneously, yet the joint reasoning complexity overwhelms its capacity and the resulting candidate space grows combinatorially. Second, when verification fails, whole-loop feedback is too coarse to identify which phase is responsible, wasting repair effort on phases that are already correct. Our key insight is that the branch structure of a multiphase loop enables two interlinked mechanisms that address both challenges. First, compositional inference: the distinct branch-condition combinations decompose the invariant synthesis task so that the LLM generates sub-invariants for each combination independently, reducing per-step reasoning complexity from the full loop to a single execution scenario. This decomposition also naturally admits multiple candidates per combination, providing candidate diversity that prevents premature commitment. Second, counterexample-guided localized refinement: because these combinations partition the state space, any counterexample can be uniquely mapped to the responsible combination, so the framework repairs only the failed phase’s sub-invariant while preserving all other phases. We realize this architecture in C LOVER, a framework that tightly integrates neural generation and symbolic verification through a shared symbolic structure derived from the program’s branch semantics. C LOVER statically analyzes the loop’s control flow to extract loop branch sequences, distinct combinations of branch conditions that partition the loop’s execution space. This symbolic structure guides LLM reasoning at every stage: it determines what the LLM generates (one sub-invariant per loop branch sequence), how candidates are composed (root-to-leaf disjunctions), and where refinement is directed (the specific loop branch sequence that caused the failure). Through this structure, the framework realizes both contributions. For compositional inference, each loop branch sequence becomes a level in a search tree, and the LLM generates multiple candidate sub-invariants for each level independently, maintaining candidate diversity across levels. For localized refinement, when the solver rejects a composed invariant, C LOVER traces the counterexample back through the loop branch

2

sequence partition to identify the responsible loop branch sequence and restricts repair to that loop branch sequence alone, preserving all other sub-invariants. We implement C LOVER and evaluate its performance on three benchmark datasets: 316 linear arithmetic benchmarks, 50 nonlinear arithmetic benchmarks, and 54 multiphase benchmarks. The first two categories are widely used in prior work and serve as standard evaluation sets for state-of-the-art invariant synthesis tools. The multiphase benchmarks are drawn from the CHC-COMP repository [23], which provides realistic, publicly available verification tasks for inductive invariant inference and safety checking, ensuring fair and representative evaluation [24]. We compare C LOVER against state-of-the-art LLM-based tools (LaM4Inv [15], Clause2Inv [16], LORIS [18], and PAL2Inv [22]), representative learning-based approaches (Code2Inv [14], CLN2INV [25], and LIPuS [26]), and traditional methods, including the multiphase invariant synthesizer ImplCheck [19], the CHC solver Eldarica [6], and the software model checkers CPAchecker [27] and UAutomizer [28], demonstrating its effectiveness across both standard and challenging benchmark settings. Our contributions are summarized as follows: • We identify limitations in current LLM-based loop invariant inference methods [15], [16], [18], [22] when applied to multiphase programs: most use whole-loop generation and composition, while even path-sensitive methods do not retain complete local alternatives that support counterexample-guided replacement of one selected loop branch sequence’s sub-invariant. • We propose C LOVER , a framework built on two interlinked mechanisms: compositional inference, which decomposes invariant synthesis along loop branch sequences so that the LLM reasons about one execution scenario at a time, and counterexample-guided localized refinement, which traces SMT counterexamples through the loop branch sequence partition to identify and repair only the failed sub-invariant while preserving all correct components. • We evaluate C LOVER on 316 linear arithmetic, 50 nonlinear arithmetic, and 54 multiphase benchmarks, demonstrating competitive loop invariant synthesis performance on linear/non-linear benchmarks and substantial loop invariant synthesis improvements on multiphase programs over both LLM-based methods, learning-based baselines and traditional verification engines.

2

BACKGROUND

This section introduces the concept of loop invariants and the principles for verifying their correctness. A loop invariant is a logical assertion I that characterizes a property holding throughout the execution of a loop. Consider a program of the form { P } while B do S { Q }, where P denotes the precondition, B the loop guard, S the loop body, and Q the postcondition. Proving the correctness of such a loop amounts to finding an invariant I that satisfies the following proof rule:

P ⇒I

{ I ∧ B } S { I } (I ∧ ¬B) ⇒ Q { P } while B do S { Q }

AUTHOR MANUSCRIPT

int main() { int x, y, w, z; 3 x = 0; w = 0; 4 assume(y > z); 1 2

5

while (unknown()) { if (x < z) { // ϕ1 : unknown() ∧ x < z w = w + 1; x = x + 1; } else { // ϕ2 : unknown() ∧ x ≥ z w = w - 2; x = x + 1; } } if (x > y + z) { // ϕ3 : ¬unknown() (exit) assert(w <= 0); }

6 7 8 9 10 11 12 13 14 15 16 17 18

}

Fig. 1. A multiphase loop with three loop branch sequences. Each loop branch sequence ϕi corresponds to a distinct combination of the loop guard and branch conditions, highlighted in blue (ϕ1 ), red (ϕ2 ), and green (ϕ3 ).

The three premises correspond to three verification conditions. Initiation (P ⇒ I ) requires the invariant to hold upon loop entry. Preservation ({I ∧ B} S {I}) requires each iteration to preserve the invariant. Termination ((I ∧ ¬B) ⇒ Q) requires the invariant, together with loop termination, to establish the postcondition. While checking these conditions is decidable for many theories via SMT solvers, synthesizing a suitable invariant I remains a key challenge, particularly for loops whose bodies contain conditional branches that give rise to distinct execution phases.

3

M OTIVATING E XAMPLE

In this section, we present a motivating example to illustrate the limitations of current LLM-based loop invariant generation methods and how our framework addresses these challenges. Figure 1 presents a C program containing a multiphase loop. The loop body exhibits three distinct execution scenarios, each characterized by a specific combination of the loop guard and branch conditions, highlighted with colored backgrounds. We call each such combination a loop branch sequence (formally defined in Definition 1) and note that a single loop branch sequence may span multiple program phases. This loop has three loop branch sequences: unknown() ∧ x < z , unknown() ∧ x ≥ z , and ¬unknown() (exit). In the loop branch sequence unknown() ∧ x < z , a loop invariant is relatively easy to identify: x < z ∧ z > 0 ∧ w ≥ 0. However, in the loop branch sequence unknown() ∧ x ≥ z , the invariant becomes more complex due to two distinct entry conditions, namely z > 0 and z ≤ 0. When z > 0, a valid invariant is: x ≥ z ∧ y > z ∧ w + 2x = 3z. When z ≤ 0, the corresponding invariant is: x ≥ z ∧ y > z ∧ w + 2x = 0. Consequently, the overall loop invariant must account for both phases, yielding the following disjunctive invariant: (x < z ∧ z > 0 ∧ w ≥ 0) ∨ x ≥ z ∧ y

> z ∧ (z > 0 ∧ w + 2x = 3z) ∨ (z ≤ 0 ∧ w + 2x = 0) .

3

Existing efforts and limitations. We illustrate the limitations of existing LLM-based methods by tracing how four representative tools handle this example. LaM4Inv [15] generates candidate invariants for the entire program, decomposes them into clauses such as w ≥ 0, x ≥ 0, y > z , and weak disjunctive terms like (x = 0 ∧ w = 0) ∨ (x > 0), and verifies each for Initiation and Preservation. Verified clauses are collected and used to check Termination. Because all clauses are generated at the program level, the tool cannot capture phase-specific properties and relies on global terms that are too coarsegrained for branch-specific relationships. LaM4Inv therefore fails on this multiphase program. Clause2Inv [16] also generates clauses from the full program and combines them via conjunction (∧) and disjunction (∨), using counterexamples to prune unsatisfied candidates. However, this pruning can discard partially correct candidates: a clause such as (x < z ∧ z > 0 ∧ w ≥ 0), valid within the x < z phase, may be eliminated because it does not satisfy the counterexample globally. Clause2Inv therefore does not succeed on this example. LORIS [18] refines a single candidate using feedback on the LLM’s own reasoning: failed verification conditions are translated into first-order implications and checked by an SMT solver, with invalid implications fed back as hints. On this example, a monolithic guess such as w = x is preserved in ϕ1 but violated in ϕ2 , and the feedback correctly reports the failure. However, this flags only a local error within one global candidate and never suggests partitioning the state into (x ≤ z ∧ w = x) ∨ (x ≥ z ∧ w = 3z − 2x). Because a missing disjunct is a structural rather than a local error, LORIS fails on this example. PAL2Inv [22] explicitly enumerates loop paths and associates atomic assertions with each path, but two difficulties remain. First, it generates assertions for all paths in one response and excludes logical connectives from each assertion, leaving the symbolic combinator to recover the required structure. For the x ≥ z loop branch sequence, the combinator must pair each equality with its corresponding guard and construct (z > 0 ∧ w + 2x = 3z) ∨ (z ≤ 0 ∧ w + 2x = 0). Path labels distinguish x < z from x ≥ z , but do not determine this internal grouping: disjoining the equalities without guards admits spurious states, while conjoining the guarded alternatives is unsatisfiable. Second, a failed global candidate triggers further clause generation or recombination, without localizing the failure to one loop branch sequence for replacement of its complete sub-invariant. A failure involving x ≥ z should direct repair to its guarded equalities while preserving the selected x < z candidate. PAL2Inv can express the required invariant in principle, but path-indexed atomic assertions alone do not provide independently replaceable, complete local candidates, leaving both their logical composition and targeted repair to be resolved. Our solution. Our framework tackles this example by first decomposing the loop into three loop branch sequences based on its branch structure: ¬unknown() (exit), unknown() ∧ x < z , and unknown() ∧ x ≥ z . The LLM is then prompted to generate candidates for each loop branch sequence independently. This scoped prompting focuses the LLM on one execution phase at a time: when reasoning

AUTHOR MANUSCRIPT

about the x ≥ z loop branch sequence, it only needs to consider how w and x evolve under x ≥ z , rather than simultaneously reasoning about all branches. However, committing to a single candidate per loop branch sequence would be fragile: the correctness of each candidate depends on its combination with candidates from other loop branch sequences, and a wrong early choice has no fallback. We therefore generate multiple candidates per loop branch sequence and organize them as a search tree, where each loop branch sequence corresponds to a level and each root-to-leaf path assembles one complete disjunctive invariant. For example, for the exit loop branch sequence the LLM might produce x ≥ z ∧ w ≤ 0 and w + x ≤ z , while for unknown() ∧ x ≥ z , it might produce x ≥ z ∧ y > z ∧ w = −2(x − z) and x ≥ z ∧ y > z ∧ w + 2x ≤ 3z . Consider the path that selects:

4

{p1 , . . . , pn }. Each maximal control-flow path through the loop body evaluates a subset of k predicates {pi1 , . . . , pik } ⊆ P , where 1 ≤ i1 < · · · < ik ≤ n are the indices of the predicates encountered along that path. A loop branch sequence is the conjunction of B with the (possibly negated) predicates along such a path: ϕ ≜ B ∧ li1 ∧ · · · ∧ lik , where each lij ∈ {pij , ¬pij } for j = 1, . . . , k . The formula ¬B defines the exit case. The set Φ of all loop branch sequences together with ¬B partitions the loop’s execution space: for any state, exactly one element of Φ holds. Example 1. Consider a loop while (B) { if (P) { if (Q) S1; else S2; } else { S3; } S4; }. Here P = {P, Q}, yielding four loop branch sequences: ϕ1 = B ∧ P ∧ Q, ϕ2 = B ∧ P ∧ ¬Q, ϕ3 = B ∧ ¬P , ϕ4 = ¬B . Note that ϕ3 does not involve Q, since the path through ¬P never evaluates it.

exit → x ≥ z ∧ w ≤ 0,

unknown() ∧ x < z → y > z ∧ x ≤ z ∧ w = x, unknown() ∧ x ≥ z → x ≥ z ∧ y > z ∧ w = −2(x − z). Their disjunction: (x ≥ z ∧ w ≤ 0) ∨ (y > z ∧ x ≤ z ∧ w = x) ∨ (x ≥ z ∧ y > z ∧ w = −2(x − z)) is sent to the SMT solver, which returns counterexample (y = 4, z = 3, x = 3, w = 3). Unlike the methods above, our framework does not discard everything. Instead, it performs counterexample-guided localized refinement. Since the loop branch sequences partition the state space, the counterexample (x = 3, z = 3) uniquely maps to the unknown() ∧ x ≥ z loop branch sequence, and evaluating SI 3 under this valuation reveals that w = −2(x − z) is the specific violated clause (w = 3 ̸= 0). We then refine only this loop branch sequence’s candidate, while preserving the already-correct candidates for exit and x < z . This phase-targeted repair is infeasible for prior methods, which operate at the whole-loop level and cannot attribute failures to specific loop branch sequences. After four refinement iterations, the corrected invariant for this loop branch sequence becomes:

y > z ∧ x ≥ z ∧ w = 3z − 2x ∧ x ≤ y + z + 1. Combining all candidates yields the final invariant: (x ≥ z ∧ w ≤ 0) ∨ (y > z ∧ x ≤ z ∧ w = x) ∨ (y > z ∧ x ≤ z ∧ w = x ∧ x ≤ y + z + 1) ∨ (y > z ∧ x ≥ z ∧ w = 3z −2x∧x ≤ y +z +1). Although this invariant differs from the manually derived one and contains a redundant disjunct (the third is subsumed by the second), it is valid: it correctly captures the necessary conditions across all execution paths. Had the first tree path failed entirely, the framework could have backtracked to an alternative candidate (e.g., w + 2x ≤ 3z ) rather than restarting the whole process.

4

A PPROACH

We first introduce the concept of a loop branch sequence, which is the key abstraction underlying our compositional invariant synthesis approach. We then present an overview of the C LOVER framework, followed by detailed descriptions of its components. Definition 1 (Loop Branch Sequence). Let a loop have guard B whose body contains branch predicates P =

4.1

Overview

Figure 2 presents the overall workflow of C LOVER, which consists of four steps: Step 1: Loop Branch Sequence Extraction (§4.2). We parse the input program to construct its control-flow graph (CFG), from which we identify loop structures and extract loop branch sequences. These loop branch sequences decompose the loop’s execution space into disjoint branches, enabling subsequent steps to reason about each branch independently rather than treating the loop as a monolithic whole. Step 2: Compositional Loop Invariant Synthesis (§4.3). Rather than asking the LLM to produce a complete invariant in one step, we perform compositional inference: each loop branch sequence becomes a level in a symbolic search tree, and the LLM generates multiple candidate sub-invariants for each level independently, so that each query focuses on a single execution scenario. The tree naturally maintains a diverse pool of partial solutions that enables the localized refinement in Step 4. Step 3: Loop Invariant Verification (§4.4.1). Complete invariant candidates are formed by composing root-to-leaf paths via disjunction (∨) and verified with an SMT solver. If any candidate satisfies all verification conditions, it is returned as the final invariant. Step 4: Counterexample-Guided Localized Refinement (§4.4.2). When verification fails, we trace the counterexample through the loop branch sequence partition to identify the specific loop branch sequence responsible for the failure, then refine only that loop branch sequence’s sub-invariant while preserving the sub-invariants of all other loop branch sequences. Prior methods operate at the whole-loop level and cannot attribute failures to specific phases, so they lack this phase-targeted repair capability. This targeted refinement loop repeats until a valid invariant is found or the time budget is exhausted. 4.2

Loop Branch Sequences Extraction

Given the CFG of a program, we first identify loop structures and extract the loop guard B . We then enumerate all feasible loop branch sequences via the algorithm in Figure 3, which performs a depth-first traversal of the CFG starting from the loop body entry.

AUTHOR MANUSCRIPT

5

Step 1: Loop Branch Seq Extraction Source

Step 2: Tree-Structured Compositional Loop Inv Synthesis

Best Path

Construct Prompt

CFG

Branch Enum ...

Input

LLM

Program Query

Task Description

(Failed ...

... ...

)

Synthesize

... ...

... ... ... ...

... ...

Refine

(CounterExample) Success

...

Candidate Invariant ....

N

CE Locate Counter Example

Y Select Best Path

Step 4: Localization & Refinement

If sat

SMT Check

Step 3: Loop Invariant Verification

Fig. 2. Overview of the C LOVER framework.

Require: Loop header v0 with guard B , CFG G Ensure: Set of loop branch sequences Φ 1: Φ ← ∅ 2: procedure C OLLECT(v, guards ) 3: if v = v0 then 4: Φ ← Φ ∪ {guards}; return 5: else if v is a nested loop header then 6: C OLLECT(v.exit, guards ) 7: else if v is a conditional with predicate p then 8: C OLLECT(vtrue , guards ∪ {p}) 9: C OLLECT(vfalse , guards ∪ {¬p}) 10: else 11: C OLLECT(v.next, guards ) 12: end if 13: end procedure 14: C OLLECT(body(v0 ), {B}) 15: Φ ← Φ ∪ {¬B} 16: return Φ Fig. 3. DFS-based loop branch sequence collection algorithm.

At each conditional node with predicate p ∈ P , the traversal forks into two branches, appending p or ¬p to the current guard list respectively. When the traversal reaches a back-edge to the loop header v0 , the accumulated guards form a complete loop branch sequence ϕ = B ∧ li1 ∧ · · · ∧ lik (Definition 1). Nested loops are treated as atomic blocks by jumping directly to their exit nodes, since their internal branches do not contribute to the outer loop’s loop branch sequences. Finally, the exit case ¬B is added as a separate loop branch sequence to ensure the invariant covers loopskipping executions. The resulting set Φ partitions the loop’s execution space, so that any program state, and in particular any counterexample returned during refinement, can be uniquely mapped to a specific loop branch sequence. Figure 4 presents the complete algorithm for our compositional loop invariant synthesis and refinement. Steps 2– 4 correspond to synthesis, verification, and refinement, re-

Require: loop branch sequences Φ = {ϕ1 , ϕ2 , . . . , ϕD }, program x, beam width k , timeout T Ensure: Valid loop invariant I or T IMEOUT 1: Y ← {[ ]} ▷ Partial paths 2: for i = 1 to D do ▷ Step 2: Synthesis 3: Pi ← G ENERATE(x, ϕi ) ▷ n candidates for ϕi 4: Y ′ ← E XPAND(Y, Pi ) ▷ Extend paths 5: V ← S CORE(x, Y ′ ) ▷ LLM scores paths 6: Y ← T OP K(Y ′ , V, k) ▷ Beam: keep top-k 7: end for 8: I ← V ERIFY(Y ) ▷ Step 3: Verify 9: if I ̸= N ONE then return I 10: end if 11: while ¬ T IMEOUT(T ) do ▷ Step 4: Refine 12: y ⋆ ← S ELECT B EST(Y ) 13: (σ, j, cond , BC ) ← D IAGNOSE(y ⋆ ) ▷ Localize CE 14: if I S A MBIGUOUS(j, cond ) then ▷ Cross-branch CE 15: j ← J UDGE B RANCH(x, σ, j) 16: end if 17: r ← R EFINE(x, y ⋆ , σ, j, cond , BC ) ▷ Refine SI j 18: Y ← U PDATE(Y, y ⋆ , j, r) 19: I ← V ERIFY(Y ) 20: if I ̸= N ONE then return I 21: end if 22: end while 23: return T IMEOUT Fig. 4. Compositional loop invariant synthesis and refinement algorithm.

spectively, each of which we describe below. 4.3 Tree-Structured Compositional Loop Invariant Synthesis This section details the synthesis phase of the algorithm in Figure 4 (Lines 2–7). Rather than generating a monolithic invariant in one step, we organize the synthesis as a treestructured symbolic search that decomposes the task along the loop branch sequences extracted in Step 1.

AUTHOR MANUSCRIPT

Tree structure. Let Φ = {ϕ1 , . . . , ϕD } be the set of loop branch sequences, where D = |Φ|. We formulate invariant generation as a tree search of depth D: the root represents the empty sequence y = (), and each level i corresponds to ϕi . A node at level i stores a partial path y = (SI 1 , . . . , SI i ), where SI j denotes the sub-invariant selected for ϕj (j ≤ i). When multiple candidates exist at each level, we write SI kj for the k -th candidate sub-invariant at level j . This tree encodes the combinatorial search over sub-invariant selections: branching at level i represents alternative sub-invariant proposals for ϕi , not alternative execution paths in the program. A root-to-leaf path assembles one complete disjunctive candidate by selecting exactly one proposal per loop branch sequence. Expansion and pruning. At level i, the LLM takes the program x and ϕi as input and generates n candidate subinvariants Pi = {SI 1i , . . . , SI n i } (G ENERATE in Figure 4). Each existing path in Y is extended with every candidate in Pi , yielding an expanded set Y ′ . To control combinatorial explosion, we score each extended path y ′ ∈ Y ′ via an LLMbased evaluation prompt (S CORE) that assesses four criteria: whether the sub-invariants along the path are mutually consistent, whether each imposes meaningful rather than vacuous constraints, whether the new sub-invariant matches the semantics of its loop branch sequence, and whether the accumulated path is likely to satisfy the proof obligations when composed via disjunction. The LLM returns a score for each path, and only the top-k paths are retained (T OP K), effectively applying beam search to bound the tree width. Synthesis prompt design. Given (x, ϕi ), the generation prompt instructs the LLM to produce sub-invariants that (1) hold whenever ϕi is active (Initialization), (2) are preserved across loop iterations even when execution transitions to another loop branch sequence (Preservation), and (3) together with ¬B imply the postcondition (Termination). Each candidate is a conjunction of predicates over program variables, where multiple conjunctive terms represent disjunctive cases when a single loop branch sequence admits distinct entry states. After D levels, each root-to-leaf path y = (SI 1 , . . . , SI D ) WD encodes a complete candidate invariant I = j=1 SI j . Beam search ensures that only the k most promising candidates survive at each level, keeping the search tractable while preserving the candidate diversity that the subsequent localized refinement (§4.4.2) relies upon. 4.4

Loop Invariant Verification and Refinement

4.4.1 Loop Invariant Verification As shown in Figure 4 (Line 8), each surviving path y = (SI 1 , . W . . , SI D ) ∈ Y is composed into a global candidate D I = j=1 SI j and checked against the three standard invariant proof obligations: Initialization, Preservation, and Termination using an SMT solver. This composition is sound because each SI j is implicitly guarded by its corresponding loop branch sequence ϕj . Since the loop branch sequences W form a partition of the state space, the disjunction j SI j represents a case split over mutually exclusive regions, rather than requiring each sub-invariant to hold globally. Specifically, the solver checks each candidate I against three conditions. Initiation (Init: P ⇒ I ) requires the pre-

6

condition to imply that at least one sub-invariant holds at loop entry. Preservation (Pres: {I ∧ B} S {I}) requires that if any SI j holds before an iteration, then some SI j ′ (possibly j ′ ̸= j ) holds afterward. This cross-branch condition is critical for multiphase loops, where a single iteration may transition from one loop branch sequence to another. Termination (Term: (I ∧ ¬B) ⇒ Q) requires that upon loop exit, the disjunction of sub-invariants together with the negated guard implies the postcondition. If any candidate satisfies all three conditions, it is returned as the valid invariant. Otherwise, for each failed candidate, the solver returns a counterexample σ and the violated condition, which are passed to the refinement phase. 4.4.2

Loop Invariant Refinement

This section details the refinement phase of the algorithm in Figure 4 (Lines 11–18). While the synthesis phase realizes compositional inference by decomposing generation along loop branch sequences, the refinement phase introduces the complementary mechanism of counterexample-guided localized refinement: it traces verification failures to a single loop branch sequence and repairs only that phase’s subinvariant while preserving those of all other phases. This phase-level repair capability is unavailable to whole-loop methods. Together, compositional inference and localized refinement are the two domain-specific contributions of C LOVER. The ablation study in Section 5.4 confirms that removing localization causes a 23% drop in solved benchmarks (from 35 to 27). Counterexample-guided localization. In each iteration, the most promising candidate y ⋆ = (SI 1 , . . . , SI D ) is selected (see S ELECT B EST below). The D IAGNOSE procedure invokes the SMT solver and returns a counterexample σ (a concrete variable valuation), the violated Hoare condition cond ∈ {Init, Pres, Term}, and a set of broken clauses BC . Because Φ partitions the state space (Definition 1), evaluating σ against the loop branch sequence guards uniquely identifies the responsible loop branch sequence ϕj . In the tree view, ϕj corresponds to level j of the path y ⋆ , and BC pinpoints which conjunctive predicates in SI j are violated under σ , providing fine-grained guidance for the LLM. Example 2. Returning to the motivating example (Section 3), suppose the synthesis phase produces a path with SI 1 = (x ≥ z ∧ w ≤ 0) for the exit loop branch sequence, SI 2 = (y > z ∧ x ≤ z ∧ w = x) for unknown() ∧ x < z , and SI 3 = (x ≥ z ∧y > z ∧w = −2(x−z)) for unknown()∧x ≥ z . The composed candidate I = SI 1 ∨ SI 2 ∨ SI 3 fails Term with counterexample σ = (y=4, z=3, x=3, w=3). Since σ satisfies unknown() ∧ x ≥ z , the failure is localized to ϕ3 . Evaluating each atomic predicate of SI 3 under σ : x ≥ z holds (3 ≥ 3), y > z holds (4 > 3), but w = −2(x − z) fails (3 ̸= 0). Hence BC = {w = −2(x − z)}, giving the LLM a precise target for repair. Localized refinement. The LLM is prompted to regenerate only SI j (R EFINE in Figure 4), receiving σ , BC , and the program context as input. The updated sub-invariant r replaces SI j in y ⋆ while all other levels remain unchanged (U PDATE). The modified candidate is then re-verified. This targeted, level-wise edit ensures that each refinement iter-

AUTHOR MANUSCRIPT

ation corrects exactly one sub-invariant without disturbing the rest. Ambiguity resolution (I S A MBIGUOUS, Line 14). For Init and Term failures, the counterexample σ is a single state, so evaluating σ against the loop branch sequence guards directly identifies the responsible loop branch sequence ϕj . For Pres failures, however, the counterexample is a pair (σpre , σpost ) representing the state before and after one loop iteration. If both states satisfy the same loop branch sequence guard, that loop branch sequence is selected. The ambiguity arises when they fall into different loop branch sequences: σpre ∈ ϕa and σpost ∈ ϕb with a ̸= b, representing a cross-branch transition. In this case, the failure may originate from either side: (1) σpre is spurious, i.e., not actually reachable during execution, meaning SI a is too weak and admits infeasible states, so the fix is to strengthen SI a . (2) σpre is genuine, i.e., the iteration legitimately transitions from ϕa to ϕb , but SI b fails to hold afterward. In this case, the fix is to repair SI b . Since reachability is undecidable in general, we use the LLM as an approximate oracle via J UDGE B RANCH: given the program, precondition, and σpre , the LLM traces concrete variable updates to judge whether σpre is reachable from the initial state. This is feasible because SMT-produced counterexamples typically involve small integer values reachable within a few iterations. If reachable, we refine ϕb , and otherwise ϕa . This judgment is approximate: the next verification round rejects an invalid refined invariant, while later LLM judgments and S E LECT B EST may recover by choosing a different component or candidate. Recovery is not guaranteed, as discussed in Section 6. Example 3. In the motivating example, suppose SI 2 for the unknown() ∧ x < z loop branch sequence is (y > z ∧ x ≤ z ∧ w = x), and the solver returns a Pres counterexample with σpre = (x=2, y=4, z=3, w=2) in ϕ2 (x < z ) and σpost = (x=3, y=4, z=3, w=3) in ϕ3 (unknown() ∧ x ≥ z ). Since the pre- and post-states belong to different loop branch sequences, the failure is ambiguous. Here σpre is genuinely reachable (starting from x=0, w=0 and iterating twice with x < z ), so the problem is that SI 3 does not accommodate states entering from ϕ2 . The framework therefore refines SI 3 , not SI 2 . Candidate selection (S ELECT B EST, Line 12). When all candidates in Y fail verification, a single candidate must be chosen for refinement. A naı̈ve heuristic that ranks by the number of satisfied Hoare conditions tends to favor vacuously true invariants (e.g., a trivially true candidate can satisfy both Init and Pres), making count-based ranking unreliable. We instead adopt an LLM-based selection strategy: a prompt presents the program x, all current candidates in Y , and their corresponding counterexamples, and asks the LLM to select the candidate whose sub-invariants impose the most specific (non-vacuous) constraints, whose violated clauses are fewest and suggest a localized fix rather than a structural mismatch. Because S ELECT B EST is invoked at every refinement iteration (Line 12), it naturally enables backtracking: if repeated refinement of one path does not converge, a different path from Y may be selected in a subsequent iteration, effectively switching to an alternative candidate at the problematic level while reusing the sub-

7

invariants at other levels.

5

E VALUATION

In this section, we address the following research questions through an empirical evaluation of C LOVER: RQ1 How effective is C LOVER on multiphase loop benchmarks compared to state-of-the-art tools? RQ2 How does C LOVER generalize to linear and nonlinear benchmarks relative to existing approaches? RQ3 What is the impact of individual components of C LOVER on its overall performance? RQ4 How do the effectiveness and runtime of C LOVER vary as the number of loop-body branches increases? 5.1

Setup

Benchmark suite. We evaluate C LOVER on three benchmark suites comprising a total of 420 verification tasks: (1) 316 linear arithmetic benchmarks from LaM4Inv [15], (2) 50 nonlinear(NL) arithmetic benchmarks from the Clause2Inv [16] benchmark suite, and (3) 54 multiphase arithmetic benchmarks from the CHC-COMP repository [23]. Linear benchmarks contain loops whose invariants can be expressed as linear arithmetic constraints (e.g., x + y ≤ 10), while nonlinear benchmarks require polynomial or more complex relationships (e.g., x × y ≥ n). These benchmarks are widely used in the loop invariant synthesis literature and cover a diverse range of program structures and invariant complexities. Baselines. We compare C LOVER against a diverse set of tools spanning three paradigms: (1) LLM-based methods, including Clause2Inv [16], LaM4Inv [15], LORIS [18] and PAL2Inv [22]; (2) learning-based methods, including Code2Inv [14] (reinforcement learning), CLN2INV [25] (neural network-based), and LIPuS [26] (RL-based); (3) traditional methods, including the multiphase invariant synthesizer ImplCheck [19], the CHC solver Eldarica [6], and the software model checkers CPAchecker [27] and UAutomizer [28]. ImplCheck discovers phase guards through model-based projection and learns phase-specific lemmas, combining them as implication invariants. Eldarica produces invariants directly by solving constrained Horn clauses. CPAchecker and UAutomizer verify safety properties via unreachability checking. For these tools, we extract loop invariants from their correctness witnesses and validate them with our SMT-based checker against the three standard Hoare conditions. Evaluation metrics. We evaluate the performance of C LOVER and the baseline tools using the following metrics: • # Solved: The total number of benchmarks for which the tool successfully synthesizes a valid invariant within the given time limit. • Avg. Time (s): The average time taken by the tool to solve each benchmark, measured in seconds. • Avg. Cost ($): The average monetary cost incurred by the tool for using the LLM API, measured in US dollars. Implementation. We implement C LOVER in Python. The front-end uses tree-sitter [29] to parse input C programs and construct ASTs, from which we derive the CFG and extract loop branch sequences. Candidate invariants are checked with Z3 [30].

AUTHOR MANUSCRIPT

8

TABLE 1 Results on the multiphase benchmark.

TABLE 2 Results on Linear and Nonlinear(NL) benchmark.

Method # Solved Avg. Time (s) Avg. Cost ($) Clause2Inv 20 51.95 0.018 LaM4Inv 25 112.69 0.709 LORIS 18 200.07 0.223 PAL2Inv 29 104.014 0.174 Code2Inv 5 58.27 N/A LIPuS 0 0.00 N/A CLN2INV 1 1.1 N/A Eldarica 20 94.76 N/A CPAchecker 4 3.60 N/A UAutomizer 19 23.05 N/A ImplCheck 22 8.95 N/A C LOVER 35 167.48 0.226

Method # Solved (Linear / NL) Avg. Time (s) Clause2Inv 345 (307 / 38) 14.41 (12.68 / 28.45) LaM4Inv 342 (311 / 31) 27.64 (23.66 / 67.58) LORIS 330 (287 / 43) 46.83 (46.16 / 51.32) PAL2Inv 242 (227 / 15) 37.78 (34.15 / 77.48) Code2Inv 205 (205 / 0) 34.54 (34.54 / 0.00) LIPuS 159 (159 / 0) 48.4 (48.4 / 0.00) CLN2INV 211 (211 / 0) 0.6 (0.6 / 0.00) Eldarica 256 (245 / 11) 2.78 (2.02 / 19.52) CPAchecker 145(134 / 11) 7.27(3.61 / 51.85) UAutomizer 321(292 / 29) 13.00(11.09 / 32.17) ImplCheck 289 (284 / 5) 2.02 (2.00 / 3.15) C LOVER 355 (311 / 44) 61.58 (51.83 / 130.51)

Experimental setup. All experiments were conducted on a 20-core Intel Core Ultra 7 265K CPU (up to 5.5 GHz) running Ubuntu 24.04 LTS. For LLM-based approaches, we use GPT5.1. For the tree-structured search, we set the parameters as follows: the number of generated samples per step is 5, the number of evaluation samples is 3, and the beam width (i.e., number of selected candidates) is 5. Each tool was allocated a maximum timeout of 600 seconds per benchmark, consistent with the budget used by LaM4Inv [15] and Clause2Inv [16]. We used the same version of the LLM API for all LLM-based tools to ensure a fair comparison.

Many of the remaining unsolved cases involve modulo (%) operations in branch conditions, which introduce highly non-monotonic and cyclic execution patterns. These behaviors make multiphase programs particularly challenging, as execution repeatedly alternates between loop branch sequences rather than following clearly separable phases. Consequently, it becomes difficult to capture program behavior using simple branch-based invariants. This pattern is common in multiphase benchmarks and poses a fundamental challenge for invariant synthesis, often requiring sophisticated reasoning even for human experts. A more detailed analysis of such cases is provided in Section 5.6. C LOVER’s higher coverage is consistent with its compositional design. Each loop branch sequence defines an inference component for which the LLM generates several complete candidate sub-invariants. Tree search selects one candidate per component, and their disjunction forms a complete loop invariant. This separates local inference from global composition: the LLM reasons about the arithmetic relations within one execution case, while the search explores alternative combinations across cases. The same component structure supports refinement: a verification counterexample identifies the component to repair, whose selected sub-invariant is replaced while the choices for other components remain fixed. Local alternatives and targeted replacement therefore work together to retain useful partial solutions across verification rounds.

5.2

RQ1: Multiphase Benchmarks

Table 1 summarizes performance on the 54 multiphase benchmarks. C LOVER solves 35 tasks, compared with 25 for LaM4Inv, 20 for Clause2Inv, and 18 for LORIS. Among these three LLM-based baselines, LaM4Inv has the highest coverage. C LOVER solves 40% more tasks. The strongest traditional method, ImplCheck, solves 22 tasks, followed by Eldarica with 20, giving C LOVER a 59.1% improvement over ImplCheck. Learning-based methods solve at most 5 tasks, indicating limited effectiveness on this suite. C LOVER takes 167.48 seconds on average and costs $0.226 per successful case: it is cheaper than LaM4Inv and close to LORIS, while Clause2Inv is substantially cheaper. PAL2Inv [22] is the strongest baseline on this suite, solving 29 tasks, six fewer than C LOVER. The relative improvement is 20.7%. Its path-sensitive design and initial invariants from abstract interpretation provide useful guidance for multiphase reasoning. It also has lower average runtime and API cost than C LOVER (104.014 seconds and $0.174). However, its refinement enriches and recombines path-indexed pools of atomic clauses rather than replacing one complete branch-specific sub-invariant while preserving the others. As these pools grow, the search must consider more clause combinations, and increasingly disjunctive candidates can burden SMT verification. This creates a potential scalability bottleneck. Abstract interpretation also supplies guidance whose precision depends on the chosen abstract domain. Thus, strong multiphase performance does not guarantee equally broad coverage across other program classes. PAL2Inv has the lowest linear and nonlinear coverage among the evaluated LLM-based methods, a contrast examined in Section 5.3.

5.3

RQ2: Linear/Nonlinear Benchmarks

As shown in Table 2, C LOVER solves 311 of the 316 linear benchmarks (98.4%). This ties LaM4Inv for the highest linear coverage, while exceeding Clause2Inv by 4 benchmarks and LORIS by 24. It also solves 19 more linear benchmarks than the strongest traditional baseline, UAutomizer, and 100 more than the strongest learning-based baseline, CLN2INV. The near-ceiling result shows that the branch-aware design does not sacrifice effectiveness on simpler control-flow structures. When a loop contains only one or a few loop branch sequences, decomposition produces a correspondingly small set of focused inference tasks. The framework therefore retains the benefit of branch-level reasoning without creating a large compositional search space, which helps it remain effective on conventional linear benchmarks. The advantage is more pronounced on the nonlinear suite. C LOVER solves 44 of 50 benchmarks (88%), the highest

AUTHOR MANUSCRIPT

TABLE 3 Ablation study on the multiphase benchmark. C LOVER-NL: No-Localization, and C LOVER-CoT: CoT-Generation.

Variant # Solved Avg. Time (s) Avg. Cost ($) C LOVER 35 167.48 0.226 C LOVER-NL 27 134.25 0.197 C LOVER-CoT 20 103.93 0.103

coverage among all evaluated tools. This is 1 more than LORIS (43), 6 more than Clause2Inv (38), 13 more than LaM4Inv (31), and 15 more than UAutomizer (29). None of the evaluated learning-based methods solves a nonlinear benchmark. These tasks require invariants containing polynomial expressions or relationships among several variables. The zero results for the learning-based approaches show that this suite lies outside their effective coverage, while the strongest traditional method reaches only 29 tasks. By separating branch-specific obligations, C LOVER presents the LLM with smaller inference problems and preserves a correct local relation when another branch requires refinement. The narrow one-benchmark margin over LORIS also indicates that improved local feedback is effective on nonlinear reasoning, whereas C LOVER’s larger gains emerge when such feedback is combined with explicit branch decomposition. PAL2Inv shows a different pattern from its strong multiphase result: it solves 227/316 linear tasks (71.8%) and 15/50 nonlinear tasks (30.0%), the lowest coverage among the evaluated LLM-based methods on both suites. C LOVER solves 84 more linear and 29 more nonlinear tasks. This contrast is consistent with limits of PAL2Inv’s dependence on guidance from abstract interpretation and its growing search over clause combinations. When the abstract domain provides only coarse information, the LLM must supply more of the missing relations. Adding atomic clauses then enlarges the combinations considered without identifying one complete local candidate to replace. C LOVER instead bounds its retained candidate paths with beam search and uses localized refinement to replace a selected component. Overall, C LOVER achieves the highest multiphase coverage while generalizing well to the linear and nonlinear suites, solving 355 of 366 tasks. It ties for the best linear coverage (311/316) and achieves the highest nonlinear coverage (44/50). These results indicate that branch-aware compositional inference and localized refinement retain effectiveness on simpler control-flow structures while supporting more complex nonlinear reasoning. 5.4

RQ3: Ablation Analysis

We conduct two ablation studies on the multiphase benchmarks to evaluate the two domain-specific contributions of C LOVER: compositional inference (decomposing generation along loop branch sequences) and counterexample-guided localized refinement. The first variant, C LOVER-NL (No-Localization), removes the localization mechanism in the refinement process. Instead of tracing counterexamples to identify and refine the specific failing loop branch sequence, the LLM is prompted to regenerate the entire invariant based on the program,

9

the counterexample, and the current (incorrect) invariant. This directly tests the value of localized refinement. The second variant, C LOVER-CoT, replaces the tree-structured search with a single Chain-of-Thought (CoT) [31] generation process, which is equivalent to setting beam width k = 1, thereby removing structured exploration over loop branch sequences while retaining localized refinement. As shown in Table 3, both variants achieve lower success rates compared to the full C LOVER framework. C LOVER-NL solves 27 out of 54 benchmarks, a drop of 8 compared to the full framework. Without localization, the LLM regenerates the entire invariant upon receiving a counterexample, which often introduces errors into previously correct subinvariants. A representative example of this regression behavior is discussed in Section 5.6. The C LOVER-CoT variant solves only 20 benchmarks, the lowest among all configurations. With k = 1, each loop branch sequence is assigned a single candidate, leaving no fallback options for either synthesis or refinement. The 43% drop in solved benchmarks (from 35 to 20) confirms that maintaining multiple candidates per loop branch sequence provides substantial benefit, as the tree-structured search explores diverse candidates and selects the combination that best satisfies local verification. The full C LOVER framework incurs moderately higher runtime and cost, which is expected given that it solves 8– 15 more benchmarks, many of which are inherently complex cases requiring multiple refinement iterations. These results confirm that the two domain-specific mechanisms address complementary failure modes: localized refinement prevents cross-branch regression during repair (C LOVER-NL drops 8 benchmarks), while compositional inference with candidate diversity prevents single-point generation errors during initial synthesis (C LOVER-CoT drops 15 benchmarks). Both are essential. Beam search provides the candidate pool but is itself a standard technique. The novelty lies in the compositional decomposition and the localized refinement it enables. 5.5

RQ4: Effect of Branch Count

To examine how branching affects C LOVER, we stratify all 420 benchmarks by control-flow structure. The original linear, nonlinear, and multiphase suites follow categories established by prior work, but arithmetic and branching characteristics can overlap: a linear-arithmetic benchmark may still contain several conditional paths. Pooling the suites and grouping them by branch count allows us to examine branching independently of these suite labels. We count the distinct non-exit loop-body branch sequences extracted from the CFG, excluding the exit case because it does not execute the loop body. A straight-line loop therefore has one branch sequence, while a loop with an internal conditional has two or more. This gives 176 singlebranch and 244 multi-branch benchmarks. C LOVER solves 174/176 single-branch tasks (98.9%), three more than the strongest LLM-based baseline, and 216/244 multi-branch tasks (88.5%), 13–76 more than the LLM-based baselines. Its success rate is 10.3 percentage points lower on the multi-branch subset, but its larger coverage margin over the baselines is consistent with decomposition being useful when inference must coordinate multiple execution cases.

AUTHOR MANUSCRIPT

10

TABLE 4 Performance of C LOVER stratified by the number of non-exit loop-body branches.

1 2

int main() { int x, y;

3

x = 0;

4

# Branches 1 2 3 4 ≥5

Benchmarks 176 139 33 55 17

Solved 174 119 31 50 16

Rate 98.9% 85.6% 93.9% 90.9% 94.1%

Median Time (s) 19.3 47.7 50.4 70.2 117.9

7 8 9 10 11 12

14

5.6

Case Study

We analyze two representative cases. The first illustrates how compositional inference and localized refinement work together on a multiphase program. The second examines a periodic program beyond the multiphase setting, offering insights into future directions. 5.6.1

Multiphase Invariant Synthesis

The program in Figure 5 exhibits clear multiphase behavior, where different ranges of x correspond to distinct update patterns for y . C LOVER addresses this by decomposing invariant synthesis along the four loop branch sequences, so that each phase is reasoned about independently. An initial invariant generated by C LOVER takes the form: (x < 5000 ∧ x ≥ 4000 ∧ y = 4x − 16000) ∨ (x < 4000 ∧ y = x) ∨ (x ≥ 6000∧y+x = 0) ∨ (x ≥ 5000∧x < 6000∧y = −3x+25000). We verify this candidate using an SMT solver, which returns a counterexample (x = 5000, y = 4000). Through counterexample-guided localization, the failure is traced to the loop branch sequence (unknown() ∧ x ≥ 5000 ∧ x < 6000), identifying the violated clause as y = −3x + 25000. Accordingly, only the sub-invariant for this loop branch sequence is updated, while all other components are preserved. By iteratively applying this targeted refinement process, C LOVER converges to a correct invariant: (x < 5000 ∧ x ≥ 4000 ∧ y = 4(x − 4000) + 4000) ∨ (x < 4000 ∧ y = x ∧ x ≥ 0) ∨ (x ≥ 6000 ∧ y = −x + 10000) ∨ (x ≥ 5000 ∧ x < 6000 ∧ y = −4x + 28000).

// pre-conditions

while (unknown()) { // loop body if (x < 5000) { if (x >= 4000) { y = y + 4; } else { y = y + 1; } } else { if (x >= 6000) { y = y - 1; } else { y = y - 4; } } x = x + 1; }

6

13

Table 4 provides a finer breakdown. Success rates vary from 85.6% to 94.1% across the groups with two or more branches and do not decrease monotonically with branch count. Median runtime, however, increases steadily from 19.3 seconds for one branch to 117.9 seconds for five or more. This trend is consistent with the framework’s design: additional branches create more sub-invariant generation tasks and enlarge the compositional search, while each generation query focuses on one execution case and localized refinement targets one component. Thus, the observed runtime grows with branch count, while coverage remains high across the groups. Semantic difficulty, including nonlinear or periodic updates and relationships spanning branches or phases, can still make local candidates difficult to infer. Because the groups differ in size and program semantics, these aggregate results do not isolate the causal effect of branch count. Nevertheless, they show increasing runtime without a monotonic decline in success on this corpus.

y = 0;

5

15 16 17 18 19 20 21 22

if (x == 10000) { assert(y == 0); }

23 24 25 26

// post-condition

}

Fig. 5. A representative multiphase loop with nested branches.

Comparing the initial and final invariants, the phase boundaries (e.g., x < 4000, 4000 ≤ x < 5000) are correctly identified from the outset, while only the arithmetic expressions within each phase require correction (e.g., y = −3x + 25000 is refined to y = −4x + 28000). This suggests that LLMs are effective at capturing the structural decomposition of multiphase programs, while precise numerical reasoning remains the primary source of error during generation. This separation between structural and arithmetic errors explains why the framework remains robust even when the initial candidate is incorrect: because each refinement iteration targets a single loop branch sequence’s arithmetic expression, errors in one branch do not propagate to others. We further observe that removing the localization mechanism causes this example to become unsolvable, providing direct evidence that localized refinement is essential for preventing cross-branch regression. Experimental evidence supporting these observations is presented in Section 5.4. 5.6.2 Periodic Programs Figure 6 presents a program that goes beyond the multiphase setting targeted by C LOVER. Unlike the monotonically progressing phases in the previous example, the modulo operation on x introduces periodic behavior: execution repeatedly alternates between x < 500 and x ≥ 500 with a fixed period of 1000, rather than progressing through separable phases. In this setting, the relationship between y and z depends on how many times the condition x < 500 holds within each cycle of length 1000. Capturing this relationship requires reasoning over periodic dependencies and global iteration counts, which lies outside the scope of phase-local analysis and remains an open challenge for all evaluated tools. A correct loop invariant does exist, as verified by an SMT solver. For example: (0 ≤ x ∧ x ≤ 500 ∧ z = y + x) ∨ (x ≥

AUTHOR MANUSCRIPT 1 2

11

int main() { int x, y, z;

3

x = 0;

4

y = 0;

z = 0;

// pre-conditions

5 6 7 8 9 10 11 12

while (unknown()) { if (x < 500) { z = z + 2; } x = (x + 1) % 1000; y = y + 1; }

// loop body

if (x == 0) { assert(y == z); }

// post-condition

13 14 15 16 17

}

Fig. 6. Periodic multiphase loop with modulo.

500∧y < 1000∧z = y+1000−x). Notably, this invariant still exhibits a disjunctive structure over branching conditions, suggesting that the decomposition strategy of C LOVER provides a useful structural foundation. The remaining gap lies in reasoning about periodic phase transitions, which we consider a promising direction for future extension.

6

D ISCUSSION

Invariant synthesis vs. unreachability-based verification. Software model checkers such as CPAchecker [27] and UAutomizer [28] verify safety properties via unreachability checking without necessarily producing explicit inductive invariants. C LOVER is not intended to replace such tools but targets the complementary problem of explicit invariant synthesis, which is needed in deductive verification [4], [32], compositional reasoning with module-level contracts [33], [34], proof certificate generation [35], and neurosymbolic verification pipelines [36]. A systematic comparison of the two paradigms on diverse program classes is a direction for future work. Relationship to PAL2I NV. PAL2I NV [22] is the closest architectural baseline because both approaches expose the structure of loop branch sequences during synthesis. It obtains initial invariants through abstract interpretation, generates atomic assertions for all enumerated loop branch sequences in one LLM response, and uses counterexampleguided clause combination to construct disjunctive invariants from clause pools indexed by loop branch sequence. C LOVER instead queries the LLM separately for each loop branch sequence, retains several complete candidate subinvariants per component, and constructs a global candidate by selecting one candidate for each component. A concrete SMT counterexample identifies the component to replace while the other selections remain fixed, whereas PAL2I NV enriches and recombines its clause pools. The distinction concerns how the structure of loop branch sequences supports independent generation and targeted replacement throughout the search. PAL2I NV solves 29 of 54 multiphase tasks compared with 35 for C LOVER, with lower mean runtime and API cost (Table 1). On the linear and nonlinear suites, C LOVER solves 311 and 44 tasks, respectively, compared with 227 and 15 for PAL2I NV (Table 2). The

main reasons for this coverage advantage are as follows. First, PAL2Inv’s abstract interpretation faces a precision– scalability trade-off: polyhedral analysis can become expensive as variables and constraints grow, while coarser domains may lose nonlinear or disjunctive relations. C LOVER generates local candidates directly, avoiding this preprocessing cost and dependence on abstraction precision. Second, growing pools of atomic assertions still require the correct grouping into conjunctions and disjunctions, increasing the cost of constructing candidates and verifying them with SMT. C LOVER generates complete local formulas, bounds retained global compositions through beam search, and repairs one selected component while preserving the others, reducing repeated reconstruction of useful combinations. Periodic control-flow patterns. As discussed in Section 5.6, C LOVER has difficulty handling programs where execution repeatedly alternates between loop branch sequences rather than progressing through separable phases. This limitation is shared by existing invariant synthesis techniques. Limits of heuristic recovery. When I S A MBIGUOUS detects a counterexample crossing two loop branch sequences, J UDGE B RANCH uses an LLM to estimate whether the predecessor state is reachable and select the component to refine. This judgment is heuristic. Misclassifying a reachable state as unreachable can direct repair toward the source component when the destination component needs correction, and the reverse error can leave a spurious predecessor unexcluded. Such misjudgments can waste refinement rounds, discard useful local candidates, or prevent synthesis before the timeout. LLM stochasticity can also provide an opportunity for recovery: if a later iteration revisits an ambiguous failure, a new sample may identify the correct loop branch sequence even when an earlier sample selected the wrong one. Candidate diversity and S ELECT B EST provide further opportunities to explore alternative compositions. However, successive samples may repeat the same error, and the verifier rejects invalid candidates without certifying the reachability judgment itself. Recovery is therefore possible but not guaranteed. These errors affect search efficiency and success within the time budget, while soundness is preserved because every returned invariant must satisfy all SMT verification conditions. LLM stochasticity and robustness. Our design mitigates LLM stochasticity at two levels: localized refinement confines each edit to one sub-invariant, while beam search provides candidate diversity. The independent ablations (Section 5.4) support both contributions: removing localization reduces solved benchmarks from 35 to 27, while restricting search to one candidate per loop branch sequence (CoT, k=1) while retaining localization reduces coverage from 35 to 20. Choice of LLM. All LLM-based tools use the same model (GPT-5.1) to ensure a fair comparison. The framework is model-agnostic in that it relies only on standard text generation with structured JSON output and does not depend on any model-specific features. Using one model isolates the contribution of our framework architecture from confounds introduced by varying model capabilities. Data contamination. Due to the opaque nature of LLM training data, benchmark programs may have been seen during pretraining. Our ablation study (Section 5.4) sug-

AUTHOR MANUSCRIPT

gests the model is not simply memorizing solutions, but this threat applies to all LLM-based baselines and cannot be entirely eliminated.

7

R ELATED W ORK

Traditional and learning-based loop invariant synthesis. Traditional approaches rely on symbolic techniques such as abstract interpretation [37], [38], [39], [40], abduction [33], [41], dynamic analysis [42], [43], [44], model checking [6], [45], Craig interpolation [9], [10], constraint-based and SyGuS methods [5], [46], [47], [48], and CEGAR [49], [50]. On the learning side, the ICE framework [11] introduced a foundational paradigm of learning from examples, counterexamples, and implications, inspiring decision-tree-based [12], [19], [51], [52], classification-based [53], and reinforcementlearning-guided [54] methods. Representative learningbased tools include Code2Inv [14], which learns candidates with neural models, CLN2INV [25], which uses continuous logic networks, and LIPuS [26], which combines reinforcement learning with SMT solving. ImplCheck [19] uses model-based projection to discover phase guards and data learning to synthesize implication invariants, including for mutually dependent periodic phases. AutoINF [55] models loop paths with a path dependency automaton and uses targeted counterexamples to refine polynomial invariant templates. Its trace-based template inference offers a symbolic comparison with our LLM-generated local candidates and search over complete compositions. These approaches differ in their supported invariant representations, abstractions, and search strategies. Our work leverages the generative capacity of LLMs and specifically targets multiphase programs where invariants must capture phase-specific behaviors. We note that software model checkers such as CPAchecker [27] and UAutomizer [28] address the orthogonal problem of unreachability-based verification without necessarily producing explicit invariants, and a detailed discussion of the complementary roles of invariant synthesis and unreachability checking is provided in Section 6. LLM-based loop invariant synthesis. Recent work leverages large language models (LLMs) to generate loop invariants, each adopting a different decomposition strategy. ACInv [17] targets data-structure-rich programs by combining static analysis with an LLM-based evaluator for iterative refinement. Clause2Inv [16] decomposes at the clause level, generating individual clauses that are assembled and validated by an SMT solver. LaM4Inv [15] filters LLM-generated predicates via bounded model checking before reassembling them for Z3 verification. LORIS [18] improves feedback quality by translating the LLM’s reasoning steps into first-order logic implications to pinpoint logical flaws. PAL2Inv [22] combines abstract interpretation with atomic assertions generated for enumerated loop branch sequences and counterexample-guided clause combination. It maintains pools of assertions for these sequences, whereas C LOVER separately generates and retains complete local candidate formulas for targeted replacement. Our work differs in two fundamental ways: compositional inference decomposes invariant synthesis along loop branch sequences so that the LLM reasons about one execution scenario at a time, and counterexample-guided localized refinement

12

traces verification failures to the specific failing loop branch sequence and repairs only that phase’s sub-invariant. This phase-level repair capability is unavailable to whole-loop methods. LLM-based formal verification. LLMs have also been applied to broader formal verification tasks. Baldur [56] demonstrates that LLMs can generate and repair complete proofs, while Lemur [36] provides a formally sound framework for integrating LLMs with SMT solvers. Cai et al. [57], [58] apply refinement calculus to guide LLMbased program synthesis with formal guarantees, and Wen et al. [59] combine LLMs with static analysis to synthesize full program specifications. Other studies evaluate LLMassisted verification workflows [60], [61], [62] or survey LLM trustworthiness from a verification perspective [63]. These works establish the viability of LLM-based formal reasoning and inform the design of our framework, which applies LLM–solver integration specifically to the problem of multiphase invariant synthesis. Structured reasoning with LLMs. Tree-of-Thought [64], [65] and self-consistency [66] extend chain-of-thought prompting [31] by exploring multiple reasoning paths via tree search or sampling. These methods use generic decompositions with LLM self-evaluation at each node. C LOVER differs in two key respects: its tree topology is derived from the program’s branch semantics (compositional inference) rather than generic reasoning steps, and refinement is guided by SMT counterexamples that precisely localize the failing loop branch sequence (localized refinement) rather than relying on LLM self-evaluation for backtracking decisions.

8

C ONCLUSION

We present C LOVER, a framework for loop invariant inference on multiphase programs. Compositional inference decomposes synthesis along loop branch sequences so that the LLM reasons about one execution scenario at a time, while counterexample-guided localized refinement traces failures to the responsible loop branch sequence and repairs only that sub-invariant. Experiments on 420 benchmarks show that C LOVER achieves state-of-the-art performance on multiphase programs and remains competitive on linear/nonlinear benchmarks.

ACKNOWLEDGMENTS ChatGPT and Claude are used for language polishing. All scientific content is solely the authors’ own work.

R EFERENCES [1] [2]

[3] [4]

C. A. Furia, B. Meyer, and S. Velder, “Loop invariants: Analysis, classification, and examples,” ACM Computing Surveys (CSUR), vol. 46, no. 3, pp. 1–51, 2014. V. D’silva, D. Kroening, and G. Weissenbacher, “A survey of automated techniques for formal software verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, pp. 1165–1178, 2008. J. H. Fetzer, “Program verification: The very idea,” Communications of the ACM, vol. 31, no. 9, pp. 1048–1063, 1988. C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576–580, 1969.

AUTHOR MANUSCRIPT

[5]

M. A. Colón, S. Sankaranarayanan, and H. B. Sipma, “Linear invariant generation using non-linear constraint solving,” in International Conference on Computer Aided Verification. Springer, 2003, pp. 420–432. [6] H. Hojjat and P. Rümmer, “The Eldarica horn solver,” in 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 2018, pp. 1–7. [7] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement,” in International Conference on Computer Aided Verification. Springer, 2000, pp. 154– 169. [8] S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample-guided refinement of template polyhedra,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2017, pp. 589–606. [9] R. Jhala and K. L. McMillan, “A practical and complete approach to predicate refinement,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2006, pp. 459–473. [10] K. L. McMillan, “Lazy annotation for program testing and verification,” in International Conference on Computer Aided Verification. Springer, 2010, pp. 104–118. [11] P. Garg, C. Löding, P. Madhusudan, and D. Neider, “Ice: A robust framework for learning invariants,” in International Conference on Computer Aided Verification. Springer, 2014, pp. 69–87. [12] P. Garg, D. Neider, P. Madhusudan, and D. Roth, “Learning invariants using decision trees and implication counterexamples,” ACM Sigplan Notices, vol. 51, no. 1, pp. 499–512, 2016. [13] T. Nguyen, T. Antonopoulos, A. Ruef, and M. Hicks, “Counterexample-guided approach to finding numerical invariants,” in Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017, pp. 605–615. [14] X. Si, A. Naik, H. Dai, M. Naik, and L. Song, “Code2Inv: A deep learning framework for program verification,” in International Conference on Computer Aided Verification. Springer, 2020, pp. 151– 164. [15] G. Wu, W. Cao, Y. Yao, H. Wei, T. Chen, and X. Ma, “Llm meets bounded model checking: Neuro-symbolic loop invariant inference,” in Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024, pp. 406–417. [16] W. Cao, G. Wu, T. Xu, Y. Yao, H. Wei, T. Chen, and X. Ma, “Clause2inv: A generate-combine-check framework for loop invariant inference,” Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 1009–1030, 2025. [17] R. Liu, M. Chen, L.-I. Wu, J. Ke, and G. Li, “Enhancing automated loop invariant generation for complex programs with large language models,” Science of Computer Programming, vol. 248, p. 103387, 2026. [Online]. Available: https://www.sciencedirect. com/science/article/pii/S0167642325001261 [18] T. Li, Z. Yan, J. Liu, P. Di, and X. Zhang, “Guiding LLM-based loop invariant synthesis via feedback on local reasoning errors,” ACM Trans. Program. Lang. Syst., vol. 48, no. 2, pp. 1–30, 2026. [19] D. Riley and G. Fedyukovich, “Multi-phase invariant synthesis,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022, pp. 607–619. [20] T. Nguyen, D. Kapur, W. Weimer, and S. Forrest, “Using dynamic analysis to generate disjunctive invariants,” in 36th International Conference on Software Engineering, ICSE ’14. ACM, 2014, pp. 608– 619. [21] S. Gulwani, S. Jain, and E. Koskinen, “Control-flow refinement and progress invariants for bound analysis,” in Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2009, pp. 375–385. [22] G. Fan, L. Chen, P. Yao, B. Yin, W. Zhang, and J. Wang, “Pathsensitive loop invariant inference via large language models and abstract interpretation,” ACM Transactions on Software Engineering and Methodology, 2026. [23] P. Rümmer, “aeval-benchmarks,” https://github.com/chc-comp/ aeval-benchmarks, 2025, gitHub repository. [24] E. De Angelis and H. G. Vediramana Krishnan, “Competition of solvers for constrained horn clauses (chc-comp 2023),” in International TOOLympics Challenge. Springer, 2023, pp. 38–51. [25] G. Ryan, J. Wong, J. Yao, R. Gu, and S. Jana, “CLN2INV: Learning loop invariants with continuous logic networks,” in The Eighth International Conference on Learning Representations (ICLR), 2020.

13

[26] S. Yu, T. Wang, and J. Wang, “Loop invariant inference through SMT solving enhanced reinforcement learning,” in Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2023. [27] D. Beyer and M. E. Keremoglu, “CPAchecker: A tool for configurable software verification,” in Proceedings of the 23rd International Conference on Computer Aided Verification (CAV). Springer, 2011, pp. 184–190. [28] M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski, “Ultimate Automizer with SMTInterpol,” in Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 2013, pp. 641–643. [29] M. Brunsfeld, A. Qureshi, A. Hlynskyi, ObserverOfTime, W. Lillis, J. Vera, dundargoc, P. Turnbull, T. Clem, D. Creager, A. Helwer, R. Rix, D. Kavolis, C. Clason, M. Davis, R. Bruins, A. Delpeuch, Ika, A. Ya, T.-A. Nguyen, bfredl, S. Brunk, M. Massicotte, N. Hasabnis, J. McCoy, M. Dong, S. Moelius, S. Kalt, and Kolja, “tree-sitter/tree-sitter: v0.25.10,” Sep. 2025. [Online]. Available: https://doi.org/10.5281/zenodo.17180150 [30] L. De Moura and N. Bjørner, “Z3: An efficient SMT solver,” in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340. [31] J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou et al., “Chain-of-thought prompting elicits reasoning in large language models,” Advances in neural information processing systems, vol. 35, pp. 24 824–24 837, 2022. [32] K. R. M. Leino, “Dafny: An automatic program verifier for functional correctness,” in Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Springer, 2010, pp. 348–370. [33] C. Calcagno, D. Distefano, and V. Vafeiadis, “Bi-abductive resource invariant synthesis,” in Asian Symposium on Programming Languages and Systems. Springer, 2009, pp. 259–274. [34] C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. O’Hearn, I. Papakonstantinou, J. Purbrick, and D. Rodriguez, “Moving fast with software verification,” in Proceedings of the 7th NASA Formal Methods Symposium (NFM). Springer, 2015, pp. 3–11. [35] D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and A. Stahlbauer, “Witness validation and stepwise testification across software verifiers,” in Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE). ACM, 2015, pp. 721–733. [36] H. Wu, C. Barrett, and N. Narodytska, “Lemur: Integrating large language models in automated program verification,” in The Twelfth International Conference on Learning Representations (ICLR), 2024. [37] P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACTSIGPLAN symposium on Principles of programming languages, 1977, pp. 238–252. [38] P. Cousot and R. Cousot, “Systematic design of program analysis frameworks,” in Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1979, pp. 269– 282. [39] M. Karr, “Affine relationships among variables of a program,” Acta informatica, vol. 6, no. 2, pp. 133–151, 1976. [40] P. Cousot and N. Halbwachs, “Automatic discovery of linear restraints among variables of a program,” in Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1978, pp. 84–96. [41] I. Dillig, T. Dillig, B. Li, and K. McMillan, “Inductive invariant generation via abductive inference,” Acm Sigplan Notices, vol. 48, no. 10, pp. 443–456, 2013. [42] M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao, “The daikon system for dynamic detection of likely invariants,” Science of computer programming, vol. 69, no. 1-3, pp. 35–45, 2007. [43] M. Echenim, N. Peltier, and Y. Sellami, “Ilinva: Using abduction to generate loop invariants,” in International Symposium on Frontiers of Combining Systems. Springer, 2019, pp. 77–93. [44] C. Lattner and V. Adve, “LLVM: A compilation framework for lifelong program analysis & transformation,” in International Symposium on Code Generation and Optimization (CGO). IEEE, 2004, pp. 75–86.

AUTHOR MANUSCRIPT

[45] H. G. Vediramana Krishnan, Y. Chen, S. Shoham, and A. Gurfinkel, “Global guidance for local generalization in model checking,” Formal Methods in System Design, vol. 63, no. 1, pp. 81–109, 2024. [46] A. Gupta, R. Majumdar, and A. Rybalchenko, “From tests to proofs,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2009, pp. 262–276. [47] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli et al., “cvc5: A versatile and industrial-strength smt solver,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2022, pp. 415–442. [48] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, and C. Tinelli, “cvc4,” in International Conference on Computer Aided Verification. Springer, 2011, pp. 171–177. [49] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement for symbolic model checking,” Journal of the ACM (JACM), vol. 50, no. 5, pp. 752–794, 2003. [50] H. Zhu, A. V. Nori, and S. Jagannathan, “Learning refinement types,” ACM SIGPLAN Notices, vol. 50, no. 9, pp. 400–411, 2015. [51] P. Ezudheen, D. Neider, D. D’Souza, P. Garg, and P. Madhusudan, “Horn-ice learning for synthesizing invariants and contracts,” Proceedings of the ACM on Programming Languages, vol. 2, no. OOPSLA, pp. 1–25, 2018. [52] R. Xu, F. He, and B.-Y. Wang, “Interval counterexamples for loop invariant learning,” in Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020, pp. 111–122. [53] H. Lu, C. Wang, J. Gui, and H. Huang, “Pblinv: Postconditionbased loop invariant learning for c programs,” 2020 IEEE 20th International Conference on Software Quality, Reliability and Security (QRS), pp. 1–12, 2020. [54] C. Liu, X. Wu, Y. Feng, Q. Cao, and J. Yan, “Towards general loop invariant generation: A benchmark of programs with memory manipulation,” in Advances in Neural Information Processing Systems 37, 2024. [55] A. S. Hadad, F. Saeed, A. A. Ahmed, and J. Zheng, “AutoINF: Path-sensitive invariant inference for multipath loops,” Computer Modeling in Engineering & Sciences, vol. 148, no. 1, p. 35, 2026. [56] E. First, M. N. Rabe, T. Ringer, and Y. Brun, “Baldur: Whole-proof generation and repair with large language models,” in Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023, pp. 1229–1241. [57] Y. Cai, Z. Hou, X. Luan, D. M. S. Baena, Y. Lin, J. Sun, and J. S. Dong, “Towards large language model aided program refinement,” arXiv preprint arXiv:2406.18616, 2024. [58] Y. Cai, Z. Hou, D. Sanán, X. Luan, Y. Lin, J. Sun, and J. S. Dong, “Automated program refinement: Guide and verify code large language model with refinement calculus,” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, pp. 2057–2089, 2025. [59] C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S.-C. Cheung, and C. Tian, “Enchanting program specification synthesis by large language models using static analysis and program verification,” in International Conference on Computer Aided Verification. Springer, 2024, pp. 302–328. [60] A. Kamath, N. Mohammed, A. Senthilnathan, S. Chakraborty, P. Deligiannis, S. K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma, “Leveraging llms for program verification,” in 2024 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2024, pp. 107–118. [61] W. Wang, M. Farrell, L. C. Cordeiro, and L. Zhao, “Supporting software formal verification with large language models: An experimental study,” in 2025 IEEE 33rd International Requirements Engineering Conference (RE). IEEE, 2025, pp. 423–431. [62] J. O. Couder, D. Gomez, and O. Ochoa, “Requirements verification through the analysis of source code by large language models,” in SoutheastCon 2024. IEEE, 2024, pp. 75–80. [63] X. Huang, W. Ruan, W. Huang, G. Jin, Y. Dong, C. Wu, S. Bensalem, R. Mu, Y. Qi, X. Zhao et al., “A survey of safety and trustworthiness of large language models through the lens of verification and validation,” Artificial Intelligence Review, vol. 57, no. 7, p. 175, 2024. [64] S. Yao, D. Yu, J. Zhao, I. Shafran, T. Griffiths, Y. Cao, and K. Narasimhan, “Tree of thoughts: Deliberate problem solving with large language models,” Advances in neural information processing systems, vol. 36, pp. 11 809–11 822, 2023.

14

[65] J. Long, “Large language model guided tree-of-thought,” arXiv preprint arXiv:2305.08291, 2023. [66] X. Wang, J. Wei, D. Schuurmans, Q. Le, E. Chi, S. Narang, A. Chowdhery, and D. Zhou, “Self-consistency improves chain of thought reasoning in language models,” in The Eleventh International Conference on Learning Representations (ICLR), 2023.

Related documents

• Recursive Semantic Divergence for LLM Agent Consistency#1455493
• ChaosBench-Logic: A Benchmark for Logical and Symbolic Reasoning on Chaotic Dynamical Systems#1355549
• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning#1325206
• COMPASS: Finding Where Reasoning Lives in Language Models#1216844
• UMAS: System-Level Uncertainty Quantification for Multi-Agent LLM Systems#1455494