Clever Eval

---
name: clever-eval
description: Evaluates end-to-end formally verified code generation by requiring models to produce both a logically equivalent formal specification and a provably correct implementation in Lean 4. It probes the model's ability to reason about non-computable specifications, synthesize machine-checkable proofs, and ensure semantic correctness beyond syntactic compilation. Use when the user wants to benchmark on CLEVER, or asks about evaluating this task. Reports pass@600-seconds.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2505.13938
  bibtex_key: [REDACTED]
  confidence: high
---

# clever-eval

> CLEVER: A Curated Benchmark for Formally Verified Code Generation — Thakur et al. (2025) (arXiv:2505.13938, 2025)

## What this evaluates

Evaluates end-to-end formally verified code generation by requiring models to produce both a logically equivalent formal specification and a provably correct implementation in Lean 4. It probes the model's ability to reason about non-computable specifications, synthesize machine-checkable proofs, and ensure semantic correctness beyond syntactic compilation.

## Datasets

- **CLEVER** — total 161; splits: test (161)

## Metrics

- `pass@600-seconds` **(primary)** — range: percent
  - Fraction of benchmark problems solved within a fixed time budget k (k=600 seconds). A task is solved only if both the formal specification and implementation are generated, compile in Lean 4, and have their equivalence and correctness proofs accepted by Lean's type checker.

## Input / output format

**Input**: Natural language problem description and a non-computable reference specification.

**Output**: Lean 4 code for a formal specification and an implementation, along with proofs of equivalence to the reference specification and correctness of the implementation.

## Scoring recipe

```python
def score(predictions, gold, timeout=600):
    solved = 0
    for pred in predictions:
        t_rem = timeout
        spec, t_rem = retry_generate_spec(pred, t_rem)
        if t_rem < 0: continue
        eq_proof, t_rem = retry_prove_equivalence(spec, gold, t_rem)
        if t_rem < 0: continue
        impl, t_rem = retry_generate_impl(pred, spec, t_rem)
        if t_rem < 0: continue
        corr_proof, t_rem = retry_prove_correctness(impl, gold, t_rem)
        if t_rem < 0: continue
        if lean_compile(spec) and lean_accept(eq_proof) and \
           lean_compile(impl) and lean_accept(corr_proof):
            solved += 1
    return solved / len(predictions)
```

## Common pitfalls

- Assuming syntactic compilation or passing example-based test cases guarantees semantic correctness; the benchmark explicitly excludes test cases from the core success metric.
- Expecting uniform difficulty across stages; specification certification and implementation correctness proofs often have inverse difficulty profiles, making joint success rare.
- Overlooking the retry mechanism; the evaluation allows infinite retries per step until timeout, so raw generation accuracy is not the bottleneck.

## Evidence (verbatim from paper)

> To fairly compare approaches that differ in model size, latency, and API usage, we adopt the metric pass@k-seconds—the fraction of benchmark problems solved within a fixed time budget k. A task is marked as solved only if both the formal specification and the implementation are generated and verified via Lean's type checker.

## Citation

```bibtex
@misc{thakur2025clever,
  title={CLEVER: A Curated Benchmark for Formally Verified Code Generation},
  author={Thakur et al. (2025)},
  year={2025},
  note={arXiv:2505.13938}
}
```

- arXiv: 2505.13938