nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition

verfasst von : Matthew England, Dorian Florescu

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

There has been recent interest in the use of machine learning (ML) approaches within mathematical software to make choices that impact on the computing performance without affecting the mathematical correctness of the result. We address the problem of selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm in Symbolic Computation. Prior work to apply ML on this problem implemented a Support Vector Machine (SVM) to select between three existing human-made heuristics, which did better than anyone heuristic alone. Here we extend this result by training ML models to select the variable ordering directly, and by trying out a wider variety of ML techniques.

We experimented with the NLSAT dataset and the Regular Chains Library CAD function for Maple 2018. For each problem, the variable ordering leading to the shortest computing time was selected as the target class for ML. Features were generated from the polynomial input and used to train the following ML models: k-nearest neighbours (KNN) classifier, multi-layer perceptron (MLP), decision tree (DT) and SVM, as implemented in the Python scikit-learn package. We also compared these with the two leading human-made heuristics for the problem: the Brown heuristic and sotd. On this dataset all of the ML approaches outperformed the human-made heuristics, some by a large margin.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Variadic Equational Matching

Nächstes Kapitel Towards Specifying Symbolic Computation

E.g. the PoSSo and FRISCO projects in the 90s and the SymbolicData Project [32].

However, as discussed by [1] a more custom approach is beneficial.

http://cs.nyu.edu/~dejan/nonlinear/.

https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf.

Ábrahám, E., et al.: \({\sf SC^ 2}\): satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 28–43. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_3CrossRef

Alemi, A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: DeepMath-deep sequence models for premise selection. In: Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS 2016, pp. 2243–2251, Curran Associates Inc. (2016). https://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection.pdf

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/0213054MathSciNetCrossRefMATH

Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Chap. 26, vol. 185 pp. 825–885. IOS Press (2009)

Bishop, C.: Pattern Recognition and Machine Learning. Springer, New York (2006)MATH

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_4CrossRef

Bradford, R., et al.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2017, pp. 45–52. ACM (2017). https://doi.org/10.1145/3087604.3087622

Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for Boolean combinations. In: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013, pp. 125–132. ACM (2013). https://doi.org/10.1145/2465506.2465516

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.002MathSciNetCrossRefMATH

10.

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_2CrossRef

11.

Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reason. 53, 141–172 (2014). 10.1007/s10817-014-9301-5CrossRef

12.

Brown, C.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447–465 (2001). https://doi.org/10.1006/jsco.2001.0463MathSciNetCrossRefMATH

13.

Brown, C.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003). https://doi.org/10.1145/968708.968710CrossRefMATH

14.

Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 32nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54–60. ACM (2007). https://doi.org/10.1145/1277548.1277557

15.

Brown, C., Kosta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput. 70, 14–48 (2015). https://doi.org/10.1016/j.jsc.2014.09.024MathSciNetCrossRefMATH

16.

Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR. Springer, Vienna (1998). https://doi.org/10.1007/978-3-7091-9459-1CrossRefMATH

17.

Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W., Sato, Y. (eds.) Computer Mathematics. LNCS (LNAI), pp. 199–221. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43799-5_17CrossRef

18.

Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the 34th International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pp. 95–102. ACM (2009). https://doi.org/10.1145/1576702.1576718

19.

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_17CrossRef

20.

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-6MathSciNetCrossRefMATH

21.

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

22.

Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1–2), 29–35 (1988). https://doi.org/10.1016/S0747-7171(88)80004-XMathSciNetCrossRefMATH

23.

Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 29th International Symposium on Symbolic and Algebraic Computation, ISSAC 2004, pp. 111–118. ACM (2004). https://doi.org/10.1145/1005285.1005303

24.

Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. SIGSAM Bull. 31(2), 2–9 (1997). https://doi.org/10.1145/261320.261324CrossRef

25.

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_20CrossRefMATH

26.

England, M., Bradford, R., Chen, C., Davenport, J.H., Maza, M.M., Wilson, D.: 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_5CrossRef

27.

