Minif2f Pipeline Eval

minif2f-pipeline-eval

miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward — Ospanov et al. (2025) (arXiv:2511.03108, 2025)

What this evaluates

Evaluates the end-to-end capability of autoformalizers and theorem provers to translate informal mathematical statements into verified Lean 4 proofs. It probes semantic fidelity during translation and the ability of provers to generate correct, aligned proofs for Olympiad-style problems.

Datasets

• miniF2F — total ?; splits: test (-1), valid (-1); repo https://github.com/roozbeh-yz/miniF2F_v2

Metrics

• effective_accuracy (primary) — range: percent
  • Percentage of problems where the generated proof passes REPL verification. Reported in two settings: (1) 'full score': credit given for any verified proof, even if excessively simplified; (2) 'Olympiad setting': credit only if the proof both passes verification and semantically aligns with the original informal statement.

Input / output format

Input: Informal mathematical statement (Math Olympiad-style problem text)

Output: Lean 4 formal statement and proof script generated by an autoformalizer followed by a theorem prover

Scoring recipe

def score_pipeline(predictions, gold):
    verified_count = 0
    aligned_count = 0
    for pred, gold_stmt in zip(predictions, gold):
        passes_repl = check_repl_verification(pred.formal_stmt, pred.proof)
        if passes_repl:
            verified_count += 1
            aligns = check_semantic_alignment(pred.proof, gold_stmt)
            if aligns:
                aligned_count += 1
    return {
        'effective_accuracy_full': verified_count / len(predictions) * 100,
        'effective_accuracy_olympiad': aligned_count / len(predictions) * 100
    }

Common pitfalls

• Overly simplified proofs that type-check but do not actually solve the original problem are counted as correct in the 'full score' setting, inflating pipeline accuracy.
• Semantic alignment requires human or LLM judgment, which can vary significantly between evaluators and affect the 'Olympiad setting' scores.
• The pipeline is sequential; errors in autoformalization compound and prevent theorem proving, making it hard to isolate prover vs. translator failures.

Evidence (verbatim from paper)

For each problem we begin by feeding the informal statement to an autoformalizer; we keep the first formal output that both passes REPL verification and remains semantically faithful to the source, which is judged by human experts. We then attempt to prove the resulting goal with several theorem provers, and finally we compare the derived theorem with the original problem, recording any discrepancies. We refer to final accuracy of autoformalizer and theorem prover collaboration as "effective accuracy". ... we report two effective accuracy metrics: (i) the percentage of proofs that pass REPL verification giving credit to all proofs even for the ones that are excessively simplified compared to the original informal statements, and (ii) the percentage of proofs that both pass verification and align with the original problem statement, i.e., the Olympiad setting.

Citation

@misc{ospanov2025minif2f,
  title={miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward},
  author={Ospanov et al. (2025)},
  year={2025},
  note={arXiv:2511.03108}
}

• arXiv: 2511.03108