Clever Eval

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

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

@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