ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving

Abstract

We propose a scalable and efficient reinforcement learning framework as a strong baseline for theorem proving with limited data. This baseline reaches performances comparable to the current state-of-the-art in theorem proving, while only training on a few hundred examples. This a first step toward an efficient and easily reproducible combination of autoformalization, synthetic data generation and reinforcement learning, which could unlock significant advancements in neural theorem proving.

PDF NeurIPSW OpenReview Semantic Scholar

Cite

Text

Gloeckle et al. "ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving." NeurIPS 2024 Workshops: MATH-AI, 2024.

Markdown

[Gloeckle et al. "ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving." NeurIPS 2024 Workshops: MATH-AI, 2024.](https://mlanthology.org/neuripsw/2024/gloeckle2024neuripsw-abel/)

BibTeX

@inproceedings{gloeckle2024neuripsw-abel,
  title     = {{ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving}},
  author    = {Gloeckle, Fabian and Limperg, Jannis and Synnaeve, Gabriel and Hayat, Amaury},
  booktitle = {NeurIPS 2024 Workshops: MATH-AI},
  year      = {2024},
  url       = {https://mlanthology.org/neuripsw/2024/gloeckle2024neuripsw-abel/}
}