Advertisement

Tree-Structure CNN for Automated Theorem Proving

  • Kebin PengEmail author
  • Dianfu Ma
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10635)

Abstract

The most difficult and heavy work of Automated Theorem Proving (ATP) is that people should search in millions of intermediate steps to finish proof. In this paper, we present a novel neural network, which can effectively help people to finish this work. Specifically, we design a tree-structure CNN, involving bidirectional LSTM. We compare our model with other neural network models and make experiments on HOLStep dataset, which is a machine learning dataset for Higher-order logic theorem proving. Being compared to previous approaches, our model improves accuracy significantly, reaching 90% accuracy on the test set.

References

  1. 1.
    Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191–213 (2014)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Alemi, A.A., Chollet, F., Irving, G., Szegedy, C., Urban, J.: DeepMath-deep sequence models for premise selection. arXiv preprint arXiv:1606.04442 (2016)
  3. 3.
    Aspinall, D., Kaliszyk, C.: What’s in a theorem name? In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 459–465. Springer, Cham (2016). doi: 10.1007/978-3-319-43144-4_28 CrossRefGoogle Scholar
  4. 4.
    Autexier, S., Hutter, D.: Structure formation in large theories. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 155–170. Springer, Cham (2015). doi: 10.1007/978-3-319-20615-8_10 CrossRefGoogle Scholar
  5. 5.
    Cezary, K., Franois, C., Christian, S.: HolStep: machine learning dataset for higher-order logic theorem proving. ICLR (2016)Google Scholar
  6. 6.
    Färber, M., Brown, C.: Internal guidance for satallax. arXiv preprint arXiv:1605.09293 (2016)
  7. 7.
    He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. arXiv preprint arXiv:1512.03385 (2015)
  8. 8.
    Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735–1780 (1997)CrossRefGoogle Scholar
  9. 9.
    Hoder, K., Voronkov, A.: Sine Qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22438-6_23 CrossRefGoogle Scholar
  10. 10.
    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)Google Scholar
  11. 11.
    Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_1 CrossRefGoogle Scholar
  12. 12.
    Mikolov, T., Sutskever, I., Chen, K., Corrado, G.S., Dean, J.: Distributed representations of words and phrases and their compositionality. In: Advances in Neural Information Processing Systems, pp. 3111–3119 (2013)Google Scholar
  13. 13.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  14. 14.
    Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. arXiv preprint arXiv:1409.1556 (2014)
  15. 15.
    Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Voronkov, A.: Logic for Programming, Artificial Intelligence, and Reasoning. Springer, Heidelberg (2010)zbMATHGoogle Scholar
  17. 17.
    Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999). doi: 10.1007/3-540-48256-3_12 CrossRefGoogle Scholar
  18. 18.
    Wiedijk, F.: The Seventeen Provers of the World. Lecture Notes in Computer Science, vol. 3600. Springer, Heidelberg (2006)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.School of Computer Science and EngineeringBeihang UniversityBeijingChina

Personalised recommendations