2020/05/29 by Josef Urban, Urban, Josef, Jan Jakubův +1 · 1 citation
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Neural and Evolutionary Computing (cs.NE) #Symbolic Computation (cs.SC) #cs.AI #cs.LG #cs.LO #cs.NE #cs.SC
paper · pdf · doi:10.48550/arxiv.2005.14664
Accepted to CICM 2020
arxiv created 2020/05/29 · arxiv updated 2020/06/01
We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms and the problems extracted from it by the MPTP system and proved by the E prover using the ENIGMA guidance. The conjecturing experiments use the Transformer architecture and in particular its GPT-2 implementation.