mlsanityData to 7 Oct 2026

Ranking LLM-Generated Loop Invariants for Program Verification

arXiv 2310.09342 ↗First posted 13 Oct 2023cs.PL cs.AI cs.CLcited by 33

Not on the map. Why?

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.

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

Builds on

9 of 37 references.

References · 9

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2022Training language models to follow instructions with human feedbackcited by 15,712
  3. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  4. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,304
  5. 2022Large Language Models are Zero-Shot Reasonerscited by 4,323
  6. 2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,779
  7. 2019CLN2INV: Learning Loop Invariants with Continuous Logic Networkscited by 20
  8. 2020Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)cited by 17
  9. 2017LoopInvGen: A Loop Invariant Generator based on Precondition Inferencecited by 3

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 2; 2024: 8; 2025: 13; 2026: 10.

33 papers.

Sort:

By area:

  1. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
  2. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  3. 2024LLMDFA: Analyzing Dataflow in Code with Large Language Modelscited by 22
  4. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  5. 2025Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inferencecited by 14
  6. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 10
  7. 2025A Contemporary Survey of Large Language Model Assisted Program Analysiscited by 10
  8. 2025Locus: Agentic Predicate Synthesis for Directed Fuzzingcited by 8
  9. 2024Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Modelscited by 7
  10. 2025On the Effectiveness of Large Language Models in Writing Alloy Formulascited by 7
  11. 2023XplainLLM: A Knowledge-Augmented Dataset for Reliable Grounded Explanations in LLMscited by 5
  12. 2025EditLord: Learning Code Transformation Rules for Code Editingcited by 4
21 more
  1. 2025Quokka: Accelerating Program Verification with LLMs via Invariant Synthesiscited by 4
  2. 2025Next Steps in LLM-Supported Java Verificationcited by 3
  3. 2025Agentic Specification Generator for Move Programscited by 3
  4. 2025Inferring multiple helper Dafny assertions with LLMscited by 3
  5. 2026AutoReSpec: A Framework for Generating Specification using Large Language Modelscited by 3
  6. 2024Towards Large Language Model Aided Program Refinementcited by 2
  7. 2026Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specificationscited by 2
  8. 2024Assured Automatic Programming via Large Language Modelscited by 1
  9. 2025Understanding Formal Reasoning Failures in LLMs as Abstract Interpreterscited by 1
  10. 2025CETBench: A Novel Dataset constructed via Transformations over Programs for Benchmarking LLMs for Code-Equivalence Checkingcited by 1
  11. 2025LLM For Loop Invariant Generation and Fixing: How Far Are We?cited by 1
  12. 2024Lucy: Think and Reason to Solve Text-to-SQLcited by 0
  13. 2025Exploring the Feasibility of End-to-End Large Language Model as a Compilercited by 0
  14. 2026Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMscited by 0
  15. 2026SpecPylot: Python Specification Generation using Large Language Modelscited by 0
  16. 2026Natural Language based Specification and Verificationcited by 0
  17. 2026Analyzing the Narration Gap in LLM-Solver Loopscited by 0
  18. 2026Privilege and confidentiality in generative AI workflowscited by 0
  19. 2026Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiabilitycited by 0
  20. 2026SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programscited by 0
  21. 2026Schwarz: Solver-Aware Agentic Program Verificationcited by 0