REVIEW 7 cited by
Formal Mathematics Statement Curriculum Learning
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.
Forward citations
Cited by 7 Pith papers
-
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
Seed-Prover and Seed-Geometry prove 121 of 155 formalized past IMO problems, reach 99.6% on MiniF2F-test, and solve 5 of 6 IMO 2025 problems after the competition deadline.
-
StepFun-Prover Preview: Let's Think and Verify Step by Step
A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine
SDE-GPG samples from a knowledge-point-to-definition mapping table, runs the AlphaGeometry symbolic deduction engine to produce conclusions, filters candidates with a checking function, and translates the formal outpu...
-
Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening
GRPO's rank bias reinforces likely answers and neglects rare correct proofs; an unlikeliness reward that down-weights likely correct samples improves pass@N in formal theorem proving.
-
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
An open-source theorem-proving model reaches state-of-the-art scores on miniF2F (57.6% Pass@32) and PutnamBench by training on 800K formal proofs synthesized through autoformalization and expert iteration.
-
Clarifying Before Reasoning: A Coq Prover with Structural Context
Enriching LLM theorem-proving prompts with Coq's internal type representations and natural-language explanations raises proof success from 21.8% to 45.8%, surpassing Graph2Tac's 33.2%.
Discussion (0). Continue with ORCID to comment.