POSTCONDBENCH：形式化后置条件推理中的正确性与完备性基准测试
POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference
AI总结：
本文提出POSTCONDBENCH多语言基准，用于评估LLM生成方法级后置条件的能力，发现正确性与完备性差距显著，仓库级依赖及方法复杂性会加剧该差距。
摘要：
形式化后置条件可精准刻画程序行为，为调试、测试及验证提供支撑，但编写这类后置条件需要深厚专业知识与大量精力，这促使近期研究利用大语言模型（LLM）从代码和自然语言制品中自动生成后置条件。不过，评估仍是关键瓶颈：现有基准主要聚焦有限评估设置下的正确性，常依赖表面形式匹配或对小型、合成数据集的人工评估。我们推出POSTCONDBENCH，这是一个用于评估从真实软件生成方法级后置条件的多语言基准，包含来自121个开源项目的420个Python和Java任务，每个任务都配有专家参与构建的高质量真实后置条件集。为实现自动评估，POSTCONDBENCH提供可运行的执行环境，并通过缺陷判别将完备性可操作化：若一个后置条件集被更多有缺陷的实现违反，同时在正确执行时仍能被满足，则该后置条件集更完备。利用POSTCONDBENCH，我们设定了三种生成设置并评估了五个SOTA LLM，结果显示正确性与完备性之间存在显著差距，且仓库级依赖关系和方法复杂性会加剧这一差距。
英文摘要：
Formal postconditions precisely characterize program behavior and support debugging, testing, and verification, but writing them requires substantial expertise and effort. This has motivated recent work on automatically generating postconditions from code and natural-language artifacts using large language models (LLMs). However, evaluation remains a key bottleneck. Existing benchmarks primarily emphasize correctness under limited evaluation settings, often relying on surface-form matching or manual assessment on small or synthetic datasets. We introduce POSTCONDBENCH, a multilingual benchmark for evaluating method-level postcondition generation from real-world software. POSTCONDBENCH comprises 420 Python and Java tasks drawn from 121 open-source projects, each paired with a high-quality ground-truth postcondition set constructed with expert involvement. To enable automatic evaluation, POSTCONDBENCH provides a runnable execution environment and operationalizes completeness via defect discrimination: a postcondition set is more complete if it is violated by more defective implementations while remaining satisfied on correct executions. Using POSTCONDBENCH, we formulate three generation settings and evaluate five SOTA LLMs. Our results reveal a substantial gap between correctness and completeness, and show that repository-level dependencies and method complexity exacerbate this gap.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
