CLEVER: A Curated Benchmark for Formally Verified Code Generation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915571958808576 |
|---|---|
| author | Thakur, Amitayush Lee, Jasper Tsoukalas, George Sistla, Meghana Zhao, Matthew Zetzsche, Stefan Durrett, Greg Yue, Yisong Chaudhuri, Swarat |
| author_facet | Thakur, Amitayush Lee, Jasper Tsoukalas, George Sistla, Meghana Zhao, Matthew Zetzsche, Stefan Durrett, Greg Yue, Yisong Chaudhuri, Swarat |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_13938 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | CLEVER: A Curated Benchmark for Formally Verified Code Generation Thakur, Amitayush Lee, Jasper Tsoukalas, George Sistla, Meghana Zhao, Matthew Zetzsche, Stefan Durrett, Greg Yue, Yisong Chaudhuri, Swarat Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages Software Engineering 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). |
| title | CLEVER: A Curated Benchmark for Formally Verified Code Generation |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2505.13938 |