Lean Theorem Proving Eval

lean-theorem-proving-eval

Llemma: An Open Language Model For Mathematics — Azerbayev et al. (2023) (arXiv:2310.10631, 2023)

What this evaluates

Evaluates a language model's ability to generate correct, step-by-step formal proof tactics for mathematical statements within the Lean 4 proof assistant.

Datasets

• miniF2F — total 488; splits: test (488)

Metrics

• solve_rate (primary) — range: [0, 1]
  • Fraction of formalized statements for which the model successfully generates a complete, verified proof within the specified search budget (N=1, S=32, T=100) and 10-minute timeout.

Input / output format

Input: A formalized Lean 4 mathematical statement, provided alongside a 3-shot prompt containing example (tactic state, next tactic) pairs.

Output: A sequence of Lean 4 tactics generated iteratively via beam search, applied to the current proof state until the proof is complete or the budget/timeout is exhausted.

Scoring recipe

def compute_solve_rate(predictions, gold):
    solved = 0
    for stmt, state in zip(predictions, gold):
        tactics = beam_search_generate(stmt, N=1, S=32, T=100)
        if lean_check_proof(tactics, state, timeout=600):
            solved += 1
    return solved / len(gold)

Common pitfalls

• Search budget is defined as NST (3200 tactics), not just the number of attempts or iterations.
• Evaluation uses Lean 4, while some baselines (e.g., ReProver) report results on Lean 3, making direct comparison difficult.
• 10-minute timeout per statement can cause significant variance in wall-clock time across different hardware setups.

Evidence (verbatim from paper)

We evaluate on miniF2F (Zheng et al., 2021), which consists of 488 formalized statements from math competitions and undergraduate coursework. Given a formalized statement, the task is to generate a formal proof that is checked by Lean. We set our search budget to N = 1, S = 32, and T = 100... We generate tactics with beam search and use a 10 minute timeout.

Citation

@misc{azerbayev2023llemma,
  title={Llemma: An Open Language Model For Mathematics},
  author={Azerbayev et al. (2023)},
  year={2023},
  note={arXiv:2310.10631}
}

• arXiv: 2310.10631