Teaching Code LLMs to Reason with Intermediate Formal Specifications

• URL: http://arxiv.org/abs/2607.04232v1
• Date: Sun, 05 Jul 2026 11:09:30 GMT
• Title: Teaching Code LLMs to Reason with Intermediate Formal Specifications
• Abstract summary: 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.
• Score: 9.552020178028576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.

Related papers

• SpecCoder: Specification-Aware Code Generation with Curriculum Dual-Task Reinforcement Learning [30.588079618949447]
  SpecCoder is a specification-aware two-stage training framework for code generation.<n>It first employs specification-guided SFT to train GRPs to derive structured specification analyses and generate code conditioned on them.<n>It then introduces curriculum dual-taskO, which jointly optimize specification-guided generation and discrimination to encourage stronger correspondence between specifications and code behavior.
  arXiv  Detail & Related papers  (2026-09-05T11:52:54Z)
• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy [14.535794931718229]
  This study is a significant undertaking to enable the systematic validation of open-source SLEIGH language specifications.<n>We design and implement a testing framework based on an automated oracle validation strategy by proxy.<n>Applying InSPECtor across diverse, open-source specifications, we uncovered over 38,920 discrepancies that led to 125 unique bugs.
  arXiv  Detail & Related papers  (2026-08-13T10:08:41Z)
• 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)
• POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference [10.01438318022033]
  We introduce POSTCONDBENCH, a benchmark for evaluating method-level postcondition generation from real-world software.<n>To enable automatic evaluation, POSTCONDBENCH provides a runnable execution environment and operationalizes completeness via defect discrimination.<n>Our results reveal a substantial gap between correctness and completeness, and show that repository-level dependencies and method complexity exacerbate this gap.
  arXiv  Detail & Related papers  (2026-05-05T04:29:38Z)
• 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)
• 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)
• 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)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
  We introduce a new benchmark for formal verification of Large Language Models (LLMs)<n>Our framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code.<n>Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs.
  arXiv  Detail & Related papers  (2025-10-07T13:19:05Z)
• From Benchmark Data To Applicable Program Repair: An Experience Report [1.6913109767046948]
  This paper describes our approach to automated program repair.<n>We combine various techniques from the literature to achieve this.<n>Experiments show that our approach performs better than other techniques on standard benchmarks.<n>On closer inspection, none of these techniques work on realistic defects that we see in industry.
  arXiv  Detail & Related papers  (2025-08-22T03:59:27Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• 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)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)

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.