Intent-aligned Formal Specification Synthesis via Traceable Refinement

• URL: http://arxiv.org/abs/2604.10392v1
• Date: Sun, 12 Apr 2026 00:52:27 GMT
• Title: Intent-aligned Formal Specification Synthesis via Traceable Refinement
• Abstract summary: We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair.<n>VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps.<n>We achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales.
• Score: 43.72968325799861
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obtain such guarantees by proving that a program satisfies a formal specification. However, specifications are frequently missing in real-world codebases, and writing high-quality specifications remains expensive and expertise-intensive. We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair. VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps to validate generated specifications. When validation fails, traceability maps attribute failures to specific requirements, enabling targeted clause-level repairs. VeriSpecGen achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales. Beyond inference-time gains, we generate 343K training examples from VeriSpecGen refinement trajectories and demonstrate that training on these trajectories substantially improves specification synthesis by 62-106% relative and transfers gains to general reasoning abilities.

Related papers

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation.<n>We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions.<n>We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references.
  arXiv  Detail & Related papers  (2026-09-09T17:59:04Z)
• How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
  Coins is an evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations.<n>We conduct a large scale study on HumanEval with a curated set of human written Rocq specifications.<n>Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality.
  arXiv  Detail & Related papers  (2026-08-13T10:45:18Z)
• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoder is a training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces.<n> SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence.
  arXiv  Detail & Related papers  (2026-07-05T11:09:30Z)
• SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
  We propose specification-grounded alignment, a new alignment paradigm that treats provider-authored model specifications as the primary alignment target.<n>We introduce SpecAlign, a framework that synthesizes alignment data directly from specification documents.
  arXiv  Detail & Related papers  (2026-06-15T06:30:52Z)
• VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation [2.2194977808724405]
  Large language models can generate useful code from natural language, but their outputs come without correctness guarantees.<n>Verifiable code generation offers a path beyond testing by requiring models to produce not only executable code, but also formal specifications and machine-checkable proofs.<n>We present VeriContest, a benchmark of 946 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus.
  arXiv  Detail & Related papers  (2026-05-08T23:25:05Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  Large Language Models show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code.<n>We provide the NaturalLanguage2VerifiedCode dataset: a collection of 60 complex algorithmic problems.<n>We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy.<n>Our results show that while contextless prompting leads to near-universal failure, structural anchors and iterative self-healing facilitate a dramatic performance turnaround.
  arXiv  Detail & Related papers  (2026-04-24T14:28:10Z)
• SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification [10.586396714718457]
  SpecSyn is a novel LLM-based specification generation method.<n>In experiments, SpecSyn maintains high precision over 90% and outstanding recall over 75%.<n>In further evaluations, SpecSyn successfully handles 1071 out of 1365 target properties for open-source programs.
  arXiv  Detail & Related papers  (2026-04-23T11:46:19Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol.<n>CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions.<n>We observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate.
  arXiv  Detail & Related papers  (2026-04-14T04:31:45Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  We present an APR tool for Dafny that uses formal specifications as oracles for fault localization and repair.<n>We localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program.<n>Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  Large language models (LLMs) are increasingly integrated in software development.<n> Ensuring correctness in LLM-generated code remains challenging.<n>Verifiable code generation offers a promising path to address this limitation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGen is a novel technique for formal program specification generation based on Large Language Models.<n>We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
  arXiv  Detail & Related papers  (2024-01-16T20:13:50Z)

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.