# LLM For Loop Invariant Generation and Fixing: How Far Are We?

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 58 references that are in the map.
- First posted on arXiv 9 Nov 2025.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [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)
- [A Survey on Evaluation of Large Language Models](https://mlsanity.com/paper/2307.03109/) (2023)
- [Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm](https://mlsanity.com/paper/2102.07350/) (2021)
- [Evaluating Large Language Models at Evaluating Instruction Following](https://mlsanity.com/paper/2310.07641/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Customizing Language Model Responses with Contrastive In-Context Learning](https://mlsanity.com/paper/2401.17390/) (2024)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [Divide-or-Conquer? Which Part Should You Distill Your LLM?](https://mlsanity.com/paper/2402.15000/) (2024)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [The Impact of Example Selection in Few-Shot Prompting on Automated Essay Scoring Using GPT Models](https://mlsanity.com/paper/2411.18924/) (2024)
- [SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic](https://mlsanity.com/paper/1903.09713/) (2019)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [How much do LLMs learn from negative examples?](https://mlsanity.com/paper/2503.14391/) (2025)
- [LoopInvGen: A Loop Invariant Generator based on Precondition Inference](https://mlsanity.com/paper/1707.02029/) (2017)
- [Ilinva: Using Abduction to Generate Loop Invariants](https://mlsanity.com/paper/1906.11033/) (2019)
- [An Empirical Study of the Effectiveness of an Ensemble of Stand-alone Sentiment Detection Tools for Software Engineering Datasets](https://mlsanity.com/paper/2111.03196/) (2021)

## Built on by (most cited first, 1 of 1)

- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)

## Abstract (arXiv)

A loop invariant is a property of a loop that remains true before and after each execution of the loop. The identification of loop invariants is a critical step to support automated program safety assessment. Recent advancements in Large Language Models (LLMs) have demonstrated potential in diverse software engineering (SE) and formal verification tasks. However, we are not aware of the performance of LLMs to infer loop invariants. We report an empirical study of both open-source and closed-source LLMs of varying sizes to assess their proficiency in inferring inductive loop invariants for programs and in fixing incorrect invariants. Our findings reveal that while LLMs exhibit some utility in inferring and repairing loop invariants, their performance is substantially enhanced when supplemented with auxiliary information such as domain knowledge and illustrative examples. LLMs achieve a maximum success rate of 78% in generating, but are limited to 16% in repairing the invariant.