CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation

Zaoyu Chen; Jianbo Dai; Boyu Zhu; Jingdong Wang; Huiming Wang; Xin Xu; Haoyang Yuan; Zhijiang Guo

cs.SEApr 14, 2026

CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation

Authors: Zaoyu Chen, Jianbo Dai, Boyu Zhu, Jingdong Wang, Huiming Wang, Xin Xu, Haoyang Yuan, Zhijiang Guo,

Organizations: The Hong Kong Polytechnic University · University of Edinburgh · UCL · CUHK (SZ) ·

Abstract

Large language models (LLMs) can generate code from natural language, but the extent to which they capture intended program behavior remains unclear. Executable behavioral specifications, defined via preconditions and postconditions, provide a concrete means to assess such understanding. However, existing work on specification generation is constrained in evaluation methodology, task settings, and specification expressiveness. We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol. CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions. Constructed from diverse real-world codebases, it enables a realistic assessment of both correctness (accepting valid behaviors) and completeness (rejecting invalid behaviors). Evaluating 15 state-of-the-art LLMs on CodeSpecBench, we observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate. We further find that specification generation is substantially more challenging than code generation, indicating that strong coding performance does not necessarily reflect deep understanding of intended program semantics. Our data and code are available at https://github.com/SparksofAGI/CodeSpecBench.

Figures & tables

Figure 1: Example of a generated executable behavioral specification from natural language problem description, sourced from CodeSpecBench -Func.

Benchmark	Func/Repo	Pre/Post	Verify	Language	Repr
VERINA ( Ye et al., 2025 )	✓ / ✗	✓ / ✓	Static	Lean	Proposition
AutoSpec ( Wen et al., 2024 )	✓ / ✓	✓ / ✓	Static	ACSL	Annotation
SpecGenBench ( Ma et al., 2025 )	✓ / ✗	✓ / ✓	Static	JML	Annotation
FormalBench ( Le-Cong et al., 2025 )	✓ / ✗	✓ / ✓	Static	JML	Annotation
nl2postcond ( Endres et al., 2024 )	✓ / ✓	✗ / ✓	Execution	Python/Java	Assertion
CodeSpecBench	✓ / ✓	✓ / ✓	Execution	Python	Function

Table 1: Comparison of CodeSpecBench with representative specification-generation benchmarks along key dimensions, including granularity (function vs. repository), specification coverage (preconditions and postconditions), verification paradigm (static vs. execution-based), specification language and representation.

Figure 2: Overview of generation and evaluation in CodeSpecBench . In CodeSpecBench -Func (top), the specification is generated from a natural language problem description (top left) and executed on correct and incorrect test cases to evaluate correctness and completeness (top right). In CodeSpecBench -Repo (bottom), the specification is generated from a natural language issue description and relevant repository code (bottom left). Correctness is evaluated using trigger and regression tests on the fixed repository, while completeness is evaluated using trigger tests on the buggy repository (bottom right).

Figure 3: Overview of the test case construction process in CodeSpecBench -Func.

Table 5

Open-Weight Models
Model	Reasoning	CodeSpecBench -Func			CodeSpecBench -Repo
Model	Reasoning	Correct	Complete	Pass	Correct	Complete	Pass
Qwen3-0.6B	✗	8.4	11.6	0.2	0.0	0.0	0.0
Qwen3-0.6B	✓	5.2	17.2	0.2	0.0	0.0	0.0
Qwen3-1.7B	✗	8.1	20.8	0.8	0.2	0.2	0.0
Qwen3-1.7B	✓	14.7	11.1	1.2	0.0	0.0	0.0

Table 4: Results on the CodeSpecBench -Func and CodeSpecBench -Repo benchmarks (percentages). Correct, Complete, and Pass report correctness, completeness, and pass rate under the benchmark’s execution-based evaluation protocol, respectively. Reasoning indicates whether the thinking mode is enabled.

Table 7

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Error Type	GPT-5-mini	GPT-OSS-120B
Output Mismatches	21.5%	23.7%
Relational Violations	5.6%	6.2%
Type Violations	24.9%	31.8%
Range Violations	23.3%	22.5%
Structural Violations	8.3%	10.3%
Interface Errors	16.2%	4.8%

Appendix

Table 7: Distribution of error categories among failed test cases on CodeSpecBench -Func.

