Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis

TL;DR

The paper tackles the challenge of automatically synthesizing formal specifications from C programs by pairing large language models with symbolic analysis tools. It examines whether LLMs can capture programmer intent versus implemented behavior and demonstrates that prompt design can guide the model toward the intended semantics, even with buggy code. By augmenting LLM prompts with outputs from PathCrawler (test-case generation) and EVA (value analysis), the authors show that symbolic context can reduce annotation noise and steer the synthesis toward more relevant preconditions or abstract postconditions. The work provides empirical evidence that neuro-symbolic prompting can improve specification usefulness and argues for integrating formal tools into LLM-driven verification pipelines, with implications for trustworthy, triad-cooperative development of implementations, tests, and specifications.

Abstract

This work is concerned with the generation of formal specifications from code, using Large Language Models (LLMs) in combination with symbolic methods. Concretely, in our study, the programming language is C, the specification language is ACSL, and the LLM is Deepseek-R1. In this context, we address two research directions, namely the specification of intent vs. implementation on the one hand, and the combination of symbolic analyses with LLMs on the other hand. For the first, we investigate how the absence or presence of bugs in the code impacts the generated specifications, as well as whether and how a user can direct the LLM to specify intent or implementation, respectively. For the second, we investigate the impact of results from symbolic analyses on the specifications generated by the LLM. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations.

Figures (21)

• Figure 1: Example PathCrawler input/outputs for BubbleSort
• Figure 2: Example EVA report
• Figure 3: Prompt used for generating ACSL annotations
• Figure 4: Prompt used for generating ACSL annotations with PathCrawler as additional context
• Figure 5: Prompt used for generating ACSL annotations with EVA as additional context