Reproduce “TheoremBench: Evaluating LLMs on Theorem Proving in Formal 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
QuocViet Pham, Elvir Karimov, Andrey Galichin, Ivan Oseledets
TheoremBench provides a new Lean4 benchmark for evaluating large language models on structured formal mathematics, demonstrating that stronger models like DeepSeek-Prover-V2-7B significantly benefit from explicit contextual premises while generally producing verbose proofs.
Key insights
- Explicitly providing structural premises significantly reduces the difficulty of formal theorem proving for stronger LLMs, indicating the importance of context-aware reasoning in formal mathematics.
- Current LLM provers exhibit qualitative differences in navigating structured proofs and completing entire theorem groups, suggesting varied abilities in handling hierarchical mathematical knowledge.
- Models frequently generate verbose proofs that are substantially longer than human-written references, pointing to a reliance on extensive tactic exploration over concise proof planning and a bias towards easier subtheorems.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.