# Ranking LLM-Generated Loop Invariants for Program Verification

arXiv: https://arxiv.org/abs/2310.09342 · HTML: https://mlsanity.com/paper/2310.09342/

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 37 references that are in the map.
- First posted on arXiv 13 Oct 2023.

## Builds on (most cited first, 9 of 9)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [LoopInvGen: A Loop Invariant Generator based on Precondition Inference](https://mlsanity.com/paper/1707.02029/) (2017)

## Built on by (most cited first, 30 of 33)

- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [LLMDFA: Analyzing Dataflow in Code with Large Language Models](https://mlsanity.com/paper/2402.10754/) (2024)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Locus: Agentic Predicate Synthesis for Directed Fuzzing](https://mlsanity.com/paper/2508.21302/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://mlsanity.com/paper/2502.15441/) (2025)
- [XplainLLM: A Knowledge-Augmented Dataset for Reliable Grounded Explanations in LLMs](https://mlsanity.com/paper/2311.08614/) (2023)
- [EditLord: Learning Code Transformation Rules for Code Editing](https://mlsanity.com/paper/2504.15284/) (2025)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Inferring multiple helper Dafny assertions with LLMs](https://mlsanity.com/paper/2511.00125/) (2025)
- [Next Steps in LLM-Supported Java Verification](https://mlsanity.com/paper/2502.01573/) (2025)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)
- [Towards Large Language Model Aided Program Refinement](https://mlsanity.com/paper/2406.18616/) (2024)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Assured Automatic Programming via Large Language Models](https://mlsanity.com/paper/2410.18494/) (2024)
- [Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters](https://mlsanity.com/paper/2503.12686/) (2025)
- [CETBench: A Novel Dataset constructed via Transformations over Programs for Benchmarking LLMs for Code-Equivalence Checking](https://mlsanity.com/paper/2506.04019/) (2025)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)
- [Lucy: Think and Reason to Solve Text-to-SQL](https://mlsanity.com/paper/2407.05153/) (2024)
- [Exploring the Feasibility of End-to-End Large Language Model as a Compiler](https://mlsanity.com/paper/2511.04132/) (2025)
- [Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs](https://mlsanity.com/paper/2603.15510/) (2026)
- [SpecPylot: Python Specification Generation using Large Language Models](https://mlsanity.com/paper/2604.16560/) (2026)
- [Natural Language based Specification and Verification](https://mlsanity.com/paper/2605.11315/) (2026)
- [Analyzing the Narration Gap in LLM-Solver Loops](https://mlsanity.com/paper/2606.19588/) (2026)
- [Privilege and confidentiality in generative AI workflows](https://mlsanity.com/paper/2607.05479/) (2026)

## Abstract (arXiv)

Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a it re-ranking approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in urlhttps://github.com/microsoft/NeuralInvariantRanker.