Error Type	Claude	DeepSeek
Syntax Errors	2.7%	26.4%
Dependency Resolution	33.4%	26.4%
Signature Mismatch	8.7%	5.9%
Execution Environment Failures	8.0%	6.2%
Untriggered Instrumentation	12.4%	11.4%
Over-restrictive Specifications	18.7%	12.7%

Appendix

Table 8: Distribution of failure types on CodeSpecBench -Repo. Claude refers to Claude-4.5-Sonnet and DeepSeek refers to DeepSeek-V3.2.

Open-Weight Models
Model	Reasoning	CodeSpecBench -Func			CodeSpecBench -Repo
Model	Reasoning	Correct	Complete	Pass	Correct	Complete	Pass
Qwen3-0.6B	✗	13.2	55.5	7.0	0.0	0.0	0.0
Qwen3-0.6B	✓	7.7	63.4	4.1	0.0	0.0	0.0
Qwen3-1.7B	✗	13.2	77.9	10.5	0.4	0.2	0.3
Qwen3-1.7B	✓	19.9	75.5	16.5	0.0	0.0	0.0

Appendix

Table 9: Fraction-based evaluation results on the CodeSpecBench -Func and CodeSpecBench -Repo benchmarks (percentages).

Model	Reasoning	Executable	Pass
Qwen3-0.6B	✗	0.0	0.0
Qwen3-0.6B	✓	0.0	0.0
Qwen3-1.7B	✗	0.4	0.0
Qwen3-1.7B	✓	0.0	0.0
Qwen3-4B	✗	1.0	0.0
Qwen3-4B	✓	2.8	0.2

Appendix

Table 10: Full experimental results showing relationship between executable specification rate (Executable) and pass rate (Pass) on CodeSpecBench -Repo (values in %).

Figure 5: Distribution of prompt token lengths for CodeSpecBench -Repo, computed with the Qwen3 tokenizer. Each bar shows the proportion of inputs falling within a specific token length range.

Algorithmic Domain	Pass Rate	Algorithmic Domain	Pass Rate
Radix Sort	66.7	Geometry	59.4
Biconnected Component	66.7	Breadth-First Search	59.3
Bucket Sort	66.7	Monotonic Stack	59.1
Randomized	66.7	Backtracking	59.1
Suffix Array	66.5	Two Pointers	59.0
Merge Sort	66.4	Math	58.9

Appendix

Table 11: Postcondition pass rates (%) for 61 algorithmic domains under GPT-5-mini.

Model	Reasoning	Temperature	TopP	TopK	MinP
Qwen3 (0.6B–32B)	✗	0.7	0.8	20	0
Qwen3 (0.6B–32B)	✓	0.6	0.95	20	0
QWQ-32B	✓	0.6	0.95	20	0
GPT-OSS (20B–120B)	✓	1.0	1.0	–	–
DeepSeek-V3.2	✗	1.0	0.95	–	–

Appendix

Table 12: Sampling parameters for different models

LLM Evaluation

Large language model evaluation measures what models can do, how reliably they do it, and whether benchmark scores predict real-world performance.

See all 2,401 papers

Teaching Code LLMs to Reason with Intermediate Formal Specifications
Jul 5, 2026Minh Le-Anh, Cuong Chi Le, Tien N. NguyenFormal Verification Code Language Models
FPT Software AI Center Hanoi Univ. of Science and Tech. Hanoi, Vietnam · University of Texas at Dallas Texas, USA
Self-Spec Verifiable Code Generation
Sep 30, 2026Jiaru Qian, Yihong Dong, Yongmin Li +3LLM Self-Correction Code Generation
School of Computer Science, Peking University · Beijing Key Laboratory of Trustworthy Code Large Language Models · Key Laboratory of High Confidence Software Technologies, Peking University, Ministry of Education +3
Inferring Code Correctness from Specification
May 28, 2026Tambon Florian, Papadakis MikeAutomated Software Testing Code Generation Evaluation
University of Luxembourg Luxembourg, Luxembourg

Jul 5, 2026J/K move · Enter open · S save

Teaching Code LLMs to Reason with Intermediate Formal Specifications

Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen

FPT Software AI Center Hanoi Univ. of Science and Tech. Hanoi, Vietnam · University of Texas at Dallas Texas, USA

Formal Verification Code Language Models

Open paper AskPDF arXiv

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.

Abstract

LLM Evaluation

Explore similar work

Teaching Code LLMs to Reason with Intermediate Formal Specifications

Self-Spec Verifiable Code Generation

Inferring Code Correctness from Specification