England, M., Bradford, R., Davenport, J.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation, ISSAC 2015, pp. 165–172. ACM (2015). https://doi.org/10.1145/2755996.2756678

28.

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_68CrossRef

29.

England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2017. LNCS, vol. 10490, pp. 93–108. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66320-3_8CrossRef

30.

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_69CrossRef

31.

Erascu, M., Hong, H.: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation). J. Symb. Comput. 75, 110–126 (2016). https://doi.org/10.1016/j.jsc.2015.11.010MathSciNetCrossRefMATH

32.

Graebe, H., Nareike, A., Johanning, S.: The SymbolicData project: towards a computer algebra social network. In: England, M., et al. (eds.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM. CEUR Workshop Proceedings, vol. 1186 (2014). http://ceur-ws.org/Vol-1186/#paper-21

33.

Heinle, A., Levandovskyy, V.: The SDEval benchmarking toolkit. ACM Commun. Comput. Algebra 49(1), 1–9 (2015). https://doi.org/10.1145/2768577.2768578MathSciNetCrossRefMATH

34.

Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the 15th International Symposium on Symbolic and Algebraic Computation, ISSAC 1990, pp. 261–264. ACM (1990), https://doi.org/10.1145/96877.96943

35.

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

36.

Huang, Z., England, M., Wilson, D., Bridge, J., Davenport, J.H., Paulson, L.: Using machine learning to improve cylindrical algebraic decomposition. Math. Comput. Sci. (2019). https://doi.org/10.1007/s11786-019-00394-8

37.

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_8CrossRef

38.

Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proceedings of the 2009 Conference on Symbolic Numeric Computation, SNC 2009, pp. 55–64 (2009). https://doi.org/10.1145/1577190.1577203

39.

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_27CrossRef

40.

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_21CrossRefMATH

41.

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_6CrossRef

42.

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_8CrossRefMATH

43.

McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR, pp. 242–268. Springer, Vienna (1998). https://doi.org/10.1007/978-3-7091-9459-1_12CrossRefMATH

44.

McCallum, S., Parusińiski, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. J. Symb. Comput. 92, 52–69 (2019). https://doi.org/10.1016/j.jsc.2017.12.002MathSciNetCrossRef

45.

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 (\({{\sf SC}}^2\) 2018). CEUR Workshop Proceedings, vol. 2189, pp. 48–60 (2018). http://ceur-ws.org/Vol-2189/

46.

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_44CrossRef

47.

Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_1CrossRef

48.

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.htmlMathSciNetMATH

49.

Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_35CrossRef

50.

Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021–1038 (2006). https://doi.org/10.1016/j.jsc.2006.06.004MathSciNetCrossRefMATH

51.

Strzeboński, A.: Cylindrical algebraic decomposition using local projections. J. Symb. Comput. 76, 36–64 (2016). https://doi.org/10.1016/j.jsc.2015.11.018MathSciNetCrossRefMATH

52.

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_25CrossRef

53.

Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, CA (reprinted in the collection [16]) (1948)

54.

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 (2007). http://ceur-ws.org/Vol-257/

55.

Wilson, D., Bradford, R., Davenport, J., England, M.: Cylindrical algebraic subdecompositions. Math. Comput. Sci. 8, 263–288 (2014). https://doi.org/10.1007/s11786-014-0191-zMathSciNetCrossRefMATH

56.

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). https://doi.org/10.1109/SYNASC.2013.14

57.

Wilson, D., England, M., Davenport, J., Bradford, R.: Using the distribution of cells by dimension in a cylindrical algebraic decomposition. In: 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, pp. 53–60. IEEE (2014). https://doi.org/10.1109/SYNASC.2014.15

58.

Wilson, D., Bradford, R., Davenport, J.: A repository for CAD examples. ACM Commun. Comput. Algebra 46(3), 67–69 (2012). https://doi.org/10.1145/2429135.2429137CrossRefMATH

59.

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.2490CrossRefMATH

Titel: Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition
verfasst von: Matthew England
Dorian Florescu
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-030-23249-8

Electronic ISBN: 978-3-030-23250-4

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-23250-4_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"