# Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 53 references that are in the map.
- First posted on arXiv 13 Dec 2024.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Pre-train, Prompt, and Predict: A Systematic Survey of Prompting Methods in Natural Language Processing](https://mlsanity.com/paper/2107.13586/) (2021)
- [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023)
- [CodePlan: Repository-level Coding using LLMs and Planning](https://mlsanity.com/paper/2309.12499/) (2023)
- [IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities](https://mlsanity.com/paper/2405.17238/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [A Quantitative and Qualitative Evaluation of LLM-Based Explainable Fault Localization](https://mlsanity.com/paper/2308.05487/) (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)
- [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)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic](https://mlsanity.com/paper/1903.09713/) (2019)
- [Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation](https://mlsanity.com/paper/2311.10483/) (2023)
- [Polynomial invariants by linear algebra](https://mlsanity.com/paper/1611.07726/) (2016)

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

- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters](https://mlsanity.com/paper/2503.12686/) (2025)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)
- [Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification](https://mlsanity.com/paper/2511.00202/) (2025)
- [Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs](https://mlsanity.com/paper/2603.15510/) (2026)
- [Agentic Model Checking](https://mlsanity.com/paper/2605.21434/) (2026)
- [Privilege and confidentiality in generative AI workflows](https://mlsanity.com/paper/2607.05479/) (2026)

## Abstract (arXiv)

Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, the automation of loop invariant analysis has effectively resolved the problem. However, real-world programs that often mix complex data structures and control flows pose challenges to traditional loop invariant generation tools. To enhance the applicability of invariant generation techniques, we proposed ACInv, an Automated Complex program loop Invariant generation tool, which combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We utilize static analysis to extract the necessary information for each loop and embed it into prompts for the LLM to generate invariants for each loop. Subsequently, we employ an LLM-based evaluator to assess the generated invariants, refining them by either strengthening, weakening, or rejecting them based on their correctness, ultimately obtaining enhanced invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures, and maintained similar performance to the state-of-the-art tool AutoSpec on numerical programs without data structures. For the total data set, ACInv can solve 21% more examples than AutoSpec and can generate reference data structure templates.