×

Using machine learning to improve cylindrical algebraic decomposition. (English) Zbl 1474.68464

Summary: Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, best known as a procedure to enable Quantifier Elimination over real-closed fields. However, it has a worst case complexity doubly exponential in the size of the input, which is often encountered in practice. It has been observed that for many problems a change in algorithm settings or problem formulation can cause huge differences in runtime costs, changing problem instances from intractable to easy. A number of heuristics have been developed to help with such choices, but the complicated nature of the geometric relationships involved means these are imperfect and can sometimes make poor choices. We investigate the use of machine learning (specifically support vector machines) to make such choices instead. Machine learning is the process of fitting a computer model to a complex function based on properties learned from measured data. In this paper we apply it in two case studies: the first to select between heuristics for choosing a CAD variable ordering; the second to identify when a CAD problem instance would benefit from Gröbner Basis preconditioning. These appear to be the first such applications of machine learning to Symbolic Computation. We demonstrate in both cases that the machine learned choice outperforms human developed heuristics.

MSC:

68W30 Symbolic computation and algebraic computation
68T05 Learning and adaptive systems in artificial intelligence
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B., Cimatti, A., Davenport, J.H., England, M., Fontaine, P., Forrest, S., Griggio, A., Kroening, D., Seiler, W.M., Sturm, T.: \[{{\sf SC}}^2\] SC2: satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) Intelligent Computer Mathematics: Proceedings CICM 2016, volume 9791 of Lecture Notes in Computer Science, pp. 28-43. Springer (2016) · Zbl 1344.68198
[2] Alpaydin, E.: Introduction to Machine Learning. MIT Press, Cambridge (2004) · Zbl 1191.68485
[3] Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC ’14, pp. 1-8. ACM (2014) · Zbl 1325.68212
[4] Arnon, D.; Collins, GE; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. Comput., 13, 865-877 (1984) · Zbl 0562.14001
[5] Baldi, P.; Brunak, S.; Chauvin, Y.; Andersen, CAF; Nielsen, H., Assessing the accuracy of prediction algorithms for classification: an overview, Bioinformatics, 16, 412-424 (2000)
[6] Basu, S., Pollack, R., Roy, M.E.: Algorithms in Real Algebraic Geometry. Volume 10 of Algorithms and Computations in Mathematics. Springer, Berlin (2006) · Zbl 1102.14041
[7] Böge, W.; Gebauer, R.; Kredel, H.; Caviness, BF (ed.), Gröbner bases using SAC2, 272-274 (1985), Berlin
[8] Boser, B.E., Guyon, I.M., Vapnik, V.N.: A training algorithm for optimal margin classifiers. In: Proceedings of the Fifth Annual Workshop on Computational Learning Theory, COLT ’92, pp. 144-152. ACM (1992)
[9] Boyan, J., Freitag, D., Joachims, T.: A machine learning architecture for optimizing web search engines. In: AAAI Workshop on Internet Based Information Systems, pp. 1-8 (1996)
[10] Bradford, R.; Chen, C.; Davenport, JH; England, M.; Moreno Maza, M.; Wilson, D.; Gerdt, VP (ed.); Koepf, W. (ed.); Seiler, WM (ed.); Vorozhtsov, EV (ed.), Truth table invariant cylindrical algebraic decomposition by regular chains, 44-58 (2014), Berlin
[11] Bradford, R., Davenport, J.H., 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 the 2017 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’17, pp. 45-52. ACM (2017) · Zbl 1444.92034
[12] Bradford, R., Davenport, J.H., 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 ’13, pp. 125-132. ACM (2013) · Zbl 1359.68327
[13] Bradford, R.; Davenport, JH; England, M.; McCallum, S.; Wilson, D., Truth table invariant cylindrical algebraic decomposition, J. Symb. Comput., 76, 1-35 (2016) · Zbl 1351.68314
[14] Bradford, R.; Davenport, JH; England, M.; Wilson, D.; Carette, J. (ed.); Aspinall, D. (ed.); Lange, C. (ed.); Sojka, P. (ed.); Windsteiger, W. (ed.), Optimising problem formulations for cylindrical algebraic decomposition, 19-34 (2013), Berlin
[15] Bridge, J.P.: Machine learning and automated theorem proving. Technical Report UCAM-CL-TR-792, University of Cambridge, Computer Laboratory (2010)
[16] Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reason. 1-32 (2014) · Zbl 1314.68274
[17] Brown, CW, Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 447-465 (2001) · Zbl 0981.68186
[18] Brown, CW, QEPCAD B: a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bull., 37, 97-108 (2003) · Zbl 1083.68148
[19] Brown, C.W.: Companion to the tutorial: cylindrical algebraic decomposition. Presented at ISSAC ’04 (2004). http://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf
[20] Brown, C.W.: Open non-uniform cylindrical algebraic decompositions. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15, pp. 85-92. ACM (2015) · Zbl 1346.68273
[21] Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC ’07, pp. 54-60. ACM (2007) · Zbl 1190.68028
[22] Brown, CW; Kahoui, M.; Novotni, D.; Weber, A., Algorithmic methods for investigating equilibria in epidemic modelling, J. Symb. Comput., 41, 1157-1173 (2006) · Zbl 1120.92034
[23] Brown, CW; Kosta, M., Constructing a single cell in cylindrical algebraic decomposition, J. Symb. Comput., 70, 14-48 (2015) · Zbl 1314.68414
[24] Buchberger, B., Bruno Buchberger’s Ph.D. thesis (1965): an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, J. Symb. Comput., 41, 475-511 (2006) · Zbl 1158.01307
[25] Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gröbner bases. Technical report, 91-06. RISC, Johannes Kepler University (1991)
[26] Byun, H.; Lee, S., A survey on pattern recognition applications of support vector machines, Int. J. Pattern Recognit. Artif. Intell., 17, 459-486 (2003)
[27] Carette, J.: Understanding expression simplification. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC ’04, pp. 72-79. ACM (2004) · Zbl 1134.68596
[28] Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Berlin (1998)
[29] Charalampakis, AE; Chatzigiannelis, I., Analytical solutions for the minimum weight design of trusses by cylindrical algebraic decomposition, Arch. Appl. Mech., 88, 39-49 (2018)
[30] Chen, C.; Moreno Maza, M.; Feng, R. (ed.); Lee, W. (ed.); Sato, Y. (ed.), An incremental algorithm for computing cylindrical algebraic decompositions, 199-221 (2014), Berlin · Zbl 1352.68291
[31] Chen, C.; Moreno Maza, M.; Hong, H. (ed.); Yap, C. (ed.), Real quantifier elimination in the RegularChains library, 283-290 (2014), Heidelberg · Zbl 1437.14006
[32] Chen, C.; Moreno Maza, M., Quantifier elimination by cylindrical algebraic decomposition based on regular chains, Journal of Symbolic Computation, 75, 74-93 (2016) · Zbl 1398.68695
[33] 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 ’09, pp. 95-102. ACM (2009) · Zbl 1237.14068
[34] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pp. 134-183. Springer (reprinted in the collection [28]) (1975)
[35] Collins, GE; Caviness, BF (ed.), The SAC-2 computer algebra system, 34-35 (1985), Berlin
[36] Collins, GE; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 299-328 (1991) · Zbl 0754.68063
[37] Cortes, C.; Vapnik, V., Support-vector networks, Mach. Learn., 20, 273-297 (1995) · Zbl 0831.68098
[38] Davenport, J.H., 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 ’12, pp. 83-88. IEEE (2012)
[39] Davenport, JH; England, M.; Greuel, GM (ed.); Koch, T. (ed.); Paule, P. (ed.); Sommese, A. (ed.), Need polynomial systems be doubly exponential?, 157-164 (2016), Berlin
[40] Davenport, JH; Heintz, J., Real quantifier elimination is doubly exponential, J. Symb. Comput., 5, 29-35 (1988) · Zbl 0663.03015
[41] Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC ’04, pp. 111-118. ACM (2004) · Zbl 1134.68575
[42] England, M.; Davenport, JH (ed.); Kauers, M. (ed.); Labahn, G. (ed.); Urban, J. (ed.), Machine Learning for Mathematical Software, 165-174 (2018), Heidelberg
[43] England, M.; Bradford, R.; Chen, C.; Davenport, JH; Moreno Maza, M.; Wilson, D.; Watt, SM (ed.); Davenport, JH (ed.); Sexton, AP (ed.); Sojka, P. (ed.); Urban, J. (ed.), Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, 45-60 (2014), Berlin
[44] England, M., Bradford, R., Davenport, J.H.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15, pp. 165-172. ACM (2015) · Zbl 1346.68283
[45] England, M.; Bradford, R.; Davenport, JH; Wilson, D.; Carette, J. (ed.); Aspinall, D. (ed.); Lange, C. (ed.); Sojka, P. (ed.); Windsteiger, W. (ed.), Understanding branch cuts of expressions, 136-151 (2013), Berlin
[46] England, M.; Bradford, R.; Davenport, JH; Wilson, D.; Hong, H. (ed.); Yap, C. (ed.), Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, 450-457 (2014), Heidelberg · Zbl 1350.68294
[47] England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Werner, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing: 18th International Workshop, CASC 2016, Volume 9890 of Lecture Notes in Computer Science, pp. 172-192. Springer (2016)
[48] England, M.; Errami, H.; Grigoriev, D.; Radulescu, O.; Sturm, T.; Weber, A.; Gerdt, VP (ed.); Koepf, W. (ed.); Seiler, WM (ed.); Vorozhtsov, EV (ed.), Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks, 93-108 (2017), Berlin · Zbl 1455.92058
[49] England, M.; Wilson, D.; Bradford, R.; Davenport, JH; Hong, H. (ed.); Yap, C. (ed.), Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting, 458-465 (2014), Berlin · Zbl 1437.14008
[50] 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) · Zbl 1335.68300
[51] Errami, H.; Eiswirth, M.; Grigoriev, D.; Seiler, WM; Sturm, T.; Weber, A., Detection of Hopf bifurcations in chemical reaction networks using convex coordinates, J. Comput. Phys., 291, 279-302 (2015) · Zbl 1349.92168
[52] Faugère, J.C.: A new efficient algorithm for computing Gröbner bases without reduction to zero (F5). In: Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, ISSAC ’02, pp. 75-83. ACM (2002) · Zbl 1072.68664
[53] Fayyad, U.M., Irani, K.B.: Multi-interval discretization of continuous-valued attributes for classification learning. In: Proceedings of the International Joint Conference on Uncertainty in AI, pp. 1022-1027. http://trs-new.jpl.nasa.gov/dspace/handle/2014/35171 (1993)
[54] Forsyth, R., Rada, R.: Machine Learning: Applications in Expert Systems and Information Retrieval. Halsted Press, New York (1986)
[55] Graebe, H.G., Nareike, A., Johanning, S.: The SymbolicData project: towards a computer algebra social network. In: England, M., Davenport, J.H., Kohlhase, A., Kohlhase, M., Libbrecht, P., Neuper, W., Quaresma, P., Sexton, A.P., Sojka, P., Urban, J., Watt, S.M. (eds.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress Track at CICM, Number 1186 in CEUR Workshop Proceedings (2014)
[56] Guyon, I.; Elisseeff, A., An introduction to variable and feature selection, J. Mach. Learn. Res., 3, 1157-1182 (2003) · Zbl 1102.68556
[57] Hall, M.; Frank, E.; Holmes, G.; Pfahringer, B.; Reutemann, P.; Witten, IH, The WEKA data mining software: an update, SIGKDD Explor. Newsl., 11, 10-18 (2009)
[58] Hall, M.A.: Correlation-based feature selection for discrete and numeric class machine learning. In: Proceedings of the Seventeenth International Conference on Machine Learning, ICML ’00, pp. 359-366. Morgan Kaufmann Publishers Inc. (2000)
[59] Hall, MA; Holmes, G., Benchmarking attribute selection techniques for discrete class data mining, IEEE Trans. Knowl. Data Eng., 15, 1437-1447 (2003)
[60] Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in CAD projection. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC ’14, pp. 240-247. ACM (2014) · Zbl 1325.68286
[61] Heinle, A.; Levandovskyy, V., The SDEval benchmarking toolkit, ACM Commun. Comput. Algebra, 49, 1-9 (2015) · Zbl 1365.68493
[62] Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC ’90, pp. 261-264. ACM (1990)
[63] Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Technical report, RISC, Linz (1991)
[64] Hornik, K.; Stinchcombe, M.; White, H., Multilayer feedforward networks are universal approximators, Neural Netw., 2, 359-366 (1989) · Zbl 1383.92015
[65] Hsu, C., Chang, C., Lin, C.: A practical guide to support vector classification. Technical report, Department of Computer Science, National Taiwan University (2003)
[66] Huang, Z., England, M., Davenport, J.H., 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 ’16), pp. 45-52. IEEE (2016)
[67] Huang, Z.; England, M.; Wilson, D.; Davenport, JH; Paulson, L.; Bridge, J.; Watt, SM (ed.); Davenport, JH (ed.); Sexton, AP (ed.); Sojka, P. (ed.); Urban, J. (ed.), Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition, 92-107 (2014), Berlin
[68] Huang, Z., Paulson, L.: An application of machine learning to RCF decision procedures. In: 20th Automated Reasoning Workshop, University of Dundee, UK, ARW ’13 (2013)
[69] 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 ’09, pp. 55-64 (2009) · Zbl 1356.68282
[70] Joachims, T.; Schölkopf, B. (ed.); Burges, CJC (ed.); Smola, AJ (ed.), Making large-scale support vector machine learning practical, 169-184 (1999), Cambridge
[71] Joachims, T.: A support vector method for multivariate performance measures. In: Proceedings of the 22nd International Conference on Machine Learning, ICML ’05, pp. 377-384. ACM (2005)
[72] Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning: 6th International Joint Conference (IJCAR), Volume 7364 of Lecture Notes in Computer Science, pp. 339-354. Springer (2012) · Zbl 1358.68257
[73] Kobayashi, M.; Iwane, H.; Matsuzaki, T.; Anai, H.; Kotsireas, SI (ed.); Rump, MS (ed.); Yap, KC (ed.), Efficient subformula orders for real quantifier elimination of non-prenex formulas, 236-251 (2016), Berlin · Zbl 1460.68086
[74] Matthews, BW, Comparison of the predicted and observed secondary structure of T4 phage lysozyme, Biochim. Biophys. Acta (BBA) Protein Struct., 405, 442-451 (1975)
[75] Mayr, EW; Meyer, AR, The complexity of the word problems for commutative semigroups and polynomial ideals, Adv. Math., 46, 305-329 (1982) · Zbl 0506.03007
[76] McCallum, S.; Caviness, B. (ed.); Johnson, J. (ed.), An improved projection operation for cylindrical algebraic decomposition, 242-268 (1998), Berlin · Zbl 0900.68279
[77] McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC ’99, pp. 145-149. ACM (1999)
[78] McCallum, S.; Hong, H., On using Lazard’s projection in CAD construction, J. Symb. Comput., 72, 65-81 (2016) · Zbl 1325.13026
[79] McCulloch, WS; Pitts, W., A logical calculus of the ideas immanent in nervous activity, Bull. Math. Biophys., 5, 115-133 (1943) · Zbl 0063.03860
[80] Mulligan, C.B.: Automated economic reasoning with quantifier elimination. Working Paper 22922, National Bureau of Economic Research (2016)
[81] Patel, BR; Kaushik, KR, A survey on decision tree algorithm for classification, Int. J. Eng. Dev. Res., 2, 1-5 (2014)
[82] Paulson, LC; Beringer, L. (ed.); Felty, A. (ed.), Metitarski: past and future, 1-10 (2012), Berlin · Zbl 1360.68765
[83] Platzer, A.; Quesel, JD; Armando, A. (ed.); Baumgartner, P. (ed.); Dowek, G. (ed.), KeYmaera: a hybrid theorem prover for hybrid systems (system description), 171-178 (2008), Berlin · Zbl 1165.68469
[84] Platzer, A.; Quesel, JD; Rümmer, P.; Schmidt, RA (ed.), Real world verification, 485-501 (2009), Berlin · Zbl 1250.68197
[85] Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes in C (2nd Ed.): The Art of Scientific Computing. Cambridge University Press, Cambridge (1992) · Zbl 0845.65001
[86] Quinlan, JR, Induction of decision trees, Mach. Learn., 1, 81-106 (1986)
[87] Rosenblatt, F., The perceptron: a probabilistic model for information storage and organization in the brain, Psychol. Rev., 65, 386 (1958)
[88] Schölkopf, B., Tsuda, K., Vert, J.-P.: Kernel methods in computational biology. MIT Press, Cambridge (2004)
[89] Sebastiani, F., Machine learning in automated text categorization, ACM Comput. Surv., 34, 1-47 (2002)
[90] Shannon, Claude E., A mathematical theory of communication, Mob. Comput. Commun. Rev., 5, 3-55 (2001)
[91] Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004) · Zbl 0994.68074
[92] Stone, P.; Veloso, M., Multiagent systems: a survey from a machine learning perspective, Auton. Robot., 8, 345-383 (2000)
[93] Strzeboński, A., Cylindrical algebraic decomposition using validated numerics, J. Symb. Comput., 41, 1021-1038 (2006) · Zbl 1124.68123
[94] Strzeboński, A., Cylindrical algebraic decomposition using local projections, J. Symb. Comput., 76, 36-64 (2016) · Zbl 1350.14042
[95] Tarski, A.: A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA (reprinted in the collection [28]) (1948) · Zbl 0035.00602
[96] Vapnik, VN; Chervonenkis, AY, A note on one class of perceptrons, Autom. Remote Control, 25, 821-837 (1964) · Zbl 0173.19103
[97] Wilson, D.; Bradford, R.; Davenport, JH; England, M., Cylindrical algebraic sub-decompositions, Math. Comput. Sci., 8, 263-288 (2014) · Zbl 1309.68232
[98] Wilson, D., Davenport, J.H., England, M., Bradford, R.: A “piano movers” problem reformulated. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’13, pp. 53-60. IEEE (2013)
[99] Wilson, D., England, M., Davenport, J.H., 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 ’14, pp. 53-60. IEEE (2014)
[100] Wilson, DJ; Bradford, RJ; Davenport, JH, A repository for CAD examples, ACM Commun. Comput. Algebra, 46, 67-69 (2012) · Zbl 1322.68294
[101] Wilson, DJ; Bradford, RJ; Davenport, JH; Jeuring, J. (ed.); Campbell, JA (ed.); Carette, J. (ed.); Reis, G. (ed.); Sojka, P. (ed.); Wenzel, M. (ed.); Sorge, V. (ed.), Speeding up cylindrical algebraic decomposition by Gröbner bases, 280-294 (2012), Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.