PaperlayerView exact revision on arXiv

Source-linked AI summary

Ranking Function Generation with LLMs for Termination

Rongkang Li, Jiaxin Hu, Taolue Chen, Yong Li, Fu Song, Zhilin Wu

arXiv:2610.35523v1cs.SEcs.AIcs.LO

TL;DR

Template-based ranking-function synthesis can require substantial manual effort, and LLMs may produce incorrect outputs. RAINFALL combines LLM generation with symbolic verification and feedback; on two benchmark suites, it outperforms state-of-the-art tools and complements PROTON 2.1.

  • Problem

    Classical ranking-function synthesis depends on suitable templates, whose design can require substantial manual effort or expensive exploration, while LLMs may struggle with ranking-function reasoning and produce incorrect outputs.

    Source: §1 · pp. 2–3

  • Method

    RAINFALL uses structured prompts and few-shot examples to generate code assertions, then symbolically checks them and feeds diagnostics back to the LLM for refinement.

    Source: §1 · p. 3

  • Results

    323 programs (90.22%) receive verifiable ranking functions from RAINFALL with MiniMax V2.7, outperforming PROTON 2.1 (86.87%) on two public benchmark suites of 358 terminating C programs.

    Source: §1 · p. 4

  • Takeaways & Limitations

    The results suggest a neuro-symbolic framework for ranking-function synthesis that may extend to formally checkable liveness certificates beyond termination.

    Source: §6 · pp. 19–20

    The evaluation uses two public benchmark suites, so effectiveness may differ on other benchmarks or real-world programs; possible benchmark contamination also remains a concern.

    Source: §5.4 · p. 19

Abstract

from arXiv · show

Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise. We propose RAINFALL, a neuro-symbolic framework which follows the generate-verify-refine paradigm and tightly integrates LLMs with symbolic verification. RAINFALL formulates ranking function synthesis as a code-completion task by inserting placeholders into the input program and constraining the LLM to fill four predefined slots for each loop. The completed program is then checked by a symbolic verifier. If verification succeeds, a valid ranking function is obtained; otherwise, the verifier's diagnostics are translated into natural-language feedback that guides iterative refinement of the LLM's output. We evaluate RAINFALL on two public benchmark suites comprising 358 terminating C programs. Using MiniMax V2.7, RAINFALL synthesizes verifiable ranking functions for 323 programs (90.22%), outperforming all promising baselines. In particular, it solves 12 more programs than PROTON 2.1, the best-performing baseline and winner of the SV-COMP 2026 Termination category. Furthermore, combining RAINFALL with PROTON 2.1 increases the success rate to 96.65% (346/358 programs). We also conduct ablation study confirming individual contributions of placeholder contracts, few-shot examples, symbolic verification, and diagnostic information feedback. Experiments across LLMs further confirm the effectiveness of RAINFALL. Our results suggest a generic, sound framework for ranking-function synthesis and, beyond termination, LLM-assisted synthesis of formally checkable liveness certificates, both of which represent new directions of software engineering research.

1 Introduction

RAINFALL addresses the difficulty of generating valid ranking functions by combining LLM generation with symbolic verification and iterative refinement. On public benchmarks, it outperforms state-of-the-art tools, while its broader framework points toward synthesis of other formally checkable liveness certificates.

1 Introduction

  • Classical template-based synthesis depends on suitable ranking templates, while LLMs may struggle with ranking-function reasoning and can generate plausible but incorrect assertions.These challenges motivate both structured generation and checks that detect and repair errors.Source: §1 · pp. 2–3
  • RAINFALL reframes ranking-function synthesis as code-assertion generation and uses structured prompts with expert knowledge and few-shot examples.This approach avoids requiring LLMs to interpret complicated ranking-function definitions.Source: §1 · pp. 3–4
  • Its symbolic pipeline checks that the program is unchanged, assertions are complete, and assertions hold; diagnostic feedback guides refinement of incorrect outputs.The checks establish soundness for accepted outputs, while feedback can identify program changes, missing conditions, or counterexamples.Source: §1 · p. 4
  • 323 programs (90.22%) receive verifiable ranking functions from RAINFALL with MiniMax V2.7, outperforming six state-of-the-art tools including PROTON 2.1 (86.87%).Combining RAINFALL with PROTON 2.1 solves 346 tasks, a 96.65% success rate.Source: §1 · p. 4
  • The framework is presented as extensible to richer ranking-function templates and as a neuro-symbolic approach that may support formally checkable liveness certificates beyond termination.The paper focuses on three common ranking-function classes and unconditional termination; conditional termination is suggested as a potential extension.Source: §1 · pp. 4–5
  • The paper’s contributions include a generate-verify-refine framework integrating LLM generation, expert knowledge, few-shot examples, symbolic checks, and diagnostic feedback.The introduction also reports an evaluation against six state-of-the-art tools.Source: §1 · p. 5

