REVIEW 7 cited by
HyperTree Proof Search for Neural 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
Signed reviews
read the original abstract
We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.
Forward citations
Cited by 7 Pith papers
-
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalForge is a Lean-grounded, self-improving agentic framework that proposes, proves, and statement-audits causal inference theorems; its runs produced nine accepted results including a new ATE minimax upper bound.
-
The Karp Dataset
A new dataset of 90 natural-language NP-completeness reduction proofs is introduced and used to benchmark reasoning in LLMs.
-
AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
A 245-problem advanced proof benchmark plus 888 expert-labeled trajectories shows frontier LLMs remain far from reliable advanced proof generation and verification.
-
VALG: An Agentic System for ML Theory Research
An agentic system called VALG produced internally finalized theorem candidates for two of nine COLT 2026 open-problem subproblems and weaker partial results for the remaining seven.
-
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.
-
CGES: Confidence-Guided Early Stopping for Efficient and Accurate Self-Consistency
Confidence-Guided Early Stopping stops querying an LLM once one candidate answer accumulates enough Bayesian posterior mass, cutting average calls from 16 to 4.9 on five reasoning benchmarks with negligible average ac...
-
Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
Bourbaki (7B), an MCTS-based system with self-generated subgoal rewards, solves 26/658 PutnamBench problems, beating the prior 7B best of 23 at a larger sample budget.
Discussion (0). Continue with ORCID to comment.