CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation

1 Introduction

• Executable behavioral specifications characterize semantics through preconditions and postconditions, providing an explicit, executable interface for program behavior.They can also support solution verification and more precise communication between agents.Source: §1 · p. 1
• Existing approaches leave limited evidence about realistic specification generation because of constraints in evaluation, task settings, and specification scope.Prior work excludes repository tasks, relies on verification settings, or uses simple datasets and limited assertion forms without preconditions.Source: §1 · pp. 1–2
• CODESPECBENCH evaluates executable behavioral specifications at both function and repository levels, covering preconditions and postconditions in Python.It assesses correctness by accepting valid behaviors and completeness by rejecting invalid behaviors.Source: §1 · p. 2
• Across 15 LLMs, performance drops sharply from function-level tasks to repository-level tasks, where the best model achieves only a 20.2% pass rate.The passage attributes the repository-level errors primarily to dependency-resolution failures.Source: §1 · p. 2
• Specification generation is substantially more challenging than code generation, so strong code-generation performance does not necessarily imply deep understanding of intended behavior.Source: §1 · p. 2

2 Related Work

• Code-generation benchmarks assess implementations from natural-language descriptions, including repository-level work that requires dependency reasoning and project-specific tests.CODESPECBENCH instead asks models to capture intended behavior through explicit specifications rather than implement solutions.Source: §2 · pp. 2–3
• Specification-generation research includes template or trace-based methods, formal-language generation, verification-oriented benchmarks, and natural-language-to-assertion work.Source: §2 · p. 3
• CODESPECBENCH focuses on executable Python preconditions and postconditions, with execution-based evaluation at both function and repository levels.Table 1 compares benchmarks by granularity, specification coverage, verification paradigm, and representation.Source: §2 · p. 3, Table 1 · p. 3

3.1 Executable Behavioral Specification Generation

• Specifications are executable Python functions that combine preconditions and postconditions, allowing flexible expression and direct test-based evaluation.Preconditions constrain admissible inputs and relevant state; postconditions describe required outputs and resulting state.Source: §3.1 · pp. 3–4

3.2 Specification Generation at Different Granularities

• Function-level tasks provide only a natural-language description and require a precondition–postcondition pair for a self-contained problem without external dependencies.These specifications cover legal inputs and input–output relationships, not broader program state or interactions among functions.Source: §3.2 · p. 4
• Repository-level tasks provide an issue description, relevant code context, and modified-function signatures, requiring specifications that also constrain relevant program state and its changes.Source: §3.2 · p. 4

3.3 Execution-Based Evaluation of Generated Specifications

• At function level, generated specifications are executed against curated correct and incorrect test cases using a framework adapted from HumanEval.Source: §3.3 · p. 5
• At repository level, specifications are dynamically injected around issue-relevant functions: preconditions run before execution and postconditions after the function body.The instrumentation runs within the SWE-bench execution framework.Source: §3.3 · p. 5

3.4 Evaluation Metrics

• Correctness checks acceptance of all curated valid tests, while completeness checks rejection of all curated invalid tests.Repository-level valid tests are trigger and regression tests on fixed repositories; invalid tests are trigger tests on buggy repositories.Source: §3.4 · p. 5
• Pass rate is the proportion of generated specifications that satisfy both correctness and completeness; violating either criterion counts as failure.Source: §3.4 · p. 5

4 CODESPECBENCH

• CODESPECBENCH has two evaluation levels: CODESPECBENCH-Func for function tasks and CODESPECBENCH-Repo for repository issues.Source: §4 · p. 5

4.1 CODESPECBENCH-Func

• CODESPECBENCH-Func contains 2,494 publicly accessible problems from LeetCodeDataset and uses over 200 generated test cases per problem.Multiple LLMs generate valid and intentionally invalid inputs; online-judge validation supplies labels and ground-truth outputs.Source: §4.1 · pp. 5–6
• Incorrect output cases are constructed from mismatches between candidate solutions and online-judge outputs, yielding an average of 67.8 cases per problem.The candidates come from three models, and the cases evaluate postcondition completeness.Source: §4.1 · p. 6
• Generated function-level tests achieve 96.3% average statement coverage and 93.6% branch coverage.Source: §4.1 · p. 6

4.2 CODESPECBENCH-Repo

• Repository tasks use SWE-bench Verified issues grounded in large, multi-file Python projects, with buggy and fixed repositories plus trigger and regression tests.Source: §4.2 · pp. 6–7
• Repository evaluation adopts UTBoost's augmented test cases to address insufficient test coverage in SWE-bench instances.Source: §4.2 · p. 7