2 Preliminaries

The preliminaries model programs as state-transition systems and explain why ranking functions certify termination. They distinguish single, multiphase, and lexicographic rankings, including cases where a single linear function is insufficient.

2 Preliminaries

  • A well-founded relation admits no infinite descending chain, which underlies the termination guarantee from a decreasing ranking function.The natural-number less-than relation is one example of a well-founded relation.Source: §2 · pp. 5–6
  • A program is modeled by its states, initial states, and transition relation; computations follow transitions from an initial state, and termination means every computation is finite.A ranking function proves termination when it decreases along transitions over a well-founded set and the lower bound entails exit from the loop.Source: §2 · pp. 5–6

2.1 Common Classes of Ranking Functions

  • A single ranking function maps states to nonnegative values that decrease by at least a positive constant on every transition.Its value must become negative when the loop guard is false, so the loop cannot continue indefinitely.Source: §2.1 · p. 6
  • The example program has no single linear ranking function, but it admits multiphase and lexicographic rankings that capture its changing phases of progress.In the multiphase account, −y decreases first while x may increase, then x decreases after y becomes positive; a lexicographic account also captures the transition.Source: §2.1 · pp. 6–7
  • A multiphase ranking function uses components that decrease in successive phases, with each phase ending when its component becomes negative.A finite sequence of such phases can witness termination when the final component becoming negative entails that the loop guard is false.Source: §2.1 · p. 6

3 Related Work

Related work spans template-based symbolic synthesis, data-driven and neural approaches, and termination-analysis tools. The approaches differ in expressiveness, reliance on templates or execution data, and how they validate candidates.

3 Related Work

  • Template-based symbolic methods solve constraints over predefined ranking-function forms, so their effectiveness depends on choosing suitable templates.Forms include linear, multiphase, and lexicographic rankings; more expressive templates may use polynomial or rational expressions.Source: §3 · pp. 7–8
  • Neural and data-driven methods learn or predict candidate functions, with some validating candidates using SMT and relying on high-quality execution data.Other symbolic methods analyze transition relations using techniques such as size-change analysis, refinement, and abstract interpretation.Source: §3 · p. 8
  • Termination tools use varied strategies, including integer transition systems, cycle analysis, candidate enumeration, and fine-tuned LLMs.The related work also distinguishes LLM-based prediction, which is not the paper’s focus.Source: §3 · p. 8

4 Our Approach

RAINFALL turns ranking-function synthesis into constrained code completion, then uses symbolic checks and diagnostic feedback to refine candidate programs. Its workflow covers instrumentation, iterative verification, and checks for preserving the original program and validating the generated assertions.

4 Our Approach

  • RAINFALL instruments each loop with four placeholders and iteratively verifies LLM-filled programs, returning a verified termination certificate or Unknown when its resource budget is exhausted.The checks cover equivalence, assertion completeness, and assertion validity; failures feed diagnostics into the next prompt.Source: §4 · pp. 8–9

4.1 Preprocessing

  • Four predefined slots capture auxiliary-variable declarations, pre-iteration values, post-iteration updates, and assertions for decrease, non-negativity, and termination.The constrained slots aim to prevent changes to other program logic and make generation more predictable.Source: §4.1 · pp. 9–10

4.2 Iterative Generation-Verification

  • The iterative phase queries the LLM, checks each candidate, and adds verifier diagnostics to the prompt until a valid ranking function is found or resources run out.The initial prompt includes the instrumented program, natural-language guidance, and few-shot examples.Source: §4.2 · p. 10, §4.1 · p. 10

4.2.1 Syntactic Equivalence Checking.

  • Syntactic equivalence checking compares program syntax after removing generated assertions, catching cases where the LLM changes original code and thereby invalidates an otherwise plausible ranking function.The example replaces x=x-y with x=x-1, so the candidate function is not valid for the original program.Source: §4.2.1 · p. 11

4.2.2 Code-Assertion Completeness Checking.

  • Incomplete assertions can pass assertion checking yet admit a non-terminating program, so completeness checking must require phase-two decrease after phase one becomes negative.The example changes x's update while leaving the assertions satisfied.Source: §4.2.2 · p. 12
  • Completeness checking parses ghost-variable declarations and updates, then checks whether assertions encode the required decrease, non-negativity, and termination conditions.The previous and current ranking components must correspond, with updates before and after each iteration; assertion requirements depend on the ranking-function class.Source: §4.2.2 · pp. 12–13

