Research map / Large language models / Agents, code and math
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces CLEVER, a manually curated 161-problem Lean 4 benchmark (from HumanEval) for end-to-end verified code generation requiring spec equivalence proofs and implementation correctness proofs, and shows few-shot and agentic LLM approaches solve at most one problem end-to-end.
Problem
Existing formally verified code generation benchmarks use specifications that are computable, leak implementation logic, rely on test cases, or are auto-generated, allowing trivial or cheating solutions; no benchmark requires complete, human-quality formal specs with machine-checked correctness.
Approach
Hand-written non-computable Lean specifications (Prop-valued) for 161 HumanEval tasks, with a staged pipeline requiring the model to generate a spec, prove isomorphism to the hidden ground-truth spec, generate an implementation, and prove it satisfies the ground-truth spec, all checked by Lean's kernel.
Key results
- Few-shot and COPRA approaches achieve at most 0.621% end-to-end success (1 of 161 problems, problem 53) across GPT-4o, o4-mini, Claude-3.7, DeepSeek-R1, and GPT-5-mini hybrid.
- Specification certification rates are at most about 1.9% (GPT-4o with COPRA), while compilation rates for specs reach 71-90%.
- Implementation certification peaks at 8.7% for Claude-3.7 with COPRA, followed by 5.6% for DeepSeek-R1 few-shot.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use COPRA instead of few-shot generation for proof steps | GPT-4o · CLEVER | implementation certification pass@600-sec: 1.863% -> 3.727% | Helped |
| Use COPRA instead of few-shot generation for proof steps | Claude-3.7 · CLEVER | implementation certification pass@600-sec: 1.863% -> 8.696% | Helped |
| Use COPRA instead of few-shot generation for proof steps | GPT-4o · CLEVER | end-to-end pass@600-sec: 0% -> 0.621% | No clear effect |
| Use COPRA instead of few-shot generation for proof steps | Claude-3.7 · CLEVER | end-to-end pass@600-sec: 0.621% -> 0.621% | No clear effect |
| Use KiminaProver-7b for proof steps | GPT-5-mini · CLEVER | specification compilation pass@600-sec: 90.062% | Helped |
| Use KiminaProver-7b for proof steps | GPT-5-mini · CLEVER | specification certification pass@600-sec: 0% | Hurt |
Surprising findings
- Specification compilation is high (up to 90%) but certification of the spec against the ground truth is nearly zero, showing the equivalence proof is the main bottleneck.
- The hybrid GPT-5-mini plus KiminaProver pipeline had the highest compilation rates but certified almost nothing due to output parsing issues.
Limitations
- Only 161 problems derived from HumanEval, which are relatively simple programming tasks.
- Some problems could not be formalized due to Lean limitations (e.g., MD5, dynamically typed problems), and specifications are manually written and may still be imperfect.
- Results depend on time budget and on proprietary models that change over time, and no error bars are reported.
Experimental setup
Datasets: HumanEval
Benchmarks: CLEVER
Metrics: pass@k-seconds compile@k prove@k end-to-end success rate
Baselines: GPT-4o few-shot o4-mini few-shot Claude-3.7 few-shot DeepSeek-R1 few-shot COPRA with GPT-4o COPRA with Claude-3.7 GPT-5-mini with Kimina prover FVAPPS
Builds on: COPRA HumanEval Kimina-Prover
Closest papers by meaning
- AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (ICML 2025 · similarity 0.89)
- Verify0: Can AI Agents Build Formally Verified Software Repositories? (NeurIPS 2026 · similarity 0.86)
- Automated Proof Generation for Rust Code via Self-Evolution (ICLR 2025 · similarity 0.86)
- Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages (NeurIPS 2024 · similarity 0.86)
- Divide-and-Conquer Meets Consensus: Unleashing the Power of Functions in Code Generation (NeurIPS 2024 · similarity 0.86)
- Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation (NeurIPS 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.