Elamur Research⌕
☰
home / papers / 2020 / First Neural Conjecturing Datasets and Experiments

First Neural Conjecturing Datasets and Experiments

Paper · 2020 · Josef Urban and Jan Jakubův

Summary

The paper addresses automated conjecture generation in large formal mathematics corpora. This covers proposing helpful intermediate lemmas and exploring a theory freely. Urban and Jakubův build four datasets from the Mizar Mathematical Library (MML). Two are textual: raw Mizar articles and an HTML-derived export enriched with types and theses. The other two come from MPTP-translated problems proved by the E prover with ENIGMA guidance: full tokenized TPTP proofs and compact prefix-notation lists of the premises each proof used. They train the smallest GPT-2 model on each dataset and test it in three ways: unconditioned sampling, conditioned completion of formulas and premise lists, and an ATP-based semantic evaluation. GPT-2 produces plausible Mizar-style theorems and proofs, and some of its suggested premise sets yield new E proofs. However, many outputs are unprovable or countersatisfiable, which exposes a gap between syntactic training loss and logical usefulness. The released datasets, models, samples and web autocompletion server give a first public basis for neural conjecturing and for future learning–reasoning feedback loops.

Key points

  • Four datasets:
    • MML version 1147 concatenated (78MB).
    • HTML-export text (156MB).
    • ENIGMA/E TPTP proofs for 28,271 theorems (658MB).
    • Prefix-notation premise selections (53MB).
  • Training setup: GPT-2 with 117M parameters, trained on one GTX 1080 GPU. Training ran for weeks on datasets 1, 2 and 4. Training on dataset 3 was stopped early because of redundant punctuation tokens.
  • Conditioned completion: The tests used 369 CARD theorems for premise completion and 462 partial CARD formulas for formula completion. Low sampling temperatures mostly reproduce existing Mizar theorems. Higher temperatures produce new well-typed lemmas, and still higher ones produce ill-typed or unparsable output.
  • ATP evaluation on 31,792 theorems (6639 unseen):
    • 12 predictions per theorem gave 381,432 predictions, or 193,320 unique ones.
    • Of the problems without new conjectures, 86,899 of 108,564 were countersatisfiable.
    • 11,866 problems were proved within 6 s, covering 8105 theorems. Many of these proofs were trivial self-premise cases.
  • New formulas: GPT-2 proposed 52,515 new syntactically correct formulas, 33,100 after deduplication. E with ENIGMA and standard premise selection proved about 9000–10000 of them. Some interesting conjectures were generalizations, for example from finite to arbitrary groups.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Josef Urban and Jan Jakubův. 2020. First Neural Conjecturing Datasets and Experiments. arXiv:2005.14664.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2005.14664 · arXiv 2005.14664

@misc{urban2020first,
  title = {{First Neural Conjecturing Datasets and Experiments}},
  author = {Josef Urban and Jan Jakubův},
  year = {2020},
  doi = {10.48550/arxiv.2005.14664},
  eprint = {2005.14664},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2005.14664}
}

References

17 references, 5 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Chad E. Brown and Thibault Gauthier. Self-learned formula synthesis in set theory. CoRR, abs/1912.01525, 2019. — [arXiv:1912.01525](https://arxiv.org/abs/1912.01525) find
  2. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In CADE 27, pages 197–215, 2019.
  3. Simon Colton. Automated Theory Formation in Pure Mathematics. Distinguished Dissertations. Springer London, 2012. http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.out.tar.gz http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.tar.gz http://grid01.ciirc.cvut.cz/~mptp/7.13… ↗
  4. Siemion Fajtlowicz. On conjectures of Graffiti. Annals of Discrete Mathematics, 72(1–3):113–118, 1988. find
  5. Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797, 2019.
  6. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In CICM’16 WiP Proceedings, pages 219–228, 2016. find
  7. Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen. Hipster: Integrating theory exploration in a proof assistant. In CICM 2014, pages 108–122, 2014. find
  8. Cezary Kaliszyk, Josef Urban, and Jirı́ Vyskocil. Automating formalization by statistical and semantic parsing of mathematics. In ITP, pages 12–27, 2017. find
  9. Cezary Kaliszyk, Josef Urban, and Jiřı́ Vyskočil. Learning to parse on aligned corpora (rough diamond). In ITP 2015, pages 227–233, 2015. find
  10. Douglas Bruce Lenat. AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search. PhD thesis, Stanford, 1976. find
  11. Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks, 2020.
  12. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAI Blog, 1(8):9, 2019. find
  13. Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735–743. Springer, 2013. find
  14. Josef Urban. XML-izing Mizar: Making semantic processing and presentation of MML easy. In Michael Kohlhase, editor, MKM, volume 3863 of LNCS, pages 346–360. Springer, 2005. find
  15. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  16. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In CPP, pages 85–98, 2020.
  17. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In CICM, pages 255–270, 2018.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/