REVIEW 16 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
Signed reviews
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 16 Pith papers
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
-
The Karp Dataset
A new dataset of 90 natural-language NP-completeness reduction proofs is introduced and used to benchmark reasoning in LLMs.
-
Proposing and solving olympiad geometry with guided tree search
TongGeometry solves every problem in the IMO-AG-30 geometry benchmark and uses its search engine to propose olympiad problems, several accepted by real competitions.
-
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.
-
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
A tree-search theorem prover trained on synthetic proof-state exploration data reaches 60.74% Pass@1 on MiniF2F and 21.18% on ProofNet using an adaptive beam size.
-
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.
-
AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
AlphaVerus bootstraps a Llama-70B model to generate Rust code that passes the Verus verifier by iteratively translating Dafny programs and refining candidates with tree search.
-
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%.
-
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
MPS-Prover, a stepwise Lean prover with curated training data and multi-perspective tree search, reports 75.82% on miniF2F and 32.97% on ProofNet, a new 7B-class step-level state of the art.
-
Hierarchical Attention Generates Better Proofs
A hierarchical attention regularizer improves pass@64 on Lean theorem proving benchmarks by about two percentage points, while its proof-complexity reduction is computed on a small subset and is less robust.
-
Probing Large Language Models in Reasoning and Translating Complex Linguistic Puzzles
On Rosetta Stone linguistic puzzles, GPT-4 performs best with plain input-output prompting, outperforming chain-of-thought and multi-persona prompting on all tested metrics.
-
Enhancing IoT Network Security through Adaptive Curriculum Learning and XAI
A curriculum-learning neural network with LIME feature un-learning and ensemble stacking reports 97 to 98 percent accuracy on Edge-IIoT, CIC-APT-IIoT-2024, and CIC-IoV-2024 intrusion detection benchmarks.
Discussion (0). Continue with ORCID to comment.