聪明：一个用于形式验证代码生成的精心策划基准

于红博

摘要: 我们介绍了${\rm C{\small LEVER}}$，这是一个高质量、经过精心筛选的基准，用于Lean中端到端验证代码生成的161个问题。每个问题包括(1)生成与预留的真实规范相匹配的规范的任务，以及(2)生成一个可证明满足这一规范的Lean实现的任务。与先前的基准不同，${\rm C{\small LEVER}}$避免了测试案例监督、LLM生成的注释以及泄漏实现逻辑或允许空洞解决方案的规范。所有输出都经过后期验证，使用Lean的类型检查器确保可机器检查的正确性。我们使用${\rm C{\small LEVER}}$评估了基于最先进的语言模型的几种少样本和主体方法。这些方法都难以实现完全验证，将其确立为程序合成和形式推理的具有挑战性的前沿基准。我们的基准可在GitHub(https://github.com/trishullab/clever)和HuggingFace(https://huggingface.co/datasets/amitayusht/clever)上找到。我们所有的评估代码也可在线获取(https://github.com/trishullab/clever-prover)。

更新时间: 2025-10-23 16:29:07

领域: cs.LG,cs.AI,cs.LO,cs.PL,cs.SE

下载: http://arxiv.org/abs/2505.13938v4