Learning to Prove Theorems by Learning to Generate Theorems

Learning to reason in large theories without imitation

Original

Bansal, K., Loos, S. M., Rabe, M. N., and Szegedy, C · 1905

Earlier work this paper cites.

Simple statistical gradient-following algorithms for connectionist reinforcement learning

Williams, R. J · 1992

Earlier work this paper cites.

Formal verification in hardware design: a survey

Kern, C. and Greenstreet, M. R · 1999

Earlier work this paper cites.

E–a brainiac theorem prover

Schulz, S · 2002

Earlier work this paper cites.

Formal proof sketches

Wiedijk, F · 2003

Earlier work this paper cites.

Coq’art: the calculus of inductive constructions, 2004

Bertot, Y. and Castéran, P · 2004

Earlier work this paper cites.

Mptp–motivation, implementation, first experiments

Urban, J · 2004

Earlier work this paper cites.

A theorem proving approach to analysis of secure information flow

Darvas, Á., Hähnle, R., and Sands, D · 2005

Earlier work this paper cites.

Bandit based monte-carlo planning

Kocsis, L. and Szepesvári, C · 2006

Earlier work this paper cites.

A brief overview of hol4

Slind, K. and Norrish, M · 2008

Earlier work this paper cites.

Malarea sg1-machine learner for automated reasoning with semantic guidance

Urban, J., Sutcliffe, G., Pudlák, P., and Vyskočil, J · 2008

Earlier work this paper cites.

HOL Light: An overview

Harrison, J · 2009

Earlier work this paper cites.

Automated theory formation in pure mathematics

Colton, S · 2012

Earlier work this paper cites.

Generative adversarial nets

Goodfellow, I., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A., and Bengio, Y · 2014

Earlier work this paper cites.

Machine learner for automated reasoning 0.4 and 0.5

Original

Kaliszyk, C., Urban, J., and Vyskočil, J · 2014

Earlier work this paper cites.

Adam: A method for stochastic optimization

Original

Kingma, D. P. and Ba, J · 2014

Cited alongside, same era.

Learning-assisted theorem proving with millions of lemmas

Kaliszyk, C. and Urban, J · 2015

Cited alongside, same era.

Lemmatization for stronger reasoning in large theories

Kaliszyk, C., Urban, J., and Vyskočil, J · 2015

Cited alongside, same era.

Certikos: An extensible architecture for building certified concurrent { \{ OS } \} kernels

Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sjöberg, V., and Costanzo, D · 2016

Cited alongside, same era.

Deepmath-deep sequence models for premise selection

Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F., and Urban, J · 2016

Cited alongside, same era.

Holophrasm: a neural automated theorem prover for higher-order logic

Reinforcement learning of theorem proving

Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M · 2018

Later among the works it cites.

Atpboost: Learning premise selection in binary setting with atp feedback

Piotrowski, B. and Urban, J · 2018

Later among the works it cites.

Learning goal embeddings via self-play for hierarchical reinforcement learning

Original

Sukhbaatar, S., Denton, E., Szlam, A., and Fergus, R · 2018

Later among the works it cites.

First experiments with data driven conjecturing

Chvalovskỳ, K., Gauthier, T., and Urban, J · 2019

Later among the works it cites.

Learning dynamic polynomial proofs

Fawzi, A., Malinowski, M., Fawzi, H., and Fawzi, O · 2019

Later among the works it cites.

On learning to prove

Original