Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications

• URL: http://arxiv.org/abs/2603.13414v1
• Date: Thu, 12 Mar 2026 15:02:26 GMT
• Title: Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
• Abstract summary: Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts.<n>We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs.<n>We introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications.
• Score: 12.783777562919383
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become a major bottleneck as large language models (LLMs) increasingly generate low-level systems code whose correctness cannot be assumed. To enable scalable formal verification, we focus exclusively on function specification generation, deliberately avoiding the synthesis of complex loop invariants that are central to traditional verification pipelines. We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs from natural language problem descriptions and function signatures. The pipeline first produces candidate specifications via in-context learning, and then iteratively refines them using compiler diagnostics from symbolic provers and the verification toolchain. In particular, we validate candidate specifications by constructing a proof for the negation of the specification with concrete examples, enabling machine-checked rejection of plausible-but-incorrect specifications. To support systematic evaluation, we introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications. Experiments show that iterative refinement substantially improves syntactic validity, while symbolic prover-based refutation significantly enhances correctness assessment by filtering false positives that LLM-only judges frequently accept. Our results demonstrate that combining neural generation with symbolic feedback provides an effective approach to formal specification synthesis for memory-safe systems software.

Related papers

• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• Agentic Separation Logic Specification Synthesis [4.177196802192322]
  Spec-Agent is an agentic system for synthesizing expressive, well-validated specifications across large C++s.<n>For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language.<n>We evaluate Spec-Agent on open source C++s comprising millions of lines of code.
  arXiv  Detail & Related papers  (2026-05-26T18:05:42Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Autoformalizing Memory Specifications with Agents [3.897906533095668]
  We show how to formalize memory chip specifications into a formal representation called DRAMPyML.<n>This can be used for the generation of SystemVerilog assertions, stimulus, and functional coverage.<n>We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities.
  arXiv  Detail & Related papers  (2026-04-30T02:01:48Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  We introduce a new error taxonomy grounded in problem solvability, inspired by cognitive theory.<n>Our taxonomy categorizes failures into syntactic, semantic, solvable functional, and unsolvable functional types.
  arXiv  Detail & Related papers  (2026-04-26T14:34:49Z)
• Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study [0.0]
  This paper studies feedback-based automated verification of LLM-generated adaptation managers in Collective Adaptive Systems (CAS)<n>We focus on the key challenges of verification in the loop: how to detect failures of generated code at runtime and how to report them.<n>Our findings suggest that feedback precision is the dominant factor for reliable vibe coding in systems designed by domain experts with no programming skills.
  arXiv  Detail & Related papers  (2026-04-16T10:58:03Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  We compare classical and prompt-based approaches for automated JML specification synthesis.<n>We investigate whether prompt optimization can push synthesis quality further by evolving prompts through structured verification feedback.<n>We propose VeriAct, a verification-guided agentic framework that iteratively synthesizes and repairs specifications.
  arXiv  Detail & Related papers  (2026-03-31T22:12:15Z)
• Understanding Contextual Recall in Transformers: How Finetuning Enables In-Context Reasoning over Pretraining Knowledge [50.009682083079205]
  We investigate whether contextual recall emerges from pretraining alone.<n>We show that finetuning on tasks requiring implicit inference, distinct from the ICL evaluation, triggers the emergence of contextual recall.<n>For mechanistic insight, we derive a construction for an attention-only transformer that replicates the transition from factual to contextual recall.
  arXiv  Detail & Related papers  (2026-03-21T22:46:55Z)
• CodeCircuit: Toward Inferring LLM-Generated Code Correctness via Attribution Graphs [13.488544043942495]
  We aim to investigate whether the model's neural dynamics encode internally decodable signals that are predictive of logical validity during code generation.<n>By decomposing complex residual flows, we aim to identify the structural signatures that distinguish sound reasoning from logical failure.<n>Analysis across Python, C++, and Java confirms that intrinsic correctness signals are robust across diverse syntaxes.
  arXiv  Detail & Related papers  (2026-02-06T03:49:15Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  Speculative decoding accelerates autoregressive language model inference by verifying multiple draft tokens in parallel.<n>Existing sparsification methods are designed primarily for standard token-by-token autoregressive decoding.<n>We propose a sparse verification framework that jointly sparsifies attention, FFN, and MoE components during the verification stage to reduce the dominant computation cost.
  arXiv  Detail & Related papers  (2025-12-26T07:53:41Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• Position: Intelligent Coding Systems Should Write Programs with Justifications [9.304020701255093]
  We argue that these systems should not only generate code but also produce clear, consistent justifications that bridge model reasoning and user understanding.<n>We advocate exploring neuro-symbolic approaches for justification generation, where symbolic constraints guide behavior during training and program semantics are enriched through neural representations.
  arXiv  Detail & Related papers  (2025-08-08T05:04:47Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  This paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast.<n>Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable.
  arXiv  Detail & Related papers  (2024-11-04T17:44:11Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries.<n>We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language.<n>We then build a binary code similarity model (FoC-Sim) upon the FoC-BinLLM to create change-sensitive representations and use it to retrieve similar implementations of unknown cryptographic functions in a database.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.