title: Towards Finding Longer Proofs
abstract: We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving.  In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.
authors: Zsolt Zombori Adrián Csiszárik Henryk Michalewski Cezary Kaliszyk Josef Urban
hIndex: Josef Urban 35