paperbot · PL 论文追踪

全部论文 待读 收藏

P2 From Prompts to Properties: Rethinking LLM Code Generation with Property-Based Testing

从提示到性质：用基于性质的测试重新审视 LLM 代码生成
FSE Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering2025匹配度 4/10 · 论文处于「PL 技术 × LLM」的交叉点，用基于性质的测试（PBT）来暴露 pass@k 掩盖的 LLM 生成代码正确性缺口，与用户对「静态分析/形式化方法用于 AI 生成程序」的兴趣方向相邻；但它关注的是评估 LLM 代码生成本身，而非用 LLM 改进分析工具，也不涉及 Agentic 程序、浮点或贝叶斯程序分析，且实验仅基于 StarCoder/CodeLlama 等偏旧模型，与画像中偏好的方向只在边缘重叠。引用 4 inbox
Dibyendu Brinto Bose
机器学习与程序语言测试、调试与修复
crossref: 2026-09-12

AI 速览

一句话：以基于性质的测试补充单元测试来评估 LLM 生成代码，揭示被 pass@k 掩盖的正确性缺口。

大语言模型在自动代码生成上表现可观，但保证正确性仍是难题。传统单元测试只检验功能正确性，难以捕捉更深层的逻辑约束。本文提出以基于性质的测试（PBT）作为补充评估策略，在 MBPP 与 HumanEval 基准上评估 StarCoder 与 CodeLlama 生成的代码，并从提示中抽取正确性性质。结果显示：pass@k 指标显示中等成功率，但 PBT 暴露出更多正确性缺口——30–32% 的生成解仅部分满足正确性性质，18–23% 完全失败；性质抽取本身也不完善，9–13% 的约束缺失。这表明仅依赖单元测试的评估会因遗漏基本逻辑错误而高估生成代码的正确性；将单元测试与 PBT 结合可给出更全面的代码正确性评估。

问题
传统基于单元测试的评估只能检验功能正确性，可能高估 LLM 生成代码的正确性，无法暴露深层逻辑错误。
方法
将基于性质的测试（PBT）作为补充评估策略，对 StarCoder 与 CodeLlama 在 MBPP 和 HumanEval 上的生成结果抽取并检验正确性性质。
评估
在 MBPP 与 HumanEval 上对比 pass@k 与 PBT 结果，发现 30–32% 的解仅部分满足性质、18–23% 完全失败，且 9–13% 的性质约束抽取缺失。
原文摘要（Abstract）

Large Language Models (LLMs) have shown promise in automated code generation, but ensuring correctness remains a significant challenge. Traditional unit testing evaluates functional correctness but often fails to capture deeper logical constraints. We apply Property-Based Testing (PBT) as an alternative evaluation strategy to StarCoder and CodeLlama on MBPP and HumanEval. Our results reveal that while pass@k evaluation shows moderate success, PBT exposes additional correctness gaps. A significant portion of generated solutions only partially adhere to correctness properties (30–32%), while 18–23% fail outright. Property extraction is also imperfect, with 9–13% of constraints missing. These findings highlight that unit test-based evaluations may overestimate solution correctness by not capturing fundamental logical errors. Our study demonstrates that combining unit testing with PBT can offer a more comprehensive assessment of generated code correctness, revealing limitations that traditional verification approaches miss.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot9179,
  title = {From Prompts to Properties: Rethinking LLM Code Generation with Property-Based Testing},
  author = {Dibyendu Brinto Bose},
  booktitle = {FSE},
  year = {2025},
  doi = {10.1145/3696630.3728702}
}