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.
%0 Generic
%1 lample2022hypertree
%A Lample, Guillaume
%A Lachaux, Marie-Anne
%A Lavril, Thibaut
%A Martinet, Xavier
%A Hayat, Amaury
%A Ebner, Gabriel
%A Rodriguez, Aurélien
%A Lacroix, Timothée
%D 2022
%K machine_learning theorem_proving
%T HyperTree Proof Search for Neural Theorem Proving
%U http://arxiv.org/abs/2205.11491
%X 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.
@misc{lample2022hypertree,
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.},
added-at = {2022-12-30T15:59:33.000+0100},
author = {Lample, Guillaume and Lachaux, Marie-Anne and Lavril, Thibaut and Martinet, Xavier and Hayat, Amaury and Ebner, Gabriel and Rodriguez, Aurélien and Lacroix, Timothée},
biburl = {https://www.bibsonomy.org/bibtex/25fd1ca1dce93101a929ad2ecdd612b9f/intfxdx},
description = {HyperTree Proof Search for Neural Theorem Proving},
interhash = {74885b4a14d24cd5a9befde653e27e7b},
intrahash = {5fd1ca1dce93101a929ad2ecdd612b9f},
keywords = {machine_learning theorem_proving},
note = {cite arxiv:2205.11491},
timestamp = {2022-12-30T15:59:33.000+0100},
title = {HyperTree Proof Search for Neural Theorem Proving},
url = {http://arxiv.org/abs/2205.11491},
year = 2022
}