BeSpec: Behavior-Level Specification Alignment for Code Generation

• URL: http://arxiv.org/abs/2607.02949v1
• Date: Fri, 03 Jul 2026 04:48:45 GMT
• Title: BeSpec: Behavior-Level Specification Alignment for Code Generation
• Abstract summary: This paper presents BeSpec, a behavioral model-based approach to specification alignment.<n>BeSpec treats the task description as partial evidence about the intended behavior of the correct program.<n>It generates candidate programs, executes them on probe inputs, and compares their observed behavior with the predicted behaviors.
• Score: 2.9611475619490633
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLMs have made substantial progress on automated code generation from natural-language descriptions of desired behavior (intent). Most existing methods improve generated programs through execution-guided code refinement: they generate a candidate solution, execute it, and patch the implementation using feedback, while leaving the underlying specification unchanged. This workflow implicitly assumes that the LLM's understanding of the intent is already correct and complete. In practice, however, intents are often ambiguous or underspecified. As a result, even a capable model may produce a correct implementation of the wrong intent, making specification mismatch a central bottleneck. This paper presents BeSpec, a behavioral model-based approach to specification alignment. BeSpec treats the task description as partial evidence about the intended behavior of the correct program. It first builds an explicit behavioral model, which are checkable properties that valid outputs must satisfy. BeSpec then generates candidate programs, executes them on probe inputs, and compares their observed behavior with the predicted behaviors. When observed behavior does not match the predicted behaviors, BeSpec either refines the specification or rejects the candidate program. We evaluate BeSpec with three LLMs on four benchmarks: CodeContests, xCodeEval, APPS, and the contamination-free LiveCodeBench. Against nine baselines, BeSpec achieves the highest Pass@1 and average pass rate across all settings, improving average Pass@1 over the strongest baseline by 8.1%--25.3% relative across the three LLMs. A failure analysis shows that after alignment, most remaining errors stem from algorithmic difficulty rather than misunderstood specifications, while ablation studies confirm that each major component of BeSpec contributes positively.

Related papers

• SpecFirst: Behavioral Specification Elicitation as a First-Class Step in Agent-Based Program Synthesis from Scratch [17.260324148993046]
  LLM-based agents excel at software engineering tasks where an existing context provides context, but constructing a program from scratch remains fundamentally harder.<n>Existing frameworks conflate documentation reading, behavioral exploration, and code synthesis into a single pass.<n>We present SpecFirst, a two-stage framework that forces the specification elicitation before code synthesis.
  arXiv  Detail & Related papers  (2026-07-29T17:42:47Z)
• 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)
• Underspecification does not imply Incoherence: The Risks of Semantic Collapse in Coding Models [6.72873429875663]
  Large Language Models (LLMs) have become increasingly effective at generating code when task descriptions are clear and precise.<n>Yet, user-provided task descriptions are often ambiguous, incomplete, or contradictory, leaving critical aspects of the intended program behavior underspecified.<n>We find that LLMs frequently collapse onto a single incorrect interpretation of the task description, consistently generating coherent but behaviorally misaligned code.
  arXiv  Detail & Related papers  (2026-07-02T09:43:15Z)
• Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
  We study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications.<n>We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems.<n>Our analysis of failure modes shows that model-generated specs can accept important input assumptions, accept incorrect outputs, & reject valid ones.
  arXiv  Detail & Related papers  (2026-05-26T02:12:48Z)
• 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)
• DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode [56.14374797825548]
  We introduce LLM-based pseudocode execution, which grounds prediction on more error-resilient pseudocode.<n>We propose DuET, a dual-execution framework that combines both approaches by functional majority voting.<n>On LiveCodeBench, DuET achieves the state-of-the-art performance, improving Pass@1 by 13.6 pp.
  arXiv  Detail & Related papers  (2026-04-13T14:18:58Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  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.
  arXiv  Detail & Related papers  (2026-04-12T00:52:27Z)
• AutoReSpec: A Framework for Generating Specification using Large Language Models [1.0026496861838448]
  Large Language Models (LLMs) have shown promise in formal specification generation, but early results reveal several limitations.<n>We present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation.<n>We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs.
  arXiv  Detail & Related papers  (2026-04-04T15:17:08Z)
• Do AI models help produce verified bug fixes? [62.985237003585674]
  Large Language Models are used to produce corrections to software bugs.<n>This paper investigates how programmers use Large Language Models to complement their own skills.<n>The results are a first step towards a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs.
  arXiv  Detail & Related papers  (2025-07-21T17:30:16Z)
• Teaching Your Models to Understand Code via Focal Preference Alignment [70.71693365502212]
  In existing approaches, a set of n candidate solutions is evaluated based on test case success rates.<n>Because this approach aligns entire failing code blocks rather than pinpointing specific errors, it lacks the granularity necessary to capture meaningful error-correction relationships.<n>We propose Target-DPO, a new preference alignment framework that mimics human iterative debug to refine Code LLMs.
  arXiv  Detail & Related papers  (2025-03-04T16:56:34Z)
• ImbSAM: A Closer Look at Sharpness-Aware Minimization in Class-Imbalanced Recognition [62.20538402226608]
  We show that the Sharpness-Aware Minimization (SAM) fails to address generalization issues under the class-imbalanced setting. We propose a class-aware smoothness optimization algorithm named Imbalanced-SAM (ImbSAM) to overcome this bottleneck. Our ImbSAM demonstrates remarkable performance improvements for tail classes and anomaly.
  arXiv  Detail & Related papers  (2023-08-15T14:46:32Z)
• Contrastive Retrospection: honing in on critical steps for rapid learning and generalization in RL [44.436494923745734]
  We present a new reinforcement learning algorithm that uses offline contrastive learning to hone in on critical steps. This algorithm, which we call Contrastive Retrospection (ConSpec), can be added to any existing RL algorithm.
  arXiv  Detail & Related papers  (2022-10-12T00:35:45Z)

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.