This paper discusses and evaluates ideas of data balancing and data augmentation in the context of mathematical objects: an important topic for both the symbolic computation and satisfiability checking communities, when they are making use of machine learning techniques to optimise their tools. We consider a dataset of non-linear polynomial problems and the problem of selecting a variable ordering for cylindrical algebraic decomposition to tackle these with. By swapping the variable names in already labelled problems, we generate new problem instances that do not require any further labelling when viewing the selection as a classification problem. We find this augmentation increases the accuracy of ML models by 63% on average. We study what part of this improvement is due to the balancing of the dataset and what is achieved thanks to further increasing the size of the dataset, concluding that both have a very significant efect. We finish the paper by reflecting on how this idea could be applied in other uses of machine learning in mathematics.
changes the meaning only if the quantifiers are diferent. These choices of variable ordering may
not afect the correctness of the end result but they can have a huge impact on the resources
required by these algorithms. In fact, Brown and Davenport found in [
Since the community realised the importance of variable ordering, various human-made
heuristics have been developed for the choice, e.g. [
This paper proposes to balance and augment the existing datasets by exploiting the arbitrary
nature of the variable representations within (the variable names). We note that this idea has
been independently proposed recently in the preprint [
Data augmentation consists of generating new data instances from existing ones. It is a widelyused technique in ML more generally, where the ability to increase the dataset can help tackle over-fitting, and increase the accuracy of the resulting model. Moreover, it can be used to mitigate the biases in the dataset and to reduce the cost of labelling [19].
Data augmentation is commonly used to generate new images in Computer Vision ML applications. Let us take these ideas used in computer vision as an analogy for generating new mathematical objects. For example, it is clear to any human that a picture of an arrow pointing to the right that is rotated 90 degrees clockwise results gives a picture of an arrow pointing downwards. This can be very useful, imagine that your dataset contains 268 images: 4 images of arrows pointing downwards, 35 pointing left, 56 pointing upwards, and 173 pointing to the right. This dataset is very unbalanced, and any model trained on it would likely have a bias towards predicting that the arrow points to the right and against predicting that the arrow points downwards. However, by simply using image rotations the dataset can be balanced to contain 67 images for each of the classes. Furthermore, since you can obtain three extra images from each of the images in the original dataset, we could actually obtain an augmented dataset of 1072 images with 268 of each class.
Returning to our mathematical context, our objects are sets of polynomials (possibly used to form polynomial constraints). For example, {21 − 2, 33 − 1}. We can determine, by computing and comparing CADs, that the optimal variable ordering to compute a CAD for this set is 2 ≻ 1 ≻ 3. Now observe that simply by swapping the names of the variables 1 and 2 we may obtain the new set of polynomials {22 − 1, 33 − 1}, in which we know, without any further CAD computation, that the optimal variable ordering is 1 ≻ 2 ≻ 3.
In this paper, we will use data augmentation to balance our initially unbalanced polynomial
dataset, obtaining an improvement in the accuracy of the models. Then, we will see how much
more accuracy will be improved by generating the maximum number of instances possible
with the data augmentation tools we have. Section 2 outlines our methodology in creating a
labelled dataset to use for ML to select a CAD variable ordering and Section 3 how we have
balanced and augmented that dataset. Then in Section 4, we compare the performance of ML
models trained and tested on these various datasets. We finish in Section 5 with conclusions, a
comparison with some similar work in the preprint [
The dataset and code used to generate the datasets and results described in this paper can be found on GitHub here:
There are three steps towards creating a dataset suitable for ML in our context: finding a collection of sets of meaningful polynomials, choosing a methodology to represent each of these sets to an ML model, and then a system for labelling them (identifying the best CAD ordering). We describe each of these steps in the following subsections.
The collection of sets of polynomials we use will be those problems in the QF_NRA collection of the SMT-LIB library [20] which involve three variables. These examples are all satisfiability problems and thus do not represent the full application range of CAD which can also address quantifier elimination. However, there are no sizeable datasets of QE problems we are aware of. The problems in the SMT-LIB do mostly emit from real applications making performance upon them meaningful. Common sources are problems include the theorem prover MetiTarski [21], attempts to prove termination of term-rewrite systems, verification conditions from Keymaera [22], and curated sets of problems from geometry [23], economics [24] and biology [25].
Representing sets of polynomials for ML is not an easy task. First, their size can vary: we have already chosen to fix the number of variables but there could then still be an arbitrary number of polynomials, and each of these polynomials can have a great many diferent terms (although in practice each has not very many).
To represent a set of polynomials we will follow the methodology of [
Ordering 0 Ordering 1 Ordering 2 Ordering 3 Ordering 4 Ordering 5
Ordering 1 ≻ 2 ≻ 3 1 ≻ 3 ≻ 2 2 ≻ 1 ≻ 3 2 ≻ 3 ≻ 1 3 ≻ 1 ≻ 2 3 ≻ 2 ≻ 1
As well as sum and average, the framework we use can apply the operations of maximum,
sum, average, and average of non-zero terms. We also have the possibility of taking the sign
at any point. Another example feature is the sum across the polynomials of the sign of the
sum of the degree of 2 across the monomials (which simplifies the number of polynomials
that contain the variable 2). For the previous set of polynomials, this feature is 1, because the
sum of the degree of 1 is 3 in the first polynomial and 0 in the second. Moreover, the degree
of the variable can be substituted by , the total degree of the monomial if the monomial
includes such a variable (it is 0 otherwise). E.g. 1 is 4 for the monomial 1223 and 0 for the
monomial 323 because 1 does not appear in the latter. See [
Applying this process results in 384 features to describe a set of polynomials in three variables, of which 195 are essentially distinct (not in a linear relationship with any other feature in our dataset). We thus use these 195 features to represent a set of polynomials in 3 variables.
In the case of sets of polynomials of three variables, there are six possible variable orderings. A CAD has been computed in Maple [26] for each ordering for every problem in our dataset, and we timed how long this took, discarding any example in which all orderings timed out (took more than 60 seconds). The label of the set of polynomials is the number associated with the ordering, as given in Table 1, whose CAD required the lowest computation time. Thus we form a labelled dataset for an ML classification problem.
The dataset described in the previous section has 1019 instances: 406 labelled 0, 93 labelled 1, 135 labelled 2, 51 labelled 3, 202 labelled 4 and 132 labelled 5. There is hence a clear imbalance in this dataset that will likely result in a bias in models trained upon it.
We split this dataset into an original testing dataset containing 20% of the instances (815) and an original training dataset containing the rest.
We first randomly changed the label of each instance permuting the variable names in the underlying polynomials. This is done in both of the original datasets (training and testing), obtaining a balanced training dataset and a balanced testing dataset of the same sizes as the original training and testing sets.
However, nothing is stopping us from adding all of the six possible re-orderings for each problem to the dataset: each would have a diferent label which we know without any further labelling. By adding all the possibilities we obtain a perfectly balanced dataset with six times more data than the original one. The sizes of all these datasets are shown in Table 2.
Dataset train unbalanced dataset train balanced dataset train augmented dataset test unbalanced dataset test balanced dataset test augmented dataset
KNN-Unbalanced DT-Unbalanced SVC-Unbalanced RF-Unbalanced MLP-Unbalanced
Comparing Tables 4 and 5 one observes that fully augmenting the dataset is superior to just balancing it for all models on any of our datasets.
Finally, comparing Tables 3 and 5 it is possible to observe that when testing on unbalanced data the improvement in performance obtained by augmenting the dataset is similar in scale to that gained by training dataset on a dataset that has the same imbalance as the testing data: three of the five models perform better on the unbalanced dataset when trained with augmented data and the other two come close. When comparing performance on a balanced testing dataset is balanced, the improvement from using balanced data or augmented data for training is significant: an increase in 63% of accuracy on average.
Our first conclusion is that, for this problem, training on an unbalanced dataset does indeed lead to overfitting and poor performance when the models are utilised on a balanced dataset. The performance in the Unbalanced column in Table 4) is much worse than previous reports on such ML models, e.g. [28], and demonstrates the importance of taking note and care of these balance issues. In general, imbalance is not always inappropriate for ML: some applications will naturally have imbalanced data and the ML models should be aware of this. However, in our case, we seek heuristics for choosing variable orderings for CAD applied in general and there is little rationale to suppose general CAD applications favour one ordering over another1. Thus our advice is to ensure ML models for such applications are trained on balanced data.
Our second conclusion is that a good deal of the ML performance can be recovered by simply training on balanced data, re-validating the value of the data-science-led approach to this task that those original papers posited.
Our third conclusion is that it is beneficial to go further and use maximum data augmentation: all models benefitted from this over just balancing the data no matter which dataset they are tested on. Using a balanced dataset instead of an unbalanced one of the same size allowed the accuracy of the models to improve on average by 27%. But using a dataset fully augmented to thus multiply the size by six allowed the accuracy of the models to improve on average by 63%. In fact, the performance lost from the original unbalanced case is basically recovered this way.
Finally, we note that these ideas should generalise easily to variable ordering choice for the other decision procedures of non-linear real arithmetic commonly found in the wider toolchains of the SC2 community.
Let us now compare the results on this paper with the ones obtained in the recent preprint [
We note that the original dataset in [
This comparison with [
Given the success of this data augmentation, an obvious area for future work is to look for additional augmentation techniques. Returning to the computer vision analogy: rotations 1except perhaps the existence of the SMT-LIB data! are not the only augmentation tool, there are others also e.g. mirror reflections. Regarding mathematical objects, a corresponding augmentation technique may be substituting a variable with its negative, which would create a new instance without the need for any further labelling. We could also consider more involved variable transformations, however, these would most likely require additional CAD computations for data labelling, which is the most expensive part of this whole process.
We note that these ideas of data augmentation could be generalised to other mathematical object datasets. One should reflect on which parts of the representation of a mathematical object are arbitrary to the problem at hand. For example, in [29] the authors consider symbolic integration by ML, with mathematical expressions represented as natural text. The order of the operands in commutative operations is arbitrary (e.g. ∧ 2 + * is the same expression as * + ∧ 2). This could be exploited to generate an exorbitant amount of new instances that do not require any relabelling!
TdR is supported by Coventry University and a travel grant from the London Mathematical Society (LMS). ME is supported by UKRI EPSRC Grant EP/T015748/1, Pushing Back the DoublyExponential Wall of Cylindrical Algebraic Decomposition (the DEWCAD Project). for real quantifier elimination using machine learning, ArXiv Preprint (2023). doi: 10. 48550/ARXIV.2302.14038. [19] C. Shorten, T. M. Khoshgoftaar, A survey on image data augmentation for deep learning,
Journal of Big Data 6 (2019) 60. doi:10.1186/s40537-019-0197-0. [20] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2016. URL: http://smtlib.cs.uiowa.edu/. [21] L. C. Paulson, Metitarski: Past and future, in: L. Beringer, A. Felty (Eds.), Interactive Theorem Proving, volume 7406 of Lecture Notes in Computer Science, Springer, 2012, pp. 1–10. doi:10.1007/978-3-642-32347-8_1. [22] A. Platzer, J. Quesel, P. Rümmer, Real world verification, in: R. A. Schmidt (Ed.), Automated Deduction (CADE-22), volume 5663 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2009, pp. 485–501. doi:10.1007/978-3-642-02959-2_35. [23] C. Brown, Z. K., T. Reico, , R. Vajda, M. Pilar Vélez, Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?, Mathematics in Computer Science 16 (2021) 31. doi:10.1007/s11786-022-00532-9. [24] C. B. Mulligan, J. H. Davenport, M. England, TheoryGuru: A Mathematica package to apply quantifier elimination technology to economics, in: J. H. Davenport, M. Kauers, G. Labahn, J. Urban (Eds.), Mathematical Software – Proc. ICMS 2018, volume 10931 of Lecture Notes in Computer Science, Springer International Publishing, 2018, pp. 369–378. doi:10.1007/978-3-319-96418-8_44. [25] R. Bradford, J. H. Davenport, M. England, H. Errami, V. Gerdt, D. Grigoriev, C. Hoyt, M. Košta, O. Radulescu, T. Sturm, A. Weber, Identifying the parametric occurrence of multiple steady states for some biological networks, Journal of Symbolic Computation 98 (2020) 84–119. doi:10.1016/j.jsc.2019.07.008. [26] C. Chen, M. Moreno Maza, Cylindrical algebraic decomposition in the RegularChains library, in: H. Hong, C. Yap (Eds.), Mathematical Software – ICMS 2014, volume 8592 of Lecture Notes in Computer Science, Springer Heidelberg, 2014, pp. 425–433. doi:10.1007/ 978-3-662-44199-2_65. [27] F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, E. Duchesnay, Scikit-learn: Machine learning in Python, Journal of Machine Learning Research 12 (2011) 2825–2830. URL: http://www.jmlr.org/papers/v12/pedregosa11a.html. [28] M. England, D. Florescu, Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition, in: C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (Eds.), Intelligent Computer Mathematics, volume 11617 of Lecture Notes in Computer Science, Springer International Publishing, 2019, pp. 93–108. doi:10.1007/ 978-3-030-23250-4_7. [29] G. Lample, F. Charton, Deep Learning for Symbolic Mathematics, in: S. Mohamed, M. White, K. Cho, D. Song (Eds.), Eighth International Conference on Learning Representations (ICLR 2020), 2020. URL: https://iclr.cc/virtual_2020/poster_S1eZYeHFDS.html. [30] B. Caviness, J. Johnson, Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation, Springer-Verlag, 1998. doi:10.1007/ 978-3-7091-9459-1.