Online Training of a Transformer-Based Automated Theorem Prover

Home

Discover

Bookmarks

Keep Up With Latest Trending Papers. Computer Science, AI and Machine Learning and more.Subscribe

CC BY

Source arXiv

Artificial Intelligence

Computation and Language

Online Training of a Transformer-Based Automated Theorem Prover

HyperTree Proof Search for Neural Theorem Proving

We propose an online training procedure for a transformer-based automated theorem prover.

Our approach leverages a new search algorithm, hypertree proofsearch (htps), inspired by the recent success of alphazero.

Our model learnsfrom previous proof searches through online training, allowing it to generalizeto domains far from the training distribution.

We report detailed ablations of our pipeline 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. 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.

Authors

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, Timothée Lacroix

◐ Latest Activity

◐ Recommended Follows