5.1 Experimental Setup

• The setup evaluates a diverse set of contemporary LLMs, with model and deployment details and the generation prompt provided in appendices.The supplied setup passage does not enumerate the models or deployment settings.Source: §5.1 · p. 7

5.2 Main Results

• 20.2% was the best CODESPECBENCH-Repo pass rate, compared with 47.0% for the best CODESPECBENCH-Func result.Claude-4.5-Sonnet led on Repo; GPT-5-mini led on Func.Source: §5.2 · p. 7, Table 4 · p. 8
• Qwen3 scaling and reasoning improved Func pass rates, but open-weight gains were weak on Repo, where proprietary models led.Qwen3-32B rose from 0.2% on Func at 0.6B to 25.8% with reasoning, but its Repo pass rate peaked at 2.0%; DeepSeek-V3.2 had the best open-weight Repo result at 6.8%.Source: §5.2 · pp. 7–8, Table 4 · p. 8
• On Func, correctness generally exceeded completeness, while Repo models showed the opposite pattern and low pass rates.For example, Gemini-2.5-Pro scored 88.1% correctness and 52.8% completeness on Func, versus 30.8% correctness and 53.0% completeness on Repo.Source: §5.2 · p. 8, Table 4 · p. 8

5.3 Analysis and Discussion

• On Func, Type and Range Violations made up 48–54% of failures; Repo failures centered on dependency resolution and over-restrictive specifications.The analysis identifies input constraints and grounding specifications in code context as major sources of errors.Source: §5.3 · p. 9
• Specification-guided re-ranking improved pass rates for both tested models, with larger gains at pass@1.Qwen3-8B rose from 59.4% to 62.2%, and Qwen3-32B from 71.2% to 73.9%.Source: §5.3 · p. 9, Table 5 · p. 9
• Solution-generation pass rates were high relative to executable specification-generation performance, showing that solving tasks does not necessarily entail precise behavioral constraints.The comparison uses solution pass rates from the models’ official technical reports.Source: §5.3 · p. 9, Table 6 · p. 9

• CodeSpecBench evaluates executable Python preconditions and postconditions at function and repository levels along correctness and completeness dimensions.Source: §6 · p. 9
• Experiments on 15 LLMs show substantial performance drops on repository-level tasks, and specification generation is significantly harder than code generation.The authors expect the benchmark and its analysis to support systematic assessment of intended-program-semantics understanding.Source: §6 · p. 10

Ethics Statement

• The benchmark uses publicly available datasets and open-source repositories, and executions are conducted in controlled environments to mitigate security risks.Source: Ethics Statement · p. 11

A.1 CODESPECBENCH-Func

• The function-level taxonomy includes type, range, structural, relational, output, interface, and runtime violations.Source: §A.1 · p. 15
• Type and Range Violations together account for 48–54% of failures in the function-level analysis, pointing to mis-specified input constraints.The analysis categorizes runtime failures encountered while executing generated specifications against test cases.Source: §A.1 · p. 15

A.2 CODESPECBENCH-Repo

• The repository taxonomy covers syntax, dependency-resolution, signature, environment, instrumentation, over-restriction, abstraction-violation, and representation-dependent errors.Dependency resolution means required imports or symbols are missing or undefined; over-restrictive specifications reject legitimate behavior.Source: §A.2 · p. 16
• Claude-4.5-Sonnet errors were led by dependency resolution (33.4%) and over-restrictive specifications (18.7%), while DeepSeek-V3.2 had 26.4% syntax errors and 26.4% dependency-resolution failures.Source: §A.2 · p. 16, Table 8 · p. 16

B CODESPECBENCH-Repo Example

• The appendix presents a SymPy issue in which solveset raises NotImplementedError instead of returning a ConditionSet, alongside relevant repository code.The example is introduced as an issue description and code paired with a generated executable behavioral specification.Source: B CODESPECBENCH-Repo Example · pp. 16–17

C Repository-level Specification Injection

• A generated conftest.py defines specification functions and a pytest_sessionstart hook that wraps the target, running preconditions before the call and postconditions after it returns.The generated file is placed at the repository root or appended to an existing conftest.py, activating the specifications when pytest starts.Source: C Repository-level Specification… · p. 17
• Django’s custom test runner requires appending the hook mechanism to setup_run_tests, while SymPy switches to pytest to support the same function-wrapping strategy.SymPy’s test-output parsing is also updated to match pytest’s format.Source: C Repository-level Specification… · p. 17
• Figure 4 illustrates a generated repository-level specification from a natural-language issue description and relevant repository code.Source: Figure 4 · p. 18

