HyperTree Proof Search for Neural Theorem Proving

By Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, X. Martinet, Amaury Hayat, Gabriel Ebner, Aur'elien Rodriguez, Timothée Lacroix. 2022

249 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Prompting & Reasoning

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “A Monte-Carlo tree search approach outperforms GPT-f in Lean [46].”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “In the future, we aim to equip DSP with more powerful mechanisms, such as HyperTree Proof Search (Lample et al., 2022), to broaden the scope of provable theorems.”
Solving olympiad geometry without human demonstrations (2024, methodology): “Innovation in the proof-search algorithm and online training 3 also improves transformer-based methods, solving a total of ten (adapted) IMO problems in algebra and number theory.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, background): “…a model on large corpora of mathematical text, which signiﬁcantly boosts downstream performance [Hendrycks et al., 2021, Polu and Sutskever, 2020, Lample et al., 2022, Lewkowycz et [Biderman et al., 2023] 4 , and then ﬁne-tuned on the proof-pile , a corpus of mathematical text whose composition…”
The alignment problem from a deep learning perspective (2022, background): “7 Many RL agents trained on hard-coded reward functions learn to reward hack, sometimes exploiting subtle misspeciﬁcations such as bugs in their training environments [Krakovna et al., 2020, Lample et al., 2022, Appendix B.5].”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “Provers targeting different proof assistants are generally not comparable, so we focus the discussion on the three existing provers in Lean [16, 17, 19].”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “, 2022b) BART 406M SQL Query result generation HTPS (Lample et al., 2022) Transformer 600M Math Masked Seq2Seq modeling Thor (Jiang et al.”