2022-06-28-aygun22a.md

title	booktitle	abstract	layout	series	publisher	issn	id	month	tex_title	firstpage	lastpage	page	order	cycles	bibtex_author	author	date	address	container-title	volume	genre	issued	pdf	extras
Proving Theorems using Incremental Learning and Hindsight Experience Replay	Proceedings of the 39th International Conference on Machine Learning	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 the state of the art heuristic-based theorem prover E in its best configuration, on the popular benchmarks MPTP2078, M2k and Mizar40. The proofs generated by our algorithm are also almost always significantly shorter than E’s proofs.	inproceedings	Proceedings of Machine Learning Research	PMLR	2640-3498	aygun22a	0	Proving Theorems using Incremental Learning and Hindsight Experience Replay	1198	1210	1198-1210	1198	false	Ayg{\"u}n, Eser and Anand, Ankit and Orseau, Laurent and Glorot, Xavier and Mcaleer, Stephen M and Firoiu, Vlad and Zhang, Lei M and Precup, Doina and Mourad, Shibl	given family Eser Aygün given family Ankit Anand given family Laurent Orseau given family Xavier Glorot given family Stephen M Mcaleer given family Vlad Firoiu given family Lei M Zhang given family Doina Precup given family Shibl Mourad	2022-06-28		Proceedings of the 39th International Conference on Machine Learning	162	inproceedings	date-parts 2022 6 28	https://proceedings.mlr.press/v162/aygun22a/aygun22a.pdf