---
title: "Deep Network Guided Proof Search — paper by Loos et al. (2017)"
description: "Saturation-based first-order provers struggle to find proofs in large libraries of formal mathematics. 47 references, cited by 47 papers here."
authors: ["Sarah Loos", "Geoffrey Irving", "Christian Szegedy", "Cezary Kaliszyk"]
year: 2017
venue: "arXiv:1701.06972 (In Thomas Eiter and David Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pages 85-105, EasyChair, 2017. ISSN 2398-7340)"
source: "https://arxiv.org/abs/1701.06972"
doi: "10.48550/arxiv.1701.06972"
arxiv: "1701.06972"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2017](https://md.research.elamur.ai/free/en/papers/2017/page/3/) / Deep Network Guided Proof Search

# Deep Network Guided Proof Search

**Authors:** [Sarah Loos](https://md.research.elamur.ai/free/en/authors/sarah-m-loos/), [Geoffrey Irving](https://md.research.elamur.ai/free/en/authors/geoffrey-irving/), [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/) and [Cezary Kaliszyk](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) · **Year:** 2017 · **Venue:** arXiv:1701.06972 (In Thomas Eiter and David Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pages 85-105, EasyChair, 2017. ISSN 2398-7340) · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1701.06972) · [PDF](https://arxiv.org/pdf/1701.06972v1) · [DOI 10.48550/arxiv.1701.06972](https://doi.org/10.48550/arxiv.1701.06972) · [arXiv 1701.06972](https://arxiv.org/abs/1701.06972) · [OpenAlex](https://openalex.org/W2581336110)

**Citations:** 92 citations (OpenAlex, 2026-10-14) · [47](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Saturation-based first-order provers struggle to find proofs in large libraries of formal mathematics. This paper addresses that by letting deep neural networks choose which clause the prover E should process next. Training data come from 91,877 existing ATP proofs of Mizar Mathematical Library statements translated to first-order logic. These proofs are split by conjecture into training and validation parts. Several networks, including a simple CNN and WaveNet-style models, learn to score unprocessed clauses from their textual or syntax-tree form.

Network inference is much slower than an ordinary prover step, so the authors combine the network's rankings with E's hand-crafted heuristics. They also use a two-phase schedule: a slow, network-guided phase followed by a fast, unguided phase to finish the search.

On 25,361 statements that no ATP had proved before ("hard" statements), the cheap CNN nearly doubles the success rate of unguided search. All methods together prove 7.36% of these statements, raising ATP coverage of the corpus from 56% to 59%. The results show that learned guidance can pay off inside a fast prover despite its computational cost.

## Key points
- **Corpus:** 57,882 MML theorems in FOL, of which 32,521 (about 56%) already had ATP proofs.
- **Data split:** training uses 82,718 proofs of 29,325 conjectures; evaluation uses 9,159 proofs of 3,196 conjectures.
- **Schedule on hard statements:** a 20-minute hybrid network-guided phase is followed by a 10-minute heuristic-only phase. Premises are chosen with the DeepMath 1 and DeepMath 2 character-level models.
- **CNN result:** the "switch" CNN strategy proves 4.34% of hard statements versus 2.33% for unguided Auto, roughly 86% more.
- **Speed vs. accuracy:** WaveNet scores better on holdout metrics but is too slow to evaluate, so it proves fewer theorems than the CNN. In total, 1,866 hard theorems were proved.

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

## Institutions

- [Google](https://md.research.elamur.ai/free/en/companies/google/) — Company, Mountain View, United States · 492 works · 440,462 citations
- [Carnegie Mellon University](https://md.research.elamur.ai/free/en/universities/carnegie-mellon-university/) — University, Pittsburgh, United States · 598 works · 191,225 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 10 works · 876 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk. 2017. Deep Network Guided Proof Search. arXiv:1701.06972 (In Thomas Eiter and David Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pages 85-105, EasyChair, 2017. ISSN 2398-7340).

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{loos2017deep,
  title = {{Deep Network Guided Proof Search}},
  author = {Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk},
  year = {2017},
  doi = {10.48550/arxiv.1701.06972},
  eprint = {1701.06972},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1701.06972}
}
```

- [← previous Learning Cognitive Features from Gaze Data for Sentiment and Sarcasm Classification using Convolutional Neural Network](https://md.research.elamur.ai/free/en/papers/mishra-2017-learning-cognitive-features-gaze-data/)
- [next → Findings of the Second Shared Task on Multimodal Machine Translation and Multilingual Image Description](https://md.research.elamur.ai/free/en/papers/elliott-2017-findings-second-shared-task-multimodal/)
- [↑ back to papers of 2017](https://md.research.elamur.ai/free/en/papers/2017/page/3/)

## References

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

1. Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenber… [find](https://scholar.google.com/scholar?q=Mart%C3%ADn+Abadi%2C+Ashish+Agarwal%2C+Paul+Barham%2C+Eugene+Brevdo%2C+Zhifeng+Chen%2C+Craig+Citro%2C+Greg+S%2E+Corrado%2C+Andy+Davis%2C+Jeffrey+Dean%2C+Matthieu+Devin%2C+Sanjay+Ghemawat%2C+Ian+Goodfellow%2C+Andrew+Harp%2C+Geoffrey+I)
2. Jesse Alama, Daniel Kühlwein, and Josef Urban. Automated and Human Proofs in General Mathematics: An Initial Comparison. In Nikolaj Bjørner and Andrei Voronkov (eds.), LPAR, volume 7180 of LNCS, pp. 37–45. Springer, 2012. ISBN 978-3-642-28716-9. [find](https://scholar.google.com/scholar?q=Jesse+Alama%2C+Daniel+K%C3%BChlwein%2C+and+Josef+Urban%2E+Automated+and+Human+Proofs+in+General+Mathematics%3A+An+Initial+Comparison%2E+In+Nikolaj+Bj%C3%B8rner+and+Andrei+Voronkov+%28eds%2E%29%2C+LPAR%2C+volume+7180+of+LNCS%2C+pp%2E+3)
3. Alexander A Alemi, Francois Chollet, Geoffrey Irving, Niklas Een, Christian Szegedy, and Josef Urban. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235[–2243, 2016](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/).
4. Serge Autexier and Dieter Hutter. Structure formation in large theories. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (eds.), Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, volume 9150… [find](https://scholar.google.com/scholar?q=Serge+Autexier+and+Dieter+Hutter%2E+Structure+formation+in+large+theories%2E+In+Manfred+Kerber%2C+Jacques+Carette%2C+Cezary+Kaliszyk%2C+Florian+Rabe%2C+and+Volker+Sorge+%28eds%2E%29%2C+Intelligent+Computer+Mathematics+%2D+)
5. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Ma-tuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (eds.), Intelligent Computer Mathematics - I… [find](https://scholar.google.com/scholar?q=Grzegorz+Bancerek%2C+Czes%C5%82aw+Byli%C5%84ski%2C+Adam+Grabowski%2C+Artur+Korni%C5%82owicz%2C+Roman+Ma%2Dtuszewski%2C+Adam+Naumowicz%2C+Karol+P%C4%85k%2C+and+Josef+Urban%2E+Mizar%3A+State%2Dof%2Dthe%2Dart+and+beyond%2E+In+Manfred+Kerber%2C+Jacques+C)
6. Springer, 2015. doi: 10.1007/978-3-319-20615-8. URL http://dx.doi.org/10.1007/978-3-319-20615-8. — [doi:10.1007/978-3-319-20615-8](https://doi.org/10.1007/978-3-319-20615-8) [↗](http://dx.doi.org/10.1007/978-3-319-20615-8)
7. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formalized Reasoning, 9(1):101–148, 2016. doi: 10.6092/issn.1972-5787/4593. URL http://dx.doi.org/10.6092/issn.1972-5787/4593. [↗](http://dx.doi.org/10.6092/issn.1972-5787/4593)
8. S. Loos, G. Irving, C. Szegedy, and C. Kaliszyk Deep Network Guided Proof Search Chris Olah. Understanding LSTM networks, 2015. URL [https://colah.github.io/posts/2015-08-Understanding-LSTMs](https://colah.github.io/posts/2015-08-Understanding-LSTMs). [↗](https://colah.github.io/posts/2015-08-Understanding-LSTMs)
9. Junyoung Chung, Caglar Gulcehre, Kyunghyun Cho, and Yoshua Bengio. Gated feedback recurrent neural networks. arXiv preprint arXiv:1502.02367, 2015. [find](https://scholar.google.com/scholar?q=Junyoung+Chung%2C+Caglar+Gulcehre%2C+Kyunghyun+Cho%2C+and+Yoshua+Bengio%2E+Gated+feedback+recurrent+neural+networks%2E+arXiv+preprint+arXiv%3A1502%2E02367%2C+2015%2E)
10. Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz. Learning from Previous Proof Experience. Technical Report AR99-4, Institut für Informatik, Technische Universität München, 1999. [find](https://scholar.google.com/scholar?q=J%C3%B6rg+Denzinger%2C+Matthias+Fuchs%2C+Christoph+Goller%2C+and+Stephan+Schulz%2E+Learning+from+Previous+Proof+Experience%2E+Technical+Report+AR99%2D4%2C+Institut+f%C3%BCr+Informatik%2C+Technische+Universit%C3%A4t+M%C3%BCnchen%2C+1999%2E)
11. Michael Färber and Chad E. Brown. Internal guidance for Satallax. In Nicola Olivetti and Ashish Tiwari (eds.), International Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pp. 349–361. [find](https://scholar.google.com/scholar?q=Michael+F%C3%A4rber+and+Chad+E%2E+Brown%2E+Internal+guidance+for+Satallax%2E+In+Nicola+Olivetti+and+Ashish+Tiwari+%28eds%2E%29%2C+International+Joint+Conference+on+Automated+Reasoning+%28IJCAR+2016%29%2C+volume+9706+of+LNCS%2C+)
12. Christoph Goller and Andreas Kuchler. Learning task-dependent distributed representations by backpropagation through structure. In Neural Networks, 1996., IEEE International Conference on, volume 1, pp. 347–352. [find](https://scholar.google.com/scholar?q=Christoph+Goller+and+Andreas+Kuchler%2E+Learning+task%2Ddependent+distributed+representations+by+backpropagation+through+structure%2E+In+Neural+Networks%2C+1996%2E%2C+IEEE+International+Conference+on%2C+volume+1%2C+p)
13. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. [find](https://scholar.google.com/scholar?q=Adam+Grabowski%2C+Artur+Korni%C5%82owicz%2C+and+Adam+Naumowicz%2E+Mizar+in+a+nutshell%2E+J%2E+Formalized+Reasoning%2C+3%282%29%3A153%E2%80%93245%2C+2010%2E)
14. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar - foreword. J. Autom. Reasoning, 55(3):191–198, 2015. doi: 10.1007/s10817-015-9345-1. URL http://dx.doi.org/10.1007/s10817-015-9345-1. — [doi:10.1007/s10817-015-9345-1](https://doi.org/10.1007/s10817-015-9345-1) [↗](http://dx.doi.org/10.1007/s10817-015-9345-1)
15. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Jos… [find](https://scholar.google.com/scholar?q=Thomas+C%2E+Hales%2C+Mark+Adams%2C+Gertrud+Bauer%2C+Dat+Tat+Dang%2C+John+Harrison%2C+Truong+Le+Hoang%2C+Cezary+Kaliszyk%2C+Victor+Magron%2C+Sean+McLaughlin%2C+Thang+Tat+Nguyen%2C+Truong+Quang+Nguyen%2C+Tobias+Nipkow%2C+Steven+)
16. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg H. Siekmann (ed.), Computational Logic, volume 9 of Handbook of the History of Logic, pp. 135 – 214. North-Holland, 2014. doi: http://dx.doi.org/10.1016/B978-0-444-51624-4.50004-6. URL http://www.sciencedi… [↗](http://dx.doi.org/10.1016/B978-0-444-51624-4.50004-6)
17. Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. [Deep residual learning for image recognition](https://md.research.elamur.ai/free/en/papers/he-2015-deep-residual-learning-image-recognition/). arXiv preprint arXiv:1512.03385, 2015.
18. Geoffrey Hinton, Li Deng, Dong Yu, George E Dahl, Abdel-rahman Mohamed, Navdeep Jaitly, Andrew Senior, Vincent Vanhoucke, Patrick Nguyen, Tara N Sainath, and Brian Kingsbury. Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups. IEEE Signal Proce… [find](https://scholar.google.com/scholar?q=Geoffrey+Hinton%2C+Li+Deng%2C+Dong+Yu%2C+George+E+Dahl%2C+Abdel%2Drahman+Mohamed%2C+Navdeep+Jaitly%2C+Andrew+Senior%2C+Vincent+Vanhoucke%2C+Patrick+Nguyen%2C+Tara+N+Sainath%2C+and+Brian+Kingsbury%2E+Deep+neural+networks+for+)
19. Geoffrey E Hinton, Nitish Srivastava, Alex Krizhevsky, Ilya Sutskever, and Ruslan R Salakhutdinov. Improving neural networks by preventing co-adaptation of feature detectors. arXiv preprint arXiv:1207.0580, 2012b. [find](https://scholar.google.com/scholar?q=Geoffrey+E+Hinton%2C+Nitish+Srivastava%2C+Alex+Krizhevsky%2C+Ilya+Sutskever%2C+and+Ruslan+R+Salakhutdinov%2E+Improving+neural+networks+by+preventing+co%2Dadaptation+of+feature+detectors%2E+arXiv+preprint+arXiv%3A1207)
20. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3): 245–256, 2015a. doi: 10.1007/s10817-015-9330-8. URL http://dx.doi.org/10.1007/s10817-015-9330-8. [↗](http://dx.doi.org/10.1007/s10817-015-9330-8)
21. S. Loos, G. Irving, C. Szegedy, and C. Kaliszyk Deep Network Guided Proof Search Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.), Logic for Programming, Artificial Intellige… [find](https://scholar.google.com/scholar?q=S%2E+Loos%2C+G%2E+Irving%2C+C%2E+Szegedy%2C+and+C%2E+Kaliszyk+Deep+Network+Guided+Proof+Search+Cezary+Kaliszyk+and+Josef+Urban%2E+FEMaLeCoP%3A+Fairly+efficient+machine+learning+connection+prover%2E+In+Martin+Davis%2C+Ansga)
22. Springer, 2015b. ISBN 978-3-662-48898-0. doi: 10.1007/978-3-662-48899-7_7. URL http://dx.doi.org/10.1007/978-3-662-48899-7_7. — [doi:10.1007/978-3-662-48899-7_7](https://doi.org/10.1007/978-3-662-48899-7_7) [↗](http://dx.doi.org/10.1007/978-3-662-48899-7_7)
23. Yoon Kim. [Convolutional neural networks for sentence classification](https://md.research.elamur.ai/free/en/papers/kim-2014-convolutional-neural-networks-sentence-classification/). arXiv:1408.5882, 2014.
24. Diederik Kingma and Jimmy Ba. [Adam: A method for stochastic optimization](https://md.research.elamur.ai/free/en/papers/kingma-2014-adam-method-stochastic-optimization/). arXiv preprint arXiv:1412.6980, 2014.
25. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. Commun. ACM, 53(6):107–115, 2010. [find](https://scholar.google.com/scholar?q=Gerwin+Klein%2C+June+Andronick%2C+Kevin+Elphinstone%2C+Gernot+Heiser%2C+David+Cock%2C+Philip+Derrin%2C+Dhammika+Elkaduwe%2C+Kai+Engelhardt%2C+Rafal+Kolanski%2C+Michael+Norrish%2C+Thomas+Sewell%2C+Harvey+Tuch%2C+and+Simon+Win)
26. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith (eds.), CAV, volume 8044 of LNCS, pp. 1–35. Springer, 2013. ISBN 978-3-642-39798-1. [find](https://scholar.google.com/scholar?q=Laura+Kov%C3%A1cs+and+Andrei+Voronkov%2E+First%2Dorder+theorem+proving+and+Vampire%2E+In+Natasha+Sharygina+and+Helmut+Veith+%28eds%2E%29%2C+CAV%2C+volume+8044+of+LNCS%2C+pp%2E+1%E2%80%9335%2E+Springer%2C+2013%2E+ISBN+978%2D3%2D642%2D39798%2D1%2E)
27. Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. [Imagenet classification with deep convolutional neural networks](https://md.research.elamur.ai/free/en/papers/krizhevsky-2012-imagenet-classification-deep-convolutional/). In Advances in neural information processing systems, pp. 1097–1105, 2012.
28. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler (eds.), IJCAR, volume 7364 of LNCS, pp. 378–392. Springer, 2012. ISBN 978-3-… [find](https://scholar.google.com/scholar?q=Daniel+K%C3%BChlwein%2C+Twan+van+Laarhoven%2C+Evgeni+Tsivtsivadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+evaluation+of+premise+selection+techniques+for+large+theory+mathematics%2E+In+Bernhard+Gramlich%2C+Dale+)
29. Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. Proceedings of the IEEE, 86(11):2278–2324, 1998. [find](https://scholar.google.com/scholar?q=Yann+LeCun%2C+L%C3%A9on+Bottou%2C+Yoshua+Bengio%2C+and+Patrick+Haffner%2E+Gradient%2Dbased+learning+applied+to+document+recognition%2E+Proceedings+of+the+IEEE%2C+86%2811%29%3A2278%E2%80%932324%2C+1998%2E)
30. Norman Megill. Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville, North Carolina, 2007. ISBN 978-1-4116-3724-5. URL [http://us.metamath.org/downloads/metamath.pdf](http://us.metamath.org/downloads/metamath.pdf). [↗](http://us.metamath.org/downloads/metamath.pdf)
31. Aäron van den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew Senior, and Koray Kavukcuoglu. [Wavenet: A generative model for raw audio](https://md.research.elamur.ai/free/en/papers/oord-2016-wavenet-generative-model-raw-audio/). arXiv preprint arXiv:1609.03499, 2016.
32. Tim Rocktäschel and Sebastian Riedel. Learning knowledge base inference with neural theorem provers. 5th Workshop on Automated Knowledge Base Construction (AKBC) 2016, 2016. [find](https://scholar.google.com/scholar?q=Tim+Rockt%C3%A4schel+and+Sebastian+Riedel%2E+Learning+knowledge+base+inference+with+neural+theorem+provers%2E+5th+Workshop+on+Automated+Knowledge+Base+Construction+%28AKBC%29+2016%2C+2016%2E)
33. Tim Rocktäschel, Edward Grefenstette, Karl Moritz Hermann, Tomáš Kočiskỳ, and Phil Blunsom. [Reasoning about entailment with neural attention](https://md.research.elamur.ai/free/en/papers/rocktaschel-2015-reasoning-about-entailment-neural-attention/). arXiv preprint arXiv:1509.06664, 2015.
34. Stephan Schulz. Learning search control knowledge for equational deduction, volume 230 of DISKI. Infix Akademische Verlagsgesellschaft, 2000. ISBN 978-3-89838-230-4. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+Learning+search+control+knowledge+for+equational+deduction%2C+volume+230+of+DISKI%2E+Infix+Akademische+Verlagsgesellschaft%2C+2000%2E+ISBN+978%2D3%2D89838%2D230%2D4%2E)
35. S. Loos, G. Irving, C. Szegedy, and C. Kaliszyk arXiv preprint Deep Network Guided Proof Search Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conferenc… — [doi:10.1007/978-3-642-45221-5_49](https://doi.org/10.1007/978-3-642-45221-5_49) [find](https://scholar.google.com/scholar?q=S%2E+Loos%2C+G%2E+Irving%2C+C%2E+Szegedy%2C+and+C%2E+Kaliszyk+arXiv+preprint+Deep+Network+Guided+Proof+Search+Stephan+Schulz%2E+System+description%3A+E+1%2E8%2E+In+Kenneth+L%2E+McMillan%2C+Aart+Middeldorp%2C+and+Andrei+Voronkov+)
36. Stephan Schulz. E 1.9.1 User Manual (preliminary version), 2016. URL [http://www.lehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_1.9.1/eprover.pdf](http://www.lehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_1.9.1/eprover.pdf). [↗](http://www.lehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_1.9.1/eprover.pdf)
37. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. Nature, 529 (7587):484–489, 2016. [find](https://scholar.google.com/scholar?q=David+Silver%2C+Aja+Huang%2C+Chris+J+Maddison%2C+Arthur+Guez%2C+Laurent+Sifre%2C+George+Van+Den+Driessche%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Veda+Panneershelvam%2C+Marc+Lanctot%2C+et+al%2E+Mastering+the+game+)
38. Richard Socher, Cliff C Lin, Chris Manning, and Andrew Y Ng. Parsing natural scenes and natural language with recursive neural networks. In Proceedings of the 28th international conference on machine learning (ICML-11), pp. 129–136, 2011. [find](https://scholar.google.com/scholar?q=Richard+Socher%2C+Cliff+C+Lin%2C+Chris+Manning%2C+and+Andrew+Y+Ng%2E+Parsing+natural+scenes+and+natural+language+with+recursive+neural+networks%2E+In+Proceedings+of+the+28th+international+conference+on+machine+)
39. Geoff Sutcliffe. The TPTP problem library and associated infrastructure. J. Autom. Reasoning, 43(4):337–362, 2009. doi: 10.1007/s10817-009-9143-8. URL http://dx.doi.org/10.1007/s10817-009-9143-8. — [doi:10.1007/s10817-009-9143-8](https://doi.org/10.1007/s10817-009-9143-8) [↗](http://dx.doi.org/10.1007/s10817-009-9143-8)
40. Christian Suttner and Wolfgang Ertel. Automatic acquisition of search guiding heuristics. In International Conference on Automated Deduction, pp. 470–484. Springer, 1990. [find](https://scholar.google.com/scholar?q=Christian+Suttner+and+Wolfgang+Ertel%2E+Automatic+acquisition+of+search+guiding+heuristics%2E+In+International+Conference+on+Automated+Deduction%2C+pp%2E+470%E2%80%93484%2E+Springer%2C+1990%2E)
41. Christian Szegedy, Wei Liu, Yangqing Jia, Pierre Sermanet, Scott Reed, Dragomir Anguelov, Dumitru Erhan, Vincent Vanhoucke, and Andrew Rabinovich. Going deeper with convolutions. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 1–9, 2015. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2C+Wei+Liu%2C+Yangqing+Jia%2C+Pierre+Sermanet%2C+Scott+Reed%2C+Dragomir+Anguelov%2C+Dumitru+Erhan%2C+Vincent+Vanhoucke%2C+and+Andrew+Rabinovich%2E+Going+deeper+with+convolutions%2E+In+Proceedings+of+the)
42. Kai Sheng Tai, Richard Socher, and Christopher D Manning. Improved semantic representations from tree-structured long short-term memory networks. arXiv preprint arXiv:1503.00075, 2015. [find](https://scholar.google.com/scholar?q=Kai+Sheng+Tai%2C+Richard+Socher%2C+and+Christopher+D+Manning%2E+Improved+semantic+representations+from+tree%2Dstructured+long+short%2Dterm+memory+networks%2E+arXiv+preprint+arXiv%3A1503%2E00075%2C+2015%2E)
43. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. doi: 10.1007/s10817-006-9032-3. URL http://dx.doi.org/10.1007/s10817-006-9032-3. — [doi:10.1007/s10817-006-9032-3](https://doi.org/10.1007/s10817-006-9032-3) [↗](http://dx.doi.org/10.1007/s10817-006-9032-3)
44. Josef Urban, Jiří Vyskočil, and Petr Štěpánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe (eds.), TABLEAUX, volume 6793 of LNCS, pp. 263– 277. Springer, 2011. ISBN 978-3-642-22118-7. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Ji%C5%99%C3%AD+Vysko%C4%8Dil%2C+and+Petr+%C5%A0t%C4%9Bp%C3%A1nek%2E+MaLeCoP%3A+Machine+learning+connection+prover%2E+In+Kai+Br%C3%BCnnler+and+George+Metcalfe+%28eds%2E%29%2C+TABLEAUX%2C+volume+6793+of+LNCS%2C+pp%2E+263%E2%80%93+277%2E+Springer%2C+2011%2E+ISB)
45. Markus Wenzel. Isar - A generic interpretative approach to readable formal proof documents. In Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, and Laurent Théry (eds.), Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, volume 1690 of LNCS, pp.… [find](https://scholar.google.com/scholar?q=Markus+Wenzel%2E+Isar+%2D+A+generic+interpretative+approach+to+readable+formal+proof+documents%2E+In+Yves+Bertot%2C+Gilles+Dowek%2C+Andr%C3%A9+Hirschowitz%2C+Christine+Paulin%2DMohring%2C+and+Laurent+Th%C3%A9ry+%28eds%2E%29%2C+Theorem)
46. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016. [find](https://scholar.google.com/scholar?q=Daniel+Whalen%2E+Holophrasm%3A+a+neural+automated+theorem+prover+for+higher%2Dorder+logic%2E+arXiv+preprint+arXiv%3A1608%2E02644%2C+2016%2E)
47. S. Loos, G. Irving, C. Szegedy, and C. Kaliszyk Deep Network Guided Proof Search [find](https://scholar.google.com/scholar?q=S%2E+Loos%2C+G%2E+Irving%2C+C%2E+Szegedy%2C+and+C%2E+Kaliszyk+Deep+Network+Guided+Proof+Search)

*Updated 2 November 2026*