First Neural Conjecturing Datasets and Experiments
Artificial Intelligence
2020-06-01 v1 Machine Learning
Logic in Computer Science
Neural and Evolutionary Computing
Symbolic Computation
Abstract
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.
Cite
@article{arxiv.2005.14664,
title = {First Neural Conjecturing Datasets and Experiments},
author = {Josef Urban and Jan Jakubův},
journal= {arXiv preprint arXiv:2005.14664},
year = {2020}
}
Comments
Accepted to CICM 2020