Elamur Research⌕
☰
home / papers / 2016 / DeepMath - Deep Sequence Models for Premise Selection

DeepMath - Deep Sequence Models for Premise Selection

Paper · 2016 · Alex A. Alemi, Francois Chollet, Niklas Een et al.

Summary

Automated theorem provers (ATPs) slow down badly when given a very large library of facts. Choosing a small set of useful premises for a new conjecture is therefore a major bottleneck in formalizing mathematics. The authors treat premise selection as a pairwise scoring task. Two separate neural encoders turn a conjecture and a candidate axiom into fixed-length vectors. Both are first-order logic strings from the Mizar Mathematical Library, translated by MPTP. A small fully connected network with logistic loss then estimates whether the axiom helps prove the conjecture. Training uses only proofs that ATPs found earlier. Stage 1 compares character-level encoders: CNN, LSTM/GRU and a convolutional-recurrent hybrid. Stage 2 adds a word-level CNN whose symbol embeddings are built from definitions by the stage-1 model, which helps with rare tokens. E prover then attempts proofs over growing top-k premise cutoffs. Plain convolutional encoders with max pooling beat recurrent ones. The best combination slightly outperformed a strong k-NN baseline built on hand-crafted features, and the two kinds of method proved largely complementary. The authors present this as the first large-scale use of deep learning for theorem proving.

Key points

  • Data: Mizar Mathematical Library version 4.181.1147, with 57,917 theorems in 1,147 articles. Training used ATP proofs for 32,524 of them (56.2%). The prover was E prover 1.9, and the test set had 2,742 theorems.
  • Best single neural model: def-CNN, which uses definition-based embeddings, proved 66.4% of the test set. Averaging its scores with char-CNN raised this to 67.9%, against 65.1% for the k-NN baseline.
  • Two convolutional layers worked best. Recurrent models (LSTM, GRU, def-CNN-LSTM) lagged behind, partly because statements range from 5 to 84,299 characters.
  • The union of def-CNN and k-NN proved 74.25% of the test set, and the union of all methods proved 80.9%. This shows that neural and hand-engineered rankings complement each other.
  • Applying the models to Mizar statements that had never been proved automatically produced 823 new proofs.

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 5The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksArts and Humanities · 17,450 worksLanguage and Linguistics · 17,296 worksComputational Theory and Mathematics · 321 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. arXiv:1606.04442.

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

@misc{alemi2016deepmath,
  title = {{DeepMath - Deep Sequence Models for Premise Selection}},
  author = {Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy and Josef Urban},
  year = {2016},
  doi = {10.48550/arxiv.1606.04442},
  eprint = {1606.04442},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1606.04442}
}

References

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

  1. M. Abadi, A. Agarwal, P. Barham, E. Brevdo, Z. Chen, C. Citro, G. S. Corrado, A. Davis, J. Dean, M. Devin, S. Ghemawat, I. Goodfellow, A. Harp, G. Irving, M. Isard, Y. Jia, R. Jozefowicz, L. Kaiser, M. Kudlur, J. Levenberg, D. Mané, R. Monga, S. Moore, D. Murray, C. Olah, M. Schuster, J. Shlens, B.… find
  2. G. Bancerek and P. Rudnicki. A Compendium of Continuous Lattices in MIZAR. J. Autom. Reasoning, 29(3-4):189–224, 2002. find
  3. P. Baudiš, J. Pichl, T. Vyskočil, and J. Šedivý. Sentence pair scoring: Towards unified framework for text comprehension. arXiv preprint arXiv:1603.06127, 2016. — [arXiv:1603.06127](https://arxiv.org/abs/1603.06127) find
  4. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  5. F. Chollet. Keras. https://github.com/fchollet/keras, 2015. ↗
  6. J. Chung, C. Gulcehre, K. Cho, and Y. Bengio. Gated feedback recurrent neural networks. arXiv preprint arXiv:1502.02367, 2015. find
  7. The Coq Proof Assistant. http://coq.inria.fr. ↗
  8. A. M. Dai and Q. V. Le. Semi-supervised sequence learning. In Advances in Neural Information Processing Systems, pages 3061–3069, 2015. find
  9. N. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In M. Laudet, editor, Proceedings of the Symposium on Automatic Demonstration, pages 29–61, Versailles, France, Dec. 1968. Springer-Verlag LNM 125. find
  10. X. Glorot and Y. Bengio. Understanding the difficulty of training deep feedforward neural networks. In International conference on artificial intelligence and statistics, pages 249–256, 2010. Model char-CNN word-CNN def-CNN-LSTM def-CNN Test min average relative rank 0.0585 0.06 0.0605 0.0575 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/