# Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods

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

## 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 (most cited first, 15 of 15)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Embers of Autoregression: Understanding Large Language Models Through the Problem They are Trained to Solve](https://mlsanity.com/paper/2309.13638/) (2023)
- [Large Language Models Understand and Can be Enhanced by Emotional Stimuli](https://mlsanity.com/paper/2307.11760/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Synthesize, Execute and Debug: Learning to Repair for Neural Program Synthesis](https://mlsanity.com/paper/2007.08095/) (2020)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [LLMSTEP: LLM proofstep suggestions in Lean](https://mlsanity.com/paper/2310.18457/) (2023)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [The Counterfeit Conundrum: Can Code Language Models Grasp the Nuances of Their Incorrect Generations?](https://mlsanity.com/paper/2402.19475/) (2024)
- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)
- [Leveraging Large Language Models to Boost Dafny's Developers Productivity](https://mlsanity.com/paper/2401.00963/) (2024)

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

- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)
- [Graph Construction and Matching for Imperative Programs using Neural and Structural Methods](https://mlsanity.com/paper/2604.26578/) (2026)
- [AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis](https://mlsanity.com/paper/2606.20969/) (2026)
- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)

## 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.