Advertisement

Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness

  • Dorian Florescu
  • Matthew EnglandEmail author
Conference paper
  • 29 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11989)

Abstract

Our topic is the use of machine learning to improve software by making choices which do not compromise the correctness of the output, but do affect the time taken to produce such output. We are particularly concerned with computer algebra systems (CASs), and in particular, our experiments are for selecting the variable ordering to use when performing a cylindrical algebraic decomposition of n-dimensional real space with respect to the signs of a set of polynomials.

In our prior work we explored the different ML models that could be used, and how to identify suitable features of the input polynomials. In the present paper we both repeat our prior experiments on problems which have more variables (and thus exponentially more possible orderings), and examine the metric which our ML classifiers targets. The natural metric is computational runtime, with classifiers trained to pick the ordering which minimises this. However, this leads to the situation where models do not distinguish between any of the non-optimal orderings, whose runtimes may still vary dramatically. In this paper we investigate a modification to the cross-validation algorithms of the classifiers so that they do distinguish these cases, leading to improved results.

Keywords

Machine Learning Cross-validation Computer algebra Symbolic computation Cylindrical algebraic decomposition 

Notes

Acknowledgements

This work is funded by EPSRC Project EP/R019622/1: Embedding Machine Learning within Quantifier Elimination Procedures.

