mlsanityData to 7 Oct 2026

Lemur: Integrating Large Language Models in Automated Program Verification

arXiv 2310.04870 ↗First posted 7 Oct 2023cs.FL cs.AI cs.LGcited by 49

Not on the map. Why?

Abstract (arXiv)

The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.

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

Builds on

9 of 29 references.

References · 9

  1. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  2. 2020Language Models are Few-Shot Learnerscited by 32,199
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  4. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  5. 2022Competition-Level Code Generation with AlphaCodecited by 1,427
  6. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  7. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  8. 2023A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verificationcited by 42
  9. 2017Sorting and Transforming Program Repair Ingredients via Deep Learning Code Similaritiescited by 26

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 1; 2024: 8; 2025: 20; 2026: 20.

49 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  2. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  3. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  4. 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
  5. 2025Frontier AI's Impact on the Cybersecurity Landscapecited by 21
  6. 2025A Contemporary Survey of Large Language Model Assisted Program Analysiscited by 10
  7. 2025Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planningcited by 10
  8. 2024Guiding Enumerative Program Synthesis with Large Language Modelscited by 9
  9. 2024MCP-Solver: Integrating Language Models with Constraint Programming Systemscited by 9
  10. 2025VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Veruscited by 8
  11. 2024Generating Streamlining Constraints with Large Language Modelscited by 7
  12. 2025Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overviewcited by 7
37 more
  1. 2025Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verificationcited by 6
  2. 2025Quokka: Accelerating Program Verification with LLMs via Invariant Synthesiscited by 4
  3. 2025Next Steps in LLM-Supported Java Verificationcited by 3
  4. 2025Integrating Expert Knowledge into Logical Programs via LLMscited by 3
  5. 2025PAT-Agent: Autoformalization for Model Checkingcited by 3
  6. 2025Inferring multiple helper Dafny assertions with LLMscited by 3
  7. 2026Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repaircited by 3
  8. 2024Generative transformations and patterns in LLM-native approaches for software verification and falsificationcited by 2
  9. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  10. 2026Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capabilitycited by 2
  11. 2025Towards Automated Formal Verification of Backend Systems with LLMscited by 1
  12. 2025LLM For Loop Invariant Generation and Fixing: How Far Are We?cited by 1
  13. 2025Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systemscited by 1
  14. 2025The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guaranteecited by 1
  15. 2026Evaluating LLM-Generated ACSL Annotations for Formal Verificationcited by 1
  16. 2026ExVerus: Verus Proof Repair via Counterexample Reasoningcited by 1
  17. 2026Fidelity Probes for Specification--Code Alignmentcited by 1
  18. 2024Lucy: Think and Reason to Solve Text-to-SQLcited by 0
  19. 2025From Scientific Texts to Verifiable Code: Automating the Process with Transformerscited by 0
  20. 2025LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditionscited by 0
  21. 2025Automated Type Annotation in Python Using Large Language Modelscited by 0
  22. 2025AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolutioncited by 0
  23. 2025A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoningcited by 0
  24. 2026Teaching LLMs Program Semantics via Symbolic Execution Tracescited by 0
  25. 2026Natural Language based Specification and Verificationcited by 0
  26. 2026Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysiscited by 0
  27. 2026Viverra: Text-to-Code with Guaranteescited by 0
  28. 2026Streamlined Constraint Reasoning via CNN Pattern Recognition on Enumerated Solutionscited by 0
  29. 2026Agentic Model Checkingcited by 0
  30. 2026Privilege and confidentiality in generative AI workflowscited by 0
  31. 2026Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiabilitycited by 0
  32. 2026Bulkhead: Automated Semantic Detection and Remediation of Container Escape Vulnerabilitiescited by 0
  33. 2026VeriSkill: A Self-Evolution Framework for Program Verification Skillscited by 0
  34. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  35. 2026Position: Reasoning is a Learnable Rule-Based Processcited by 0
  36. 2026When Does Structured Knowledge Help Neural Theorem Proving?cited by 0
  37. 2026From Verification Failures to Reusable Guidance for Coding Agentscited by 0