Machine Learning for Mathematical Software

  • Matthew EnglandEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10931)


While there has been some discussion on how Symbolic Computation could be used for AI there is little literature on applications in the other direction. However, recent results for quantifier elimination suggest that, given enough example problems, there is scope for machine learning tools like Support Vector Machines to improve the performance of Computer Algebra Systems. We survey the author’s own work and similar applications for other mathematical software.

It may seem that the inherently probabilistic nature of machine learning tools would invalidate the exact results prized by mathematical software. However, algorithms and implementations often come with a range of choices which have no effect on the mathematical correctness of the end result but a great effect on the resources required to find it, and thus here, machine learning can have a significant impact.


Machine learning Mathematical software 



Surveyed work in Sect. 2 was supported by the European Union’s Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689 (SC\(^2\)); and EPSRC grant EP/J003247/1. The author is now supported by EPSRC grant EP/R019622/1.


  1. 1.
    Alemi, A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: DeepMath - deep sequence models for premise selection. In: Proceedings 30th International Conference on Neural Information Processing Systems (NIPS 2016), pp. 2243–2251. Curran Associates Inc. (2016)Google Scholar
  2. 2.
    Arnon, D., Collins, G., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13, 865–877 (1984). Scholar
  3. 3.
    Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability, vol. 185. Frontiers in Artificial Intelligence and Applications. IOS Press (2009)Google Scholar
  4. 4.
    Bradford, R., Davenport, J., England, M., Errami, H., Gerdt, V., Grigoriev, D., Hoyt, C., Košta, M., Radulescu, O., Sturm, T., Weber, A.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of 2017 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), pp. 45–52. ACM (2017).
  5. 5.
    Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symbolic Comput. 76, 1–35 (2016). Scholar
  6. 6.
    Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulation for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 19–34. Springer, Heidelberg (2013). Scholar
  7. 7.
    Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reasoning 53(2), 141–172 (2014). Scholar
  8. 8.
    Brown, C.: Companion to the tutorial: cylindrical algebraic decomposition. In: Presented at ISSAC 2004 (2004).
  9. 9.
    Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of 2007 International Symposium on Symbolic and Algebraic Computation (ISSAC 2007), pp. 54–60. ACM (2007).
  10. 10.
    Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gröbner bases. Technical report, 91–06. RISC, Johannes Kepler University (1991)Google Scholar
  11. 11.
    Carette, J.: Understanding expression simplification. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), pp. 72–79. ACM (2004).
  12. 12.
    Carette, J., Farmer, W.M.: A review of mathematical knowledge management. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS (LNAI), vol. 5625, pp. 233–246. Springer, Heidelberg (2009). Scholar
  13. 13.
    Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995). Scholar
  14. 14.
    Davenport, J., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, pp. 83–88. IEEE (2012).
  15. 15.
    Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbolic Comput. 5(1–2), 29–35 (1988). Scholar
  16. 16.
    Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), pp. 111–118. ACM (2004).
  17. 17.
    England, M., et al.: Problem Formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 45–60. Springer, Cham (2014). Scholar
  18. 18.
    England, M., Bradford, R., Davenport, J.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of 2015 International Symposium on Symbolic and Algebraic Computation (ISSAC 2015), pp. 165–172. ACM (2015).
  19. 19.
    England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 172–192. Springer, Cham (2016). Scholar
  20. 20.
    Fukasaku, R., Iwane, H., Sato, Y.: Real quantifier elimination by computation of comprehensive Gröbner systems. In: Proceedings of 2015 International Symposium on Symbolic and Algebraic Computation (ISSAC 2015), pp. 173–180. ACM (2015).
  21. 21.
    Ghaffarian, S., Shahriari, H.: Software vulnerability analysis and discovery using machine-learning and data-mining techniques: a survey. ACM Comput. Surv. 50(4) (2017). 36 pages, Article no. 56, Scholar
  22. 22.
    Huang, Z., England, M., Davenport, J., Paulson, L.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), pp. 45–52. IEEE (2016).
  23. 23.
    Huang, Z., et al.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 92–107. Springer, Cham (2014). Scholar
  24. 24.
    Kobayashi, M., Iwane, H., Matsuzaki, T., Anai, H.: Efficient subformula orders for real quantifier elimination of non-prenex formulas. In: Kotsireas, I.S., Rump, S.M., Yap, C.K. (eds.) MACIS 2015. LNCS, vol. 9582, pp. 236–251. Springer, Cham (2016). Scholar
  25. 25.
    Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013). Scholar
  26. 26.
    Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 378–392. Springer, Heidelberg (2012). Scholar
  27. 27.
    Liang, J.H., V.K., H.G., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119–135. Springer, Cham (2017). Scholar
  28. 28.
    McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of 1999 International Symposium on Symbolic and Algebraic Computation (ISSAC 1999), pp. 145–149. ACM (1999).
  29. 29.
    Schöneberg, U., Sperber, W.: POS tagging and its applications for mathematics. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 213–223. Springer, Cham (2014). Scholar
  30. 30.
    Seshia, S., Lahiri, S., Bryant, R.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proceedings of 2003 Design Automation Conference, pp. 425–430 (2003).
  31. 31.
    Shawe-Taylor, J., Cristianini, N.: Kernel methods for pattern analysis. CUP (2004)Google Scholar
  32. 32.
    Stoutemyer, D.: Ten commandments for good default expression simplification. J. Symbolic Comput. 46(7), 859–887 (2011). Scholar
  33. 33.
    Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comp. Sci. 11(3), 483–502 (2017). Scholar
  34. 34.
    Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Empirically Successful Automated Reasoning in Large Theories (ESARLT 2007), CEUR Workshop Proceedings, vol. 257, 14 pages. CEUR-WS (2007)Google Scholar
  35. 35.
    Řehůřek, R., Sojka, P.: Automated classification and categorization of mathematical knowledge. In: Autexier, S., et al. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 543–557. Springer, Heidelberg (2008). Scholar
  36. 36.
    Wilson, D.J., Bradford, R.J., Davenport, J.H.: Speeding up cylindrical algebraic decomposition by Gröbner Bases. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 280–294. Springer, Heidelberg (2012). Scholar
  37. 37.
    Wu, H.: Improving SAT-solving with machine learning. In: Proceedings of the 2017 ACM SIGCSE Technical Symposium Computer Science Education, pp. 787–788. ACM (2017).
  38. 38.
    Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565–606 (2008)zbMATHGoogle Scholar
  39. 39.
    Yadollahi, A., Shahraki, A., Zaiane, O.: Current state of text sentiment analysis from opinion to emotion mining. ACM Comput. Surv. 50(2) (2017). 33 pages, Article no. 25, Scholar
  40. 40.
    Yau, K.L., Qadir, J., Khoo, H., Ling, M., Komisarczuk, P.: A survey on reinforcement learning models and algorithms for traffic signal control. ACM Comput. Surv. 50(3) (2017). 38 pages, Article no. 34, Scholar
  41. 41.
    Zhang, D., Tsai, J.: Machine learning and software engineering. Software Qual. J. 11(2), 87–119 (2003). Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Coventry UniversityCoventryUK

Personalised recommendations