Reproduce “MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Kunhao Zheng, Jesse Michael Han, Stanislas Polu
This paper presents miniF2F, a cross-system benchmark for formal Olympiad-level mathematics, to enable direct comparison of neural theorem provers across different formal systems. The work demonstrates that neural models achieve substantially higher performance when integrated with formal systems offering high-level tactics, with a GPT-f/PACT model reaching a 29.2% Pass@8 rate on Lean.
Key insights
- Neural theorem provers achieve substantially higher performance when integrated with formal systems that provide powerful high-level tactics, as evidenced by the Lean baseline's 29.2% Pass@8 rate compared to Metamath's 1.6%.
- Formal systems act as robust verifiers and provide access to automated tactics, allowing neural models to focus on guidance rather than generating every low-level proof step, which significantly improves formal reasoning performance over informal methods.
- Olympiad-level mathematics problems offer a suitable testbed for advanced mathematical reasoning in formal systems due to their non-trivial nature and requirement for creative problem-solving.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.