REVIEW 6 cited by
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
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
Formal theorem proving, a field at the intersection of mathematics and computer science, has seen renewed interest with advancements in large language models (LLMs). This paper introduces SubgoalXL, a novel approach that synergizes subgoal-based proofs with expert learning to enhance LLMs' capabilities in formal theorem proving within the Isabelle environment. SubgoalXL addresses two critical challenges: the scarcity of specialized mathematics and theorem-proving data, and the need for improved multi-step reasoning abilities in LLMs. By optimizing data efficiency and employing subgoal-level supervision, SubgoalXL extracts richer information from limited human-generated proofs. The framework integrates subgoal-oriented proof strategies with an expert learning system, iteratively refining formal statement, proof, and subgoal generators. Leveraging the Isabelle environment's advantages in subgoal-based proofs, SubgoalXL achieves a new state-of-the-art performance of 56.1\% in Isabelle on the standard miniF2F dataset, marking an absolute improvement of 4.9\%. Notably, SubgoalXL successfully solves 41 AMC12, 9 AIME, and 3 IMO problems from miniF2F. These results underscore the effectiveness of maximizing limited data utility and employing targeted guidance for complex reasoning in formal theorem proving, contributing to the ongoing advancement of AI reasoning capabilities. The implementation is available at \url{https://github.com/zhaoxlpku/SubgoalXL}.
Forward citations
Cited by 6 Pith papers
-
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
A dual-model framework that extracts proof sketches from whole-proof candidates and refines them with a tactic model and Sledgehammer, reaching 59.4 percent on miniF2F in Isabelle.
-
Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
A decoupled reasoning-and-proving framework generated machine-verified Lean proofs for five post-2000 IMO problems.
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
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...
-
Solving Formal Math Problems by Decomposition and Iterative Reflection
An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.
-
Scaling Reasoning without Attention
A purely attention-free Mamba-2 model, fine-tuned with PromptCoT-style synthetic data, reaches state-of-the-art scores on AIME and LiveCodeBench among open models of its size and surpasses Gemma3-27B on three benchmarks.
Discussion (0). Continue with ORCID to comment.