mlsanityData to 14 Oct 2026

Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods

arXiv 2406.15540 ↗First posted 21 Jun 2024cs.SE cs.FL cs.LGcited by 6

Not on the map. Why?

Abstract (arXiv)

We investigate how combinations of Large Language Models (LLMs) and symbolic analyses can be used to synthesise specifications of C programs. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA, to produce C program annotations in the specification language ACSL. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations: information about input/output examples from Pathcrawler produce more context-aware annotations, while the inclusion of EVA reports yields annotations more attuned to runtime errors. In addition, we show that the method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs.

Key facts. Cited by 6 papers in the map (data through 14 Oct 2026). Builds on 15 of its 48 references that are in the map. First posted on arXiv 21 Jun 2024.

Builds on

15 of 48 references.

References · 15

  1. 2020Language Models are Few-Shot Learnerscited by 32,419
  2. 2023A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPTcited by 619
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  4. 2023Embers of Autoregression: Understanding Large Language Models Through the Problem They are Trained to Solvecited by 178
  5. 2023Large Language Models Understand and Can be Enhanced by Emotional Stimulicited by 146
  6. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  7. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  8. 2020Synthesize, Execute and Debug: Learning to Repair for Neural Program Synthesiscited by 39
  9. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 36
  10. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  11. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  12. 2020The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coqcited by 24
3 more
  1. 2024The Counterfeit Conundrum: Can Code Language Models Grasp the Nuances of Their Incorrect Generations?cited by 20
  2. 2023Can ChatGPT support software verification?cited by 14
  3. 2024Leveraging Large Language Models to Boost Dafny's Developers Productivitycited by 7

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 1; 2026: 5.

6 papers.

  1. 2025Formalising Software Requirements using Large Language Modelscited by 2
  2. 2026Evaluating LLM-Generated ACSL Annotations for Formal Verificationcited by 1
  3. 2026Talking with Verifiers: Automatic Specification Generation for Neural Network Verificationcited by 0
  4. 2026Graph Construction and Matching for Imperative Programs using Neural and Structural Methodscited by 0
  5. 2026AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysiscited by 0
  6. 2026Partial Contracts Suffice: Sound, LLM-Inferred Regression Verificationcited by 0