Poster
in
Workshop: MATH-AI: The 4th Workshop on Mathematical Reasoning and AI
ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving
Fabian Gloeckle · Jannis Limperg · Gabriel Synnaeve · Amaury Hayat
Keywords: [ automated theorem proving ] [ Reasoning ] [ theorem proving ] [ Lean ] [ Reinforcement Learning ] [ MCTS ]
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.