Advertisement

Machine Learning for Mathematical Software

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

Abstract

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.

Keywords

Machine learning Mathematical software 

Notes

Acknowledgements

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.

References

  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).  https://doi.org/10.1137/0213054MathSciNetCrossRefzbMATHGoogle 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). https://doi.org/10.1145/3087604.3087622
  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).  https://doi.org/10.1016/j.jsc.2015.11.002MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-39320-4_2CrossRefGoogle Scholar
  7. 7.
    Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reasoning 53(2), 141–172 (2014).  https://doi.org/10.1007/s10817-014-9301-5CrossRefzbMATHGoogle Scholar
  8. 8.
    Brown, C.: Companion to the tutorial: cylindrical algebraic decomposition. In: Presented at ISSAC 2004 (2004). http://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf
  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). https://doi.org/10.1145/1277548.1277557
  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). https://doi.org/10.1145/1005285.1005298
  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).  https://doi.org/10.1007/978-3-642-02614-0_21CrossRefGoogle Scholar
  13. 13.
    Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995).  https://doi.org/10.1023/A:1022627411411CrossRefzbMATHGoogle 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). https://doi.org/10.1109/SYNASC.2012.68
  15. 15.
    Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbolic Comput. 5(1–2), 29–35 (1988).  https://doi.org/10.1016/S0747-7171(88)80004-XMathSciNetCrossRefzbMATHGoogle 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). https://doi.org/10.1145/1005285.1005303
  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).  https://doi.org/10.1007/978-3-319-08434-3_5CrossRefGoogle 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). https://doi.org/10.1145/2755996.2756678
  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).  https://doi.org/10.1007/978-3-319-45641-6_12CrossRefGoogle 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). https://doi.org/10.1145/2755996.2756646
  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, https://doi.org/10.1145/3092566CrossRefGoogle 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). https://doi.org/10.1109/SYNASC.2016.020
  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).  https://doi.org/10.1007/978-3-319-08434-3_8CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-32859-1_21CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-39634-2_6CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-31365-3_30CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-66263-3_8CrossRefGoogle 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). https://doi.org/10.1145/309831.309892
  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).  https://doi.org/10.1007/978-3-319-08434-3_16CrossRefzbMATHGoogle 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). https://doi.org/10.1145/775832.775945
  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).  https://doi.org/10.1016/j.jsc.2010.08.017MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/s11786-017-0319-zMathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-540-85110-3_44CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-31374-5_19CrossRefGoogle 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). https://doi.org/10.1145/3017680.3022464
  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, https://doi.org/10.1145/3057270CrossRefGoogle 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, https://doi.org/10.1145/3068287CrossRefGoogle Scholar
  41. 41.
    Zhang, D., Tsai, J.: Machine learning and software engineering. Software Qual. J. 11(2), 87–119 (2003).  https://doi.org/10.1109/TAI.2002.1180784CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Coventry UniversityCoventryUK

Personalised recommendations