Timezone: »

 
Poster
Proving Theorems using Incremental Learning and Hindsight Experience Replay
Eser Aygün · Laurent Orseau · Ankit Anand · Xavier Glorot · Stephen McAleer · Vlad Firoiu · Lei Zhang · Doina Precup · Shibl Mourad

@ None #None

Traditional automated theorem proving systems for first-order logic depend on speed-optimized search and many handcrafted heuristics designed to work over a wide range of domains. Machine learning approaches in the literature either depend on these traditional provers to bootstrap themselves, by leveraging these heuristics, or can struggle due to limited existing proof data. The latter issue can be explained by the lack of a smooth difficulty gradient in theorem proving datasets; large gaps in difficulty between different theorems can make training harder or even impossible. In this paper, we adapt the idea of hindsight experience replay from reinforcement learning to the automated theorem proving domain, so as to use the intermediate data generated during unsuccessful proof attempts. We build a first-order logic prover by disabling all the smart clause-scoring heuristics of the state-of-the-art E prover and replacing them with a clause-scoring neural network learned by using hindsight experience replay in an incremental learning setting. Clauses are represented as graphs and presented to transformer networks with spectral features.We show that provers trained in this way can outperform previous machine learning approaches and compete with state of the art heuristic-based theorem provers such as E in its best configuration, on the popular benchmarks MPTP2078 and M2k.The proofs generated by our algorithm are also almost always significantly shorter than E's proofs.

Author Information

Eser Aygün (DeepMind)
Laurent Orseau (DeepMind)
Ankit Anand (DeepMind)
Xavier Glorot (DeepMind)
Stephen McAleer (UCI)
Vlad Firoiu (DeepMind)
Lei Zhang (DeepMind)
Doina Precup (DeepMind)
Shibl Mourad (DeepMind)

Related Events (a corresponding poster, oral, or spotlight)

More from the Same Authors