D Quality Assurance

• Each problem has 217.8 test cases, providing more evaluation signals than benchmarks with fewer cases per problem.Source: D Quality Assurance · p. 18
• Test inputs are checked against the official judge, and redundant inputs—including formatting-only variants—are removed.Incorrect output cases for postcondition completeness are built from candidate solutions generated by LLMs with diverse capability levels; repository instances also receive UTBoost tests to address known coverage gaps.Source: D Quality Assurance · p. 19
• Generated tests average 96.3% statement coverage and 93.6% branch coverage, exercising a wide range of program behaviors.Source: D Quality Assurance · p. 19

E Fraction-Based Evaluation Metrics

• Strict pass rate requires a specification to accept every correct test and reject every incorrect test; a single failing test makes the metric coarse.Fraction-based metrics separately measure the shares of correct tests accepted and incorrect tests rejected, then combine correctness and completeness using their harmonic mean.Source: E Fraction-Based Evaluation Metrics · pp. 19–20
• Fraction-based measures capture partial success and typically preserve the ranking trends and scaling behaviors of strict evaluation, especially on challenging repository tasks.Many repository-level outputs fail strict criteria while differing in how many tests they satisfy.Source: E Fraction-Based Evaluation Metrics · p. 20

F Syntactic Executability as a Key Bottleneck

• 9.8% of Qwen3-8B-Thinking specifications are syntactically executable, while GPT-5 and Claude-4.5-Sonnet reach 77.6% and 82.0%, respectively; executability positively correlates with pass rate.For stronger models, high executability still leaves repository pass rates limited, with remaining challenges in understanding repository behavior and expressing accurate constraints.Source: F Syntactic Executability as a Key… · pp. 20–21

G Impact of Prompt Length and Context Window

• 84.8% of repository prompts are at most 32k tokens, 14.2% fall in 32k–128k, and about 1% are at least 128k; 32k-context models have lower pass rates on the long tail.128k-context models accommodate nearly all inputs and perform more stably as prompt length increases, while 200k–272k contexts yield only marginal average gains.Source: G Impact of Prompt Length and Context… · p. 21, Figure 5 · p. 21

H Postcondition Pass Rates Across Algorithmic Domains

• Sorting tasks average approximately 66% postcondition pass rate, compared with 47.9% for Tree, 46.2% for Binary Tree, 28.4% for Strongly Connected Component, and 22.2% for Binary Search Tree.Failures concentrate in domains requiring global structural properties or recursive invariants; locally verifiable output properties are handled more reliably.Source: H Postcondition Pass Rates Across… · p. 21

I.1 Prompt for Test Case Generation / I.2 Prompt for Solution Generation

• The test-generation prompt requests 30 inputs mixing valid and invalid cases, while the solution-generation prompt asks for an implementation adhering to starter code.Source: §I.1 · p. 22, §I.2 · p. 23

I.3.1 Prompt for Specification Generation in CODESPECBENCH-Func

• For function-level tasks, models implement preconditions and postconditions using only assert statements, without returning values.Preconditions check input validity; postconditions check output correctness against the problem’s expected behavior.Source: §I.3.1 · p. 23

I.3.2 Prompt for Specification Generation in CODESPECBENCH-Repo

• Repository-level prompts provide an issue and relevant code, then require a conftest.py hook that wraps the target function to check behavior against the issue.The supplied files use the SWE-bench Verified Oracle setting, which provides files modified by the ground-truth issue patch.Source: §I.3.2 · p. 24

K Limitations

• Execution on curated function tests and repository trigger/regression tests is only an approximation, so passing specifications may remain unsound or incomplete on untested behaviors.Richer test suites could improve the approximation but would not provide full functional-correctness guarantees.Source: K Limitations · p. 25
• CODESPECBENCH-Func depends on an external online judge to validate inputs and obtain reference outputs, limiting the construction pipeline’s self-containment and reproducibility.The pipeline depends on the service’s long-term availability.Source: K Limitations · p. 25
• Specifications are represented exclusively as executable Python preconditions and postconditions, restricting the benchmark to one programming language.Support for other specification languages remains future work.Source: K Limitations · p. 25