CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation

📄 arXiv: 2604.12268v1 📥 PDF

作者: Zaoyu Chen, Jianbo Dai, Boyu Zhu, Jingdong Wang, Huiming Wang, Xin Xu, Haoyang Yuan, Zhijiang Guo, Xiao-Ming Wu

分类: cs.SE, cs.CL

发布日期: 2026-04-14

🔗 代码/项目: GITHUB

💡 一句话要点

CodeSpecBench：用于评估LLM生成可执行行为规范能力的基准测试

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 行为规范生成 基准测试 代码生成 程序理解 软件工程 可执行规范

📋 核心要点

  1. 现有规范生成工作在评估方法、任务设置和规范表达方面存在局限性，难以全面评估LLM对程序行为的理解。
  2. CodeSpecBench通过构建函数级和仓库级的可执行Python规范，并采用基于执行的评估协议，来解决上述问题。
  3. 实验表明，LLM在仓库级任务上性能显著下降，且规范生成比代码生成更具挑战性，揭示了LLM理解程序语义的不足。

📝 摘要（中文）

大型语言模型（LLM）可以从自然语言生成代码，但它们在多大程度上捕捉了预期的程序行为仍不清楚。可执行的行为规范，通过前置条件和后置条件定义，提供了一种评估这种理解的具体方法。然而，现有的规范生成工作在评估方法、任务设置和规范表达方面受到限制。我们引入了CodeSpecBench，这是一个在基于执行的评估协议下，用于可执行行为规范生成的基准测试。CodeSpecBench支持函数级别和仓库级别的任务，并将规范编码为可执行的Python函数。它构建于各种真实世界的代码库，能够对正确性（接受有效的行为）和完整性（拒绝无效的行为）进行现实的评估。在CodeSpecBench上评估了15个最先进的LLM，我们观察到仓库级别任务的性能急剧下降，最好的模型仅达到20.2%的通过率。我们进一步发现，规范生成比代码生成更具挑战性，这表明强大的编码性能并不一定反映对预期程序语义的深刻理解。我们的数据和代码可在https://github.com/SparksofAGI/CodeSpecBench获得。

🔬 方法详解

问题定义：论文旨在解决如何有效评估大型语言模型（LLM）理解程序行为意图的问题。现有方法在评估规范生成任务时，存在评估方法不完善、任务设置不够真实、规范表达能力有限等痛点，难以准确衡量LLM对程序语义的理解程度。

核心思路：论文的核心思路是构建一个更全面、更真实的基准测试，即CodeSpecBench，通过可执行的行为规范（前置条件和后置条件）来评估LLM生成的规范的正确性和完整性。这种方法基于执行结果来判断LLM是否真正理解了程序的行为。

技术框架：CodeSpecBench包含以下主要组成部分：1) 函数级别和仓库级别的任务，覆盖不同粒度的代码；2) 可执行的Python规范，作为前置条件和后置条件；3) 基于执行的评估协议，通过运行测试用例来判断生成的规范是否正确和完整。整体流程是：给定一段代码和自然语言描述，LLM生成规范，然后通过执行测试用例来验证规范的有效性。

关键创新：CodeSpecBench的关键创新在于其评估方法的真实性和全面性。它使用可执行的规范，并基于执行结果进行评估，避免了主观判断和模糊性。此外，它还包含了仓库级别的任务，更贴近实际应用场景，能够更有效地评估LLM对复杂程序行为的理解。与现有方法相比，CodeSpecBench在任务设置和评估协议上都更加完善。

关键设计：CodeSpecBench的关键设计包括：1) 任务的多样性，涵盖函数级别和仓库级别的代码；2) 规范的表达形式，使用可执行的Python函数，保证了评估的客观性；3) 评估指标，包括正确率（接受有效行为）和完整率（拒绝无效行为），全面衡量了规范的质量。具体的参数设置和损失函数没有在论文中详细描述，可能使用了标准的代码生成和测试框架。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在CodeSpecBench上对15个最先进的LLM进行了评估，结果表明，在仓库级别的任务上，LLM的性能显著下降，最佳模型的通过率仅为20.2%。此外，实验还发现，规范生成任务比代码生成任务更具挑战性，这表明LLM在代码生成方面的优秀表现并不一定意味着其对程序语义有深刻的理解。

🎯 应用场景

CodeSpecBench可用于评估和提升LLM在软件开发中的应用能力，例如代码自动生成、程序理解和缺陷检测。通过更准确地评估LLM对程序行为的理解，可以提高代码生成的质量和可靠性，减少软件开发中的错误和风险。未来，该基准测试可以促进LLM在自动化软件工程领域的更广泛应用。

📄 摘要（原文）

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.