Minif2f Pipeline Eval

---
name: minif2f-pipeline-eval
description: 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. Use when the user wants to benchmark on miniF2F, or asks about evaluating this task. Reports effective_accuracy.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2511.03108
  bibtex_key: ospanov2025minif2f
  confidence: high
---

# 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

```python
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

```bibtex
@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