4.2.3 Assertion Checking.

  • Semantic assertion checking verifies whether the assertions induce a valid ranking function for the unchanged original program; a counterexample identifies a violated assertion for refinement.The example's candidate fails non-negativity, while the refined candidate passes all three checks and proves termination.Source: §4.2.3 · p. 14

4.2.4 Prompt Augment with Diagnostic Information Feedback.

  • Feedback is tailored to the failed check: it can identify mismatched statements, incomplete slot contents, or a violated assertion and counterexample.When the verifier reports Unknown or times out, that outcome is also included in the diagnostic information.Source: §4.2.3 · p. 14, §4.2.4 · p. 15

5 Evaluation

Across two benchmark suites, RAINFALL solves more tasks than the baselines, while combining it with PROTON proves 346 of 358 programs. Ablations and cross-LLM evaluations examine the framework’s components and robustness; the evaluation is limited to selected benchmarks and depends on the safety verifier used.

5.4 Threats to validity

  • The evaluation uses two public benchmark suites of terminating C programs, with RQ2 and RQ3 limited to BS-F because of LLM token costs.The authors note that effectiveness may differ on other benchmarks or real-world programs, and that public benchmark contamination is possible.Source: §5 · p. 15, §5.4 · p. 19

5.1 RQ1: Effectiveness

  • RAIN​​FALL solves 12 more tasks than PROTON, the best-performing baseline, and leads the baselines across both benchmark suites.Table 1 reports the baseline comparison; RAINFALL is slower than other baselines because of remote LLM-query overhead.Source: §5.1 · p. 16, Table 1 · p. 16
  • 346 of 358 programs are proved by combining RAINFALL with PROTON: 167 of 170 on BS-F and 179 of 188 on BS-L.On the 14 programs RAINFALL leaves unsolved in BS-F, the reported causes include incorrect loop bounds, empty initial outputs, verifier timeouts, and query exhaustion.Source: §5.1 · p. 17

5.2 RQ2: Ablation Study

  • On BS-F, few-shot examples raise solved tasks from 70 to 110 in a single MiniMax query, while symbolic checks remain necessary to filter and diagnose invalid outputs.With few-shot examples, the three checks still report 4 syntactic-equivalence, 9 completeness, and 7 assertion-checking errors; under the full setting they report 10, 9, and 15, respectively.Source: §5.2 · p. 17
  • With more LLM queries, RAINFALL’s solved-program count rises and exceeds LOOPY’s: it solves 129 versus 107 using six queries and 156 versus 124 using twelve.Within each six-query attempt, solved counts rise rapidly at first and then plateau; restarting an attempt produces another sharp increase.Source: §5.2 · p. 18

5.3 RQ3: Impact of LLMs

  • RAIN​​FALL outperforms the baselines with most evaluated LLMs; GPT and Claude-Opus solve the most programs and have the lowest average time, while Claude-Opus costs over three times as much as GPT.Qwen-Plus is the exception, performing worse than ddlTerm and PROTON despite higher token usage and longer runtime.Source: §5.3 · p. 18, Table 2 · p. 19

5.4 Threats to validity

  • RAIN​​FALL’s effectiveness may vary with the safety verifier employed; the evaluation uses UAutomizer as its backend.The authors identify evaluation on additional benchmarks and real-world programs as future work.Source: §5.4 · p. 19

6 Conclusion

RAINFALL frames ranking-function synthesis as code-assertion generation within an iterative generate-verify-refine workflow. Its experiments show improvements over state-of-the-art baselines and complementarity with symbolic termination tools, supporting the promise of combining LLM generation with symbolic verification.

6 Conclusion

  • RAINFALL formulates ranking-function synthesis as code-assertion generation with dedicated placeholders in an iterative generate-verify-refine workflow.Its symbolic verification pipeline is tailored to LLM-generated code assertions.Source: §6 · p. 19
  • Incorporating ranking-function expertise, few-shot examples, and diagnostic information into prompts can significantly enhance generation accuracy.The framework uses a symbolic verification pipeline to ensure soundness.Source: §6 · p. 19
  • RAINFALL outperforms state-of-the-art baselines and complements existing symbolic termination analysis tools.Source: §6 · p. 19
  • The work demonstrates the promise of combining LLM generation with the formal rigor of symbolic verification for ranking-function synthesis.The authors expect this paradigm to become increasingly effective as LLMs improve.Source: §6 · p. 20
Loading 2610.35523v1…