构建首个端到端可验证代码生成基准，推动形式化推理研究
CLEVER: A Curated Benchmark for Formally Verified Code Generation
- 设计161个需生成可验证规范与实现的数学问题
- 所有输出经Lean类型检查器后验验证，确保机器可读正确性
- 专为评估大模型在形式化证明中的能力而设，适合程序合成研究者
我们提出CLEVER，一个高质量、精心筛选的161个问题的基准，用于在Lean中进行端到端可验证的代码生成。每个问题包含两个任务：一是生成与预留真值规范匹配的规范；二是生成可证明满足该规范的Lean实现。与以往基准不同，CLEVER避免了测试用例监督、大模型生成的注释，以及泄露实现逻辑或允许空洞解的规范。所有输出均通过Lean的类型检查器进行后验验证，确保机器可检查的正确性。我们使用CLEVER评估多个基于前沿语言模型的少样本和代理式方法，这些方法均未能实现完全验证，确立其作为程序合成与形式推理挑战性基准的地位。该基准可在GitHub（https://github.com/trishullab/clever）及HuggingFace（https://huggingface.co/datasets/amitayusht/clever）获取，所有评估代码亦公开于https://github.com/trishullab/clever-prover。
原文摘要 · Abstract (English)
We introduce ${\rm C{\small LEVER}}$, a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification. Unlike prior benchmarks, ${\rm C{\small LEVER}}$ avoids test-case supervision, LLM-generated annotations, and specifications that leak implementation logic or allow vacuous solutions. All outputs are verified post-hoc using Lean's type checker to ensure machine-checkable correctness. We use ${\rm C{\small LEVER}}$ to evaluate several few-shot and agentic approaches based on state-of-the-art language models. These methods all struggle to achieve full verification, establishing it as a challenging frontier benchmark for program synthesis and formal reasoning. Our benchmark can be found on GitHub(https://github.com/trishullab/clever) as well as HuggingFace(https://huggingface.co/datasets/amitayusht/clever). All our evaluation code is also available online(https://github.com/trishullab/clever-prover).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。