References

  1. 1.
    Bishop, C.: Pattern Recognition and Machine Learning. Springer, New York (2006)zbMATHGoogle Scholar
  2. 2.
    Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2014. LNCS, vol. 8660, pp. 44–58. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10515-4_4CrossRefGoogle Scholar
  3. 3.
    Bradford, R., et al.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC 2017, pp. 45–52. ACM (2017). https://doi.org/10.1145/3087604.3087622
  4. 4.
    Bradford, R., et al.: Identifying the parametric occurrence of multiple steady states for some biological networks. J. Symb. Comput. 98, 84–119 (2020).  https://doi.org/10.1016/j.jsc.2019.07.008MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symb. 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.: Machine learning and automated theorem proving. Technical report. UCAM-CL-TR-792, University of Cambridge, Computer Laboratory (2010)Google Scholar
  8. 8.
    Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reason. 53, 141–172 (2014).  https://doi.org/10.1007/s10817-014-9301-5CrossRefzbMATHGoogle Scholar
  9. 9.
    Brown, C.: Companion to the tutorial: cylindrical algebraic decomposition. Presented at ISSAC 2004 (2004). http://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf
  10. 10.
    Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54–60. ACM (2007). https://doi.org/10.1145/1277548.1277557
  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.
    Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation. Springer, New York (1998).  https://doi.org/10.1007/978-3-7091-9459-1CrossRefzbMATHGoogle Scholar
  13. 13.
    Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W., Sato, Y. (eds.) Computer Mathematics, pp. 199–221. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-43799-5_17CrossRefGoogle Scholar
  14. 14.
    Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pp. 95–102. ACM (2009). https://doi.org/10.1145/1576702.1576718
  15. 15.
    Chinchor, N.: MUC-4 evaluation metrics. In: Proceedings of the 4th Conference on Message Understanding (MUC4 1992), pp. 22–29. Association for Computational Linguistics (1992). https://doi.org/10.3115/1072064.1072067
  16. 16.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975).  https://doi.org/10.1007/3-540-07407-4_17. Reprinted in the collection [12]CrossRefGoogle Scholar
  17. 17.
    Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299–328 (1991).  https://doi.org/10.1016/S0747-7171(08)80152-6MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    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). http://dx.doi.org/10.1109/SYNASC.2012.68
  19. 19.
    Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC 2004, pp. 111–118. ACM (2004). https://doi.org/10.1145/1005285.1005303
  20. 20.
    England, M.: Machine learning for mathematical software. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) ICMS 2018. LNCS, vol. 10931, pp. 165–174. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96418-8_20CrossRefzbMATHGoogle Scholar
  21. 21.
    England, M., Bradford, R., Davenport, J.: Cylindrical algebraic decomposition with equational constraints. J. Symb. Comput. (2019). https://doi.org/10.1016/j.jsc.2019.07.019
  22. 22.
    England, M., Bradford, R., Davenport, J.H., Wilson, D.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 450–457. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44199-2_68CrossRefGoogle Scholar
  23. 23.
    England, M., Florescu, D.: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 93–108. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-23250-4_7CrossRefGoogle Scholar
  24. 24.
    England, M., Wilson, D., Bradford, R., Davenport, J.H.: Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 458–465. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44199-2_69CrossRefGoogle Scholar
  25. 25.
    Florescu, D., England, M.: Algorithmically generating new algebraic features of polynomial systems for machine learning. In: Abbott, J., Griggio, A. (eds.) Proceedings of the 4th Workshop on Satisfiability Checking and Symbolic Computation (SC\(^2\) 2019). No. 2460 in CEUR Workshop Proceedings (2019). http://ceur-ws.org/Vol-2460/
  26. 26.
    Ghaffarian, S., Shahriari, H.: Software vulnerability analysis and discovery using machine-learning and data-mining techniques: a survey. ACM Comput. Surv. 50(4) (2017).  https://doi.org/10.1145/3092566
  27. 27.
    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
  28. 28.
    Huang, Z., England, M., Wilson, D., Bridge, J., Davenport, J., Paulson, L.: Using machine learning to improve cylindrical algebraic decomposition. Math. Comput. Sci. 13(4), 461–488 (2019).  https://doi.org/10.1007/s11786-019-00394-8MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L.C., Bridge, J.: 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
  30. 30.
    Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31365-3_27CrossRefGoogle Scholar
  31. 31.
    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
  32. 32.
    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
  33. 33.
    Kuipers, J., Ueda, T., Vermaseren, J.: Code optimization in FORM. Comput. Phys. Commun. 189, 1–19 (2015).  https://doi.org/10.1016/j.cpc.2014.08.008CrossRefzbMATHGoogle Scholar
  34. 34.
    Liang, J.H., Hari Govind, V.K., 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_8CrossRefzbMATHGoogle Scholar
  35. 35.
    Mulligan, C., Bradford, R., Davenport, J., England, M., Tonks, Z.: Non-linear real arithmetic benchmarks derived from automated reasoning in economics. In: Bigatti, A., Brain, M. (eds.) Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation (SC\(^2\) 2018). No. 2189 in CEUR Workshop Proceedings, pp. 48–60 (2018). http://ceur-ws.org/Vol-2189/
  36. 36.
    Mulligan, C.B., Davenport, J.H., England, M.: TheoryGuru: a mathematica package to apply quantifier elimination technology to economics. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) ICMS 2018. LNCS, vol. 10931, pp. 369–378. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96418-8_44CrossRefGoogle Scholar
  37. 37.
    Pedregosa, F., et al.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011). http://www.jmlr.org/papers/v12/pedregosa11a.htmlMathSciNetzbMATHGoogle Scholar
  38. 38.
    Sturm, T.: New domains for applied quantifier elimination. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2006. LNCS, vol. 4194, pp. 295–301. Springer, Heidelberg (2006).  https://doi.org/10.1007/11870814_25CrossRefGoogle Scholar
  39. 39.
    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, p. 14. CEUR-WS (2007). http://ceur-ws.org/Vol-257/
  40. 40.
    Wilson, D., Davenport, J., England, M., Bradford, R.: A “piano movers” problem reformulated. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, pp. 53–60. IEEE (2013). http://dx.doi.org/10.1109/SYNASC.2013.14
  41. 41.
    Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565–606 (2008).  https://doi.org/10.1613/jair.2490CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Faculty of Engineering, Environment and ComputingCoventry UniversityCoventryUK

Personalised recommendations