# Lessons on Datasets and Paradigms in Machine Learning for Symbolic
Computation: A Case Study on CAD

Tereso del Río  Coventry University, UK<EMAIL_ADDRESS>Matthew
England  Coventry University, UK<EMAIL_ADDRESS>
(Date: January 19, 2024)

###### Abstract.

Symbolic Computation algorithms and their implementation in computer algebra
systems often contain choices which do not affect the correctness of the
output but can significantly impact the resources required: such choices can
benefit from having them made separately for each problem via a machine
learning model. This study reports lessons on such use of machine learning in
symbolic computation, in particular on the importance of analysing datasets
prior to machine learning and on the different machine learning paradigms that
may be utilised. We present results for a particular case study, the selection
of variable ordering for cylindrical algebraic decomposition, but expect that
the lessons learned are applicable to other decisions in symbolic computation.

We utilise an existing dataset of examples derived from applications which was
found to be imbalanced with respect to the variable ordering decision. We
introduce an augmentation technique for polynomial systems problems that
allows us to balance and further augment the dataset, improving the machine
learning results by 28% and 38% on average, respectively. We then demonstrate
how the existing machine learning methodology used for the problem $-$
classification $-$ might be recast into the regression paradigm. While this
does not have a radical change on the performance, it does widen the scope in
which the methodology can be applied to make choices.

###### Key words and phrases:

Symbolic Computation, Machine Learning, Data Augmentation, Classification,
Regression, Cylindrical Algebraic Decomposition

###### 1991 Mathematics Subject Classification:

68W30; 68T05

##  1\. Introduction

Symbolic computation algorithms, including those commonly used within theory
solvers for SMT, often have within them a variety of choices to be made:
choices that do not affect the correctness of the outputs, but can still have
a significant effect upon the resources needed for such algorithms to return
an output and on the form that such outputs take. For example, when running
Buchberger’s algorithm, we may choose any $S$-pair of polynomials from the
list of those to process when computing the next S-polynomial: as long as we
process all pairs in the list eventually, then we obtain a Gröbner basis of
the original polynomials. However, it is well observed that the strategy
utilised to make such choices can significantly impact the cost of running the
algorithm, and also how the final output is presented. Historically, these
choices have been made using heuristics developed by experts, such as the
sugar heuristic developed to choose pairs of polynomials in Buchberger’s
algorithm [21]. However, not all choices are well-documented or evaluated
openly in the literature.

There has been a trend in recent years for programmers to train machine
learning models to make these choices. _Machine Learning_ (ML) refers to
statistical techniques that learn rules from data. It has been well documented
that ML has outperformed expert humans in a wide range of fields, driven
forward by growth in computing power, new techniques, and methods, and an
explosion in available training data. It has been suggested that ML can
enhance the effectiveness of symbolic computation algorithms by replacing
human-designed heuristics. This would allow non-expert users of symbolic
computation to optimise algorithms to their application domain, and for
mathematicians to focus on the theory with less distraction from such
implementation details. Further, the emergence of Explainable AI techniques
may allow for ML to provide suggestions and guidance on algorithm development,
even for those who do not wish to incorporate ML into their final software
[33].

We will investigate two aspects of ML methodology, as introduced in the next
two subsections, in the context of choices for symbolic computation. We will
present experimental results for our case study problem of choosing the
variable ordering for cylindrical algebraic decomposition, introduced shortly,
but emphasise that the lessons drawn should be applied more widely.

###  1.1. Machine learning paradigms

Many of these choices in symbolic computation fall naturally into the ML
_classification_ paradigm: where we train the ML model to choose one option
from a set of discrete possibilities. An alternative paradigm is ML
_regression_ : where we train the ML model to estimate a continuous real
numbered variable. These are often presented as distinct approaches for
tackling different types of problem, but this paper notes that either may be
used for optimisation of symbolic computation algorithms. Given our heuristic
choice from a set of distinct possibilities, we identify the optimal one by
the evaluation of some metric, e.g. the time taken for the algorithm to run
with that choice, or the size of the output produced with that choice. This
metric is used to identify the best choice in the classification problem; but
it could also be the variable we seek to estimate in the regression problem,
with the set of estimations for the different possibilities then used
subsequently to make that discrete choice.

This raises the question of which paradigm is better to view such problems.
Regression is certainly a more difficult problem than classification; however,
for our purposes, the learning needs only to be sufficient to _rank_ the
discrete possibilities allowing scope for significant error in the estimations
of the continuous variable without loss of performance in the symbolic
computation. With that in mind, our hypothesis is that regression should be
superior since it exposes more information to the ML model during training.
Given a choice between $n$ discrete possibilities, the classification paradigm
treats each example as a single instance for the model to learn from, while
the regression paradigm treats each example as $n$ different instances for the
model to learn from. The regression paradigm should thus allow the ML model to
obverse more information: not just which choice was the best, but what effect
all of the possible choices have.

###  1.2. Data augmentation

Data augmentation consists of generating new data instances from existing
ones. It is a widely-used technique in ML applications where a larger dataset
can help tackle overfitting and increase the accuracy of the resulting model.
Moreover, it can be used to mitigate biases in the dataset and to reduce the
cost of labelling [35].

Data augmentation is commonly used to generate new images in Computer Vision
ML applications in particular. For example, in a vision classification problem
we can rotate and reflect the image without changing its label. In our work
later, we will demonstrate how these ideas of data augmentation may be used in
the context of choices for symbolic computation through the permutation of the
variables. In our case, the label of these new instances will change but can
be easily identified from the original label: important since the labelling of
data with symbolic computation will often be the most expensive part of
training a ML model to make such choices.

###  1.3. Our case study problem

This paper will focus on the case study of choosing the variable ordering for
Cylindrical Algebraic Decomposition (CAD): an algorithm that decomposes the
$n$-dimensional real space into distinct cells (connected regions of the
space). It is traditionally applied on sets of polynomials to produce cells in
which each of those polynomials is sign-invariant (either positive, negative,
or zero throughout the cell). Such a CAD is a powerful tool for analysing and
understanding the behaviour of polynomial systems, enabling us to solve tasks
such as real quantifier elimination. However, the doubly exponential
complexity of CAD with respect to the number of variables strongly limits its
practical application. The careful study of its optimisation can only add new
applications to its scope.

One particular area in need of optimisation is the variable order. This may be
free or constrained, depending on the intended use of the CAD after it is
created. When free, it has been observed that the choice of variable ordering
can significantly impact both the theoretical complexity of CAD [8] and the
practical tractability of CAD implementations [17]. Much of the experimental
methodology used in this paper is replicated from our prior work on this
topic, with the changes under study being the paradigm used to train the ML
models and the augmenting of the dataset.

###  1.4. Paper outline

Section 2 contains a literature review: we start with previous work on the use
of ML in symbolic computation, then describe the CAD algorithm used as a case
study in this paper and the current state-of-the-art approaches to choose its
variable ordering. Section 3 then covers some common methodology used in all
our experiments.

Section 4 considers the classification paradigm, replicating previous work and
identifying weaknesses that arise from the imbalance of the dataset. We
describe how data augmentation fixes both these issues and improves the
performance of ML models. This contribution was originally presented in a
paper of the SC-Square 2023 workshop [15] which this present article extends.

In Section 5 we move on to reframe this problem in the the regression
paradigm, comparing to classification and in Section 6 we present an
alternative formulation that is more widely applicable. Finally, in Section 7
we share our conclusions obtained with these experiments.

##  2\. Literature Review

ML has been improving multiple fields over the past two decades. In some
safety-critical areas, such as automatic driving and medicine, ML models are
not fully trusted, as they are not 100% accurate and an error could be fatal.
However, they are still used to assist humans, such as when your car applies
lane assist technology, or a doctor’s attention is drawn to particular cases.
Similarly in mathematics, and thus symbolic computation, we usually require
exact answers and so on the surface it may seem unlikely to use ML in computer
algebra systems; except perhaps for drawing human attention to things of
potential interest, as in [14], or where an ML-produced output can be easily
checked for correctness, as in [29]. However, as discussed in the
introduction, symbolic computation algorithms often contain choices that do
not affect correctness but which have a great impact on the resources needed:
such choices may be safely addressed by ML and are the focus of our study. We
start by reviewing the prior literature for examples of this, paying
particular attention to the learning paradigm utilised, before reviewing the
literature for our case study problem.

###  2.1. Machine learning in symbolic computation

####  2.1.1. Traditional classification paradigm

Most of the examples in the literature of ML to optimise symbolic computation
take the form of supervised learning with the classification paradigm.
_Supervised_ ML means that we start with a dataset of labelled instances that
we use to train the ML models. For example, a dataset of images where each
image is labelled as either a cat or a dog is used to train a binary
classifier to make that distinction. It is important that the data structure
has some fixed features across the instances in the dataset, e.g. images of
the same resolution or a representation as a fixed feature vector.

This paradigm was first used for symbolic computation by Huang et al. in 2014
[25]. They trained a support vector machine to choose the variable ordering
for three-variable CAD problems (meaning six possible variable orderings); and
later the same authors used this methodology to decide when to precondition a
CAD input with computation ofa Groebner basis [23], a binary classification.
Florescu and England built on this, experimenting with models [18] and
features [19].

There are further examples of supervised ML classification for computer
algebra away from CAD in the literature. An early example was by Simpson et
al. who used ML classifiers to pick from different algorithms to compute the
resultant [36], substantially improving the runtimes in both Maple and
Mathematica. ML classifiers to select the subalgorithm for a task have proved
powerful in computational logic: where SATZilla was an early example to select
a SAT-solver for a problem [39], and recently MachSMT did this for the far
more diverse world of SMT [34].

Other recent examples of ML classification in computer algebra include the use
of classifiers to predict features of amoebae in algebraic geometry [1], and
the number of real solutions to polynomial systems [3]. However, we draw a
distinction between these and the prior examples since here ML is directly
predicting the output, and thus inaccuracy in the ML predictions does not just
lead to inefficiencies, but to incorrect answers.

####  2.1.2. Modified classification paradigms

Brown and Daves used ML to choose a polynomial ordering for the NuCAD
algorithm in [9]. This required them to be able to choose between an _a
priori_ unspecified number of options: i.e., it is not just that there are
multiple options but that the number of options may differ at each selection
point. Brown tackled this by training a binary classifier to choose between
two polynomials and then having the options compete with each other under this
classifier until one stands as a winner.

The work in the literature that comes closest to our ideas in Section 5 is
that of Florescu and England [20]. They also started from the recognition that
the classification paradigm was not revealing as much information to the ML
models as there was available. They edited the procedure that performs cross-
validation for hyperparameter selection on the classifiers so that the
hyperparameters were selected based, not on classification accuracy of
choices, but on the runtime achieved by those choices. In fact, this improved
performance, motivated our hypothesis. However, after the selection of
hyperparameters was completed, the actual classifiers in [20] were still
trained on accuracy as normal and so this does not represent a full use of the
regression paradigm.

####  2.1.3. Regression and reinforcement learning

There are fewer examples of regression for the optimisation of computer
algebra in the literature. We were particularly motivated by the work of
Peifer et al. which used regression to choose $S$-pairs of polynomials in
Buchberger’s algorithm [32]. Classification could not be used here since the
number of possible $S$-pairs to choose from differed from one problem instance
to another. They instead trained a regressor to predict the number of
polynomial additions that are required after choosing a given pair, in an
iteration of the main loop of Buchberger’s algorithm. In this way, instead of
informing the algorithm about the best option, the algorithm is informed about
how much work the chosen option required.

As well as a move to regression instead of classification, this work also
represents a shift from supervised to unsupervised learning. Peifer et al. did
not measure the number of additional required for every possible $S$-pair in
advance to create a dataset to learn from. Instead, their model made choices,
got scored (the score being the number of additions), and amended its
parameters in each iteration of the algorithm. This approach is usually known
as _reinforcement learning_ 111Another example of reinforcement learning is
[27] which used it to learn the best pivot to use in Gaussian Elimination..

We note that [32] aimed to minimise the cost of each step, in the hope that if
the cheapest decision is taken at each step, then the cost of the overall
algorithm will be small. There is a risk with this approach that it leads to
more $S$-pairs being generated overall, but [32] reported strong performance,
with their reinforcement learning agent outperforming all human designed
$S$-pair selection strategies. This motivates our own hypothesis that
regression can allow for deeper learning than classification. However, unlike
[32], we will not switch to reinforcement learning. We will directly compare
supervised learning with classification and supervised learning with
regression to see what, if any, performance difference there is.

###  2.2. Cylindrical algebraic decomposition

####  2.2.1. Definition

Cylindrical Algebraic Decomposition (CAD) is both a mathematical object and an
algorithm to produce such objects, first proposed by Collins in 1975 [12]. It
takes a set of polynomials $S_{n}\in\mathbb{R}[x_{1},\dots,x_{n}]$ as input,
along with a variable ordering, and then builds a decomposition of
$\mathbb{R}^{n}$ into connected regions called cells that are each sign-
invariant for each of the input polynomials. Further, each cell is semi-
algebraic, meaning that it may be described using polynomial constraints; and
the cells are arranged in cylinders, meaning the projection of any two cells
onto a lower-dimensional space (with respect to the variable ordering) is
either equal or distinct. The latter condition makes membership testing,
projection, and negation easy which all aid the use of CAD for quantifier
elimination; the former condition allows for easy solution formula creation.

####  2.2.2. Algorithm

CAD algorithms usually proceed in two phases: projection and lifting. The
first step of projection takes the set of polynomials $S_{n}$ and returns a
set of polynomials $S_{n-1}$ without the largest variable in the ordering,
$x_{n}$. In the next step of the projection phase, a set of polynomials
without $x_{n-1}$ is created. This phase continues until we reach a set of
univariate polynomials in $x_{1}$.

In the first step of the lifting phase, a CAD sign-invariant for the set of
polynomials $S_{1}$ is built. This may be done by using real root isolation
and forming cells from the roots and intervals inbetween. In the next step,
this first CAD of $\mathbb{R}$ is extended to a CAD of $\mathbb{R}^{2}$ sign-
invariant for the set of polynomials $S_{2}$. This is achieved by taking each
cell $C\in\mathbb{R}$ and choosing a single sample point $s\in C$ that we
substitute into $S_{2}$ to produce univariate polynomials upon which we can
apply real root isolation. We are able to conclude the sign-invariant
decomposition we form for $\mathbb{R}\times s$ as representative for
$\mathbb{R}\times C$, meaning the same split into cells according to roots of
polynomials and the intervals inbetween throughout. The conclusion may be
drawn because the information captured in the projection phase encodes the
places where the behaviour of those roots changes (the notion of
_delineability_). This lifting phase continues until a CAD sign-invariant
decomposition of $\mathbb{R}^{n}$ is built.

####  2.2.3. Complexity

Davenport and Heinz proved that CAD generates a doubly exponential number of
cells ($2^{2^{n}}$) in the worst case with respect to the number of variables
($n$) [13]. Brown and Davenport in [6] have shown that there is a family of
sets of polynomials for which the right choice of variable ordering would
yield a constant complexity and the wrong choice of variable ordering would
result in a doubly exponential complexity. Numerous practical experiments have
also shown the significant effect of the variable ordering choice in practice.
This is the choice that we seek to optimise.

###  2.3. Heuristics for choosing the CAD variable ordering

We use _heuristic_ to refer to a rule we may apply to choose a CAD variable
ordering. Heuristics are not guaranteed to produce an optimal answer, but they
should produce an answer quickly. They are usually based on a simple feature
(metric) or combination of features of the input. Although commonly designed
by humans, we may also think of an ML model as a heuristic (noting that while
ML models may be expensive to train, they are, once trained, quick to make a
prediction on a single instance). In this section, we will present the best
non-ML heuristics that have been found for our problem so far.

####  2.3.1. The Brown heuristic

For many years, a well-known and widely used heuristic is the one of Brown
introduced in his ISSAC 2004 tutorial notes [7]. Denoted Brown, this uses
three simple criteria in turn, breaking ties in previous ones with the
subsequent ones. For a given set of polynomials $S$, it projects first:

  * •

$x_{i}$ s.t. $\max\limits_{p\in S}\left(\max\limits_{monom\in
p}\left(degree_{x_{i}}\left(monom\right)\right)\right)$ is minimal,
(i.e. using the highest degree with which the variable appears in the
polynomials);
breaking ties with,

  * •

$x_{i}$ s.t. $\max\limits_{p\in S}\left(\max\limits_{monom\in
p}\left(totaldegree_{x_{i}}(monom)\right)\right)$ is minimal,
(i.e. using the highest total degree of a monomial in which the variable
appears);
breaking ties with

  * •

$x_{i}$ s.t. $\max\limits_{p\in S}\left(\max\limits_{monom\in
p}\left(sign(degree_{x_{i}}(monom))\right)\right)$ is minimal,
(i.e. using the number of monomials in which the variable appears).

It is not specified in [7] what to do if there is a third tie: our
implementation randomly picks between the tied variables. Furthermore, whether
the entire order of variables is chosen at once or one variable at a time is
also not specified in [7].

####  2.3.2. Other human designed heuristics

There have been other human-designed heuristics since then that used more
expensive algebraic information (see [17], [4], and [38]). However, given our
emphasis on heuristics that give answers quickly and the fact that they do not
produce results much better than Brown [24], we do not consider them further
here.

More recently, the authors of this article proposed the heuristic gmods in
[16], motivated by the complexity analysis of CAD. This heuristic projects
first the variable with the lowest degree in the product of the polynomials.
Again, if there are ties, our implementation picks randomly.

####  2.3.3. Human-level heuristics

The state-of-the-art human-level heuristic in the current literature is T1,
from [33]. We call this _human-level_ because although it was informed by ML
techniques, it can be expressed independently of an ML model in a similar
quantity of text as the human-designed heuristics above. In fact, it uses
three simple features in a chain just like Brown. The features were those
found most impactful after a SHAP analysis to interpret decisions of ML
classifiers trained to choose the best variable ordering [33]. For a given set
of polynomials $S$, this heuristic projects first:

  * •

$x_{i}$ s.t. $\sum\limits_{p\in S}\left(\max\limits_{monom\in
p}\left(degree_{x_{i}}\left(monom\right)\right)\right)$ is minimal,
(i.e. using the degree of the variable in the product of the polynomials);
breaking ties with,

  * •

$x_{i}$ s.t. $\operatorname*{aveg}\limits_{p\in
S}\left(\operatorname*{aveg}\limits_{monom\in
p}\left(degree_{x_{i}}(monom)\right)\right)$ is minimal,
(i.e. using the average of the average degree of the variable in the
polynomials);
breaking ties with

  * •

$x_{i}$ s.t. $\sum\limits_{p\in S}\left(\sum\limits_{monom\in
p}\left(degree_{x_{i}}(monom))\right)\right)$ is minimal,
(i.e. using the sum of all degrees of the variable in the polynomials).

Once again, if there is a third tie our implementation picks randomly.

##  3\. Our Methodology for Machine Learning

In this section, we present the core of the ML methodology we will follow in
all the experiments of the following sections.

###  3.1. Dataset

To train and test supervised ML models, one needs a dataset of labelled
instances to train upon. For our purpose, each instance is a set of
polynomials in three variables, labelled with the best variable ordering for
CAD (the one for which a CAD could be built in the least time). We build this
as follows.

  * •

Acquisition of sets of polynomials: We select the 5942 three-variable problems
from the QF_NRA category of the SMT-LIB [2], and extract the set of
polynomials used from each. We acknowledge that these are all satisfiability
problems and so do not represent the full application range of CAD (e.g. the
more general problem of quantifier elimination). However, they do (mostly)
arise from applications, making performance upon them particularly meaningful.
Most problems are generated by the theorem prover MetiTarski [31], but there
are also examples coming from, e.g., biology [5] and the GeoGebra dynamic
geometry tool [37].

  * •

CAD timings: For each set of polynomials, CylindricalAlgebraicDecomposition
from Maple’s Regular Chains Library [10] was timed to build the CAD for all
six possible variable orderings. A time limit of 30 seconds was used and for
the cases in which no variable ordering finished within the limit, the process
was repeated with a time limit of 60 seconds.

  * •

Removal of over-complicated problems: Problems in which the construction of a
CAD took more than 60 seconds for all six orderings were discarded, leaving
5599 problems.

  * •

Elimination of duplicates: Each problem has associated with it six CADs (one
for each ordering) and thus a vector of six CAD cell counts. When we
identified two problems for whom these vectors were identical then we
discarded one problem. This happened extensively in the dataset where there
are many problems that differ only by a single coefficient, having little
effect on the geometry/topology of the problem. After this step, only 1019
problems were left. We note that this step is the main difference between our
work and [22]: despite the latter using six times more data, they reported
similar performance of the ML models trained. Aside from efficiency, this
should avoid data leakage between testing and training.

###  3.2. Data embedding via features

There are various possible embeddings that ML models can take as input (e.g.
images, text, numbers), but there is no ML model known to the authors that
takes a set of polynomials directly as an input. In line with prior work on ML
for the CAD variable ordering problem, we take a feature-engineering approach,
representing each set of polynomials by a vector of floats defined from simple
to compute metrics on the input such as those used by Brown and T1 above [25,
19, 11].

Florescu and England [19] proposed a semi-automated approach which allowed
them to generate 1728 features for each variable in a given set of polynomials
in three variables. However, many of these features were copies of each other,
and there are 27 per variable which are unique. We will imitate their approach
using different, hopefully more accessible, notation. Let us first introduce
four different ways to convey information about a polynomial with respect to a
variable. We will use the variable $x_{1}$ in the polynomial
$f=2x_{1}^{3}x_{2}+x_{1}^{2}x_{2}x_{3}+2x_{1}^{2}x_{3}^{3}-3x_{1}-x_{2}^{3}x_{3}-4x_{3}^{2}+7$
as an example.

  1. (1)

Extract the degree of the variable of each monomial. E.g.
$I_{1,x_{1}}(f)=[3,2,2,1,0,0,0]$.

  2. (2)

Extract the total degree of each monomial in which the variable appears.
E.g. $I_{2,x_{1}}(f)=[4,4,5,1]$.

  3. (3)

Represent with a 1 for each monomial containing the variable and with a 0 from
each monomial not containing the variable. E.g.
$I_{3,x_{1}}(f)=[1,1,1,1,0,0,0]$.

  4. (4)

Extract the total degree of each monomial in which the variable appears and
add a zero for each monomial in which the variable does not appear. E.g.
$I_{4,x_{1}}(f)=[4,4,5,1,0,0,0]$.

Information relative to a variable in a set of polynomials is then described
with a vector of vectors. For example, using the first option above, the
information relative to the variable $x_{1}$ in the set of polynomials
$S=\\{4x_{1}^{3}x_{3}-x_{2}x_{3}+5x_{3}^{2}-1,f\\}$ is
$I_{1,x_{1}}(S)=[[3,0,0,0],[3,2,2,1,0,0,0]]$.

To condense this vector of vectors down to a single feature, Florescu and
England [19] proposed using the operations of maximum, summation, and average,
taking inspiration again from the features in the human-design heuristic of
Brown [7]. Taking the example in the previous paragraph, an option would be
using summation and then average, to obtain

$avg(sum(I_{1,x_{1}}(S)))=avg([sum([3,0,0,0]),sum([3,2,2,1,0,0,0])])=avg([3,8])=5.5.$

The template that Florescu and England [19] proposed can be simplified to

$\operatorname*{operation}\limits_{p\in\mathcal{T}}\left(\operatorname*{operation}\limits_{M\in
p}\left(\operatorname*{information}(M)\right)\right)$

where $\operatorname*{operation}$ is either a maximum, a sum or an average.

This allowed them to extract nine features per variable and information
extraction. We note that [19] used $I_{1,x_{i}}(S),I_{3,x_{i}}(S)$ and
$I_{4,x_{i}}(S)$ while we use $I_{1,x_{i}}(S),I_{2,x_{i}}(S)$ and
$I_{3,x_{i}}(S)$ (which we found led to better performance). This obtains for
us 27 features for each variable $x_{i}$. The number is reduced to 26 after
$max(max(I_{3,x_{i}}(S)))$ is eliminated (which we do since it evaluated to
$1$ for every instance in our dataset: every variable $x_{i}$ appears in every
set of polynomials $S$ at least once). Then, motivated by Li et al. [30], for
each variable we added another feature, the number of other variables that
appear in the same polynomials as the variable under consideration, bringing
the total back to 27 features per variable.

###  3.3. Dataset preprocessing

To prepare the data for the ML models, it is common to standardise it by
setting the mean of each feature to 0 and the standard deviation to 1.
Standardisation of the data helps avoid biases towards certain features and
improves the accuracy and effectiveness of the model, as explained by [28]. We
use the function  StandardScaler from the library sklearn.preprocessing for
this.

###  3.4. Train/test split

We will divide our dataset into five separate parts, known as “ _folds_ ”. We
will be careful to ensure that problems from the same source (the same
directory of the SMT-LIB) end up in the same fold. This is to prevent “ _data
leakage_ ”: a situation in which a model is tested using the same or similar
data to the data it was trained on. We will choose the hyperparameters and
train models on four of these folds using the strategy being studied; then the
models will be tested on the remaining fold. Repeating this until all folds
have been used for testing, and taking the average to get final results. This
process ensures that our testing is fair and that a model does not benefit
from the test/train split, while still ensuring that the models are evaluated
on data they have not seen during the selection of its hyperparameters or its
training.

###  3.5. Hyperparameter tunning

In ML, “ _hyperparameters_ ” are settings that govern the architecture and
learning process of the model. Hyperparameters are set prior to training, in
contract to model parameters which are optimised during training, e.g. the
number of layers in a neural network or the number of branches in a decision
tree. To find the best hyperparameters, we employ a technique called “
_Bayesian Optimisation_ ” through the function BayesSearchCV in scikit-
optimize. This function is more sophisticated than the more commonly used
GridSearchCV which would evaluate all combinations of values for
hyperparameters taken from discrete sets, and RandomisedSearchCV which
randomly samples from such a grid. BayesSearchCV tries a fixed number of
parameter samples from a specified distributions and intelligently navigates
the hyperparameter space to select these.

Additionally, instead of relying on default metrics like accuracy or mean
squared error, we utilise a custom scoring function. Our custom scorer
evaluates a model based on the time it takes to construct CADs using the
chosen variable ordering, rather than, for example, how often the optimal
variable ordering is chosen. This aligns the evaluation used to choose the
hyperparameters with the specific goals of our research, similarly to [20].

###  3.6. ML models used

During our experiments, we will train a variety of models to ensure that the
conclusions drawn generalise. The models we use are: K-Nearest Neighbours
(KNN), Random Forest (RF), Support Vector Machine (SVM), Multi-Layer
Perceptron (MLP), and Extreme Gradient Boosting (XGB). For the latter we use
the implementation in the xgboost library and for the others the
implementations in the sklearn library.

For training the models, we use the .fit() method in the sklearn library with
default settings, maintaining a standardised process to fairly compare the
changes under scrutiny.

###  3.7. Testing the models

Unless otherwise specified, the dataset that will be used to test the
different strategies will be the balanced dataset described later in Section
4.3 to ensure the fairness of the comparisons.

In this paper, we aim to find a methodology to make good choices in symbolic
computation. In particular, we focus on the case study of choosing good
variable orderings. But what does “ _good_ ” stand for in this context? To
measure the complexity of a CAD we will use the time needed to generate it,
but as it is impossible to obtain a model that guarantees choosing the optimal
ordering every single time we must find ways to compare strategies that may be
better in some instances but worse in others. We make use of the following
metrics.

####  3.7.1. Number of solved instances

The most basic metric is the number of solved instances, i.e. the number of
instances for which the strategy chose a variable ordering that did not
timeout.

####  3.7.2. Time accuracy

Time accuracy is the percentage of instances for which the strategy selects
the fastest variable ordering to build a CAD. Accuracy is very commonly used
to measure the performance of ML models in classification problems. However,
it does not suit our interests very well. Imagine that the best variable
ordering to build a CAD takes 12.43 seconds. If our strategy chooses a
variable ordering that takes 12.47 seconds, that is still pretty good, but the
accuracy measure does not see it that way. It treats this almost-right choice
as completely wrong, the same way it would treat a terrible choice, even if
that choice timed out. This is even worse when we consider that slight
differences in the timings may be the result of computational noise.

####  3.7.3. Total time

Perhaps the metric most aligned with user satisfaction is total time: the time
needed to build a CAD for each instance in the testing dataset, when choosing
the ordering according to the strategy being studied. Unlike accuracy, this
metric treats suboptimal choices based on how suboptimal they are. In the
example of Section 3.7.2, a choice that takes 12.43 seconds will be evaluated
only marginally better than a choice that takes 12.47 seconds.

However, this metric does not fairly reflect performance in instances where
building a CAD took a small amount of time for all orderings. For instance, if
two variable orderings take 1 second and 4 seconds, respectively, to build a
CAD, the impact of this choice is equivalent to the impact of a choice between
a variable ordering that took 31 seconds and one that took 34 seconds.
However, you may argue that selecting an option that costs 4 instead of 1 is a
much worse decision than choosing an option that costs 34 instead of one that
costs 31.

Moreover, this metric is very dataset-dependent, meaning that a total time of
1000 seconds might be a fabulous time for one dataset while being a terrible
time for another dataset. Therefore, it is a poor metric for evaluating a
single sample or a dataset for which the performance of other strategies is
unknown. This implies that it is not the right metric to use in, say,
Reinforcement Learning, where the model should be rewarded or penalised based
on its performance in a group of instances.

####  3.7.4. Time markup

We desire a metric that does not completely penalise suboptimal orderings
while reflecting the effectiveness in fast instances. For this purpose, in
[16], we proposed _time markup_. This metric is the percentage of extra time
needed to build a CAD using the chosen variable ordering measured against the
optimal ordering. Given a chosen suboptimal ordering with time $t_{chosen}$ in
a sample where the optimal ordering time is $t_{optimal}$ the markup is
defined as

$\frac{t_{chosen}-t_{optimal}}{t_{optimal}+1}.$

We add +1 to the denominator to avoid high markups for small differences in
simple problems because these may be caused by computational noise rather than
by the orderings themselves.

####  3.7.5. Metrics based on cell counts

An alternative set of metrics to those in Sections 3.7.2 $-$ 3.7.4 could be
defined using a count of the number of cells of a CAD rather than the time
taken to compute the CAD. In theory, such metrics would be implementation
independent (although in practice, all CAD implementations differ on some of
the underlying theory they implement). The cell count and the time taken
should be closely correlated: we choose to focus on the time taken, as it is
the measure of most value to users.

####  3.7.6. Timeout penalisation

Note that total time and time markup metrics depend on knowing the time needed
to complete a CAD using the variable ordering suggested by the strategy
studied. However, as described in Section 3.1, CADs in Maple were called with
a time limit, after which, if the call has not finished, it is stopped by
Python222We make each CAD call in a separate Maple session launched and timed
by Python to avoid any instance having the benefit of Maple’s previous caching
of intermediate results. For example, the same resultant may be needed for two
different variable orderings, and we want to ensure the cost of its
computation is included in both instances.. When this happens, we do not get
to know the time needed to build a CAD with such an ordering; we only know it
is more than the chosen time limit. However, we need to choose a numerical
value to be able to evaluate these choices. This time should be at least the
time limit; however, to penalise these bad choices, in our implementation, we
set the time to twice the time limit in such cases.

##  4\. Improvements when using the Classification Paradigm

In this section, we will work with the supervised ML classification paradigm,
most commonly used in the literature. First. in Section 4.1, the usual
approach to creation of inputs for the ML model will be described. In Section
4.2 some problems in the created classification dataset will be identified,
and in Section 4.3 some tools will be introduced to solve these problems. In
Section 4.4 the misleading results that can be obtained if these issues are
not detected are presented, and in the following subsections a series of
improvements to the classification model are presented to overcome these
difficulties. The first improvement solves the imbalanced problem in the
training dataset, the second increases the size of the training dataset, and
the last reduces the number of features describing an instance while
preserving most of the information these features carry. These contributions
were largely presented in the SC-Square 2023 workshop paper [15].

###  4.1. Creating a classification instance

A classification instance in supervised learning consists of a pair: an input
and its label. In our case, from each set of polynomials in three variables,
we must find its optimal variable ordering label. We also need to create an
embedding that can be taken as input by a ML model.

####  4.1.1. Creating the inputs

The task here is to represent a set of polynomials in three variables as a
list of features. In Section 3.2 we described a methodology for creating a
list of features, which we will denote by $f_{x}(\mathcal{T})$ for a given
variable $x$ and a given set of polynomials $\mathcal{T}$.

To represent a three-variable set of polynomials
$\mathcal{T}\in\mathbb{R}[x_{1},x_{2},x_{3}]$ to the classification model, we
will therefore use the lists of features created with each variable appended
to each other, placing the features related to the variable $x_{1}$ first,
then those related to $x_{2}$ and finally those related to $x_{3}$. This list
of features will be denoted by
$F_{x_{1},x_{2},x_{3}}(\mathcal{T})=f_{x_{1}}(T)\,|\,f_{x_{2}}(\mathcal{T})\,|\,f_{x_{3}}(\mathcal{T})$.

####  4.1.2. Creating the labels

The labels correspond to the possible variable orderings that a CAD can use
for a set of polynomials $\mathcal{T}\in\mathbb{R}[x_{1},x_{2},x_{3}]$. We
will use as a label the variable ordering for which building a CAD took the
shortest time. We will use the notation $\succ_{ijk}$ to refer to ordering
$x_{i}\succ x_{j}\succ x_{k}$.

####  4.1.3. Illustrative example

For illustration purposes, we will consider a hypothetical example which
producues the timings to build a three-variable CAD indicated in Table 1.
Figure 1 then illustrates how we create ML classification instances from our
working example. This will serve as a comparison for the alternative
methodologies presented later.

Table 1. Hypothetical timings to build a CAD for a set of polynomials with six possible variable orderings Ordering | Timing
---|---
$\succ_{123}$ | 22.16s
$\succ_{132}$ | 17.14s
$\succ_{213}$ | Timeout 30s
$\succ_{231}$ | 24.87
$\succ_{312}$ | 16.06
$\succ_{321}$ | 22.58
Figure 1. Classification training workflow for the example of Section 4.1.3

####  4.1.4. Reflection on the number of variables

Note that the length of the feature array describing the set of polynomials
and the number of labels (possible variable orderings) depends on the number
of variables. Therefore, a model trained on three variable sets will not be
useful for sets of polynomials with a higher number of variables. In Section 5
we will eliminate the dependence the output has on the number of variables,
and in Section 6 we will further eliminate the dependence of the feature array
with respect to the number of variables, creating a strategy that can be used
to choose a variable ordering to build a CAD for sets of polynomials of an
arbitrary number of variables.

###  4.2. Imbalance in the dataset

As observed recently in [15] and [22] an analysis on the classification
dataset described in Section 4.1 reveals that the dataset obtained is
imbalanced: there are far more pairs of labels with ordering $\succ_{123}$
than any of the others, as can be observed in Figure 5. Such an imbalance is a
problem for ML, because models trained on an imbalance dataset will be biased
towards the majority class. Moreover, this problem may go unnoticed if the
testing dataset is also imbalanced in a similar way, reporting misleading
results that will not generalise when testing on a balance dataset.

There is no reason to expect real-world data to have such an imbalance and so
it is essential to balance the data prior to ML to avoid model bias. There are
various approaches: e.g., we could oversample the minority classes (giving
instances in the minority classes multiple times to the model), or undersample
the majority classes (not giving all instances in the majority classes to the
model). Instead, we use a data augmentation technique to generate more
instances of the minority classes.

###  4.3. Improving the datasets with data augmentation

As introduced in Section 1.2, data augmentation consists of generating new
data instances from existing ones and is a common technique in computer
vision.

As a motivating example, let us imagine that we have a dataset of arrows: 56
arrows pointing up, 35 left, 4 downward, and 175 right. Like our CAD dataset,
this dataset is very imbalanced; 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 downward.

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
downward. Similar to this we could rotate by $180^{\circ}$ or $270^{\circ}$
clockwise to give arrows facing left and up, respectively. Editing images in
this way can be very useful because it allows us to obtain a balanced dataset
from the imbalanced dataset: simply randomly rotating each image by
$0^{\circ},90^{\circ},180^{\circ}$ or $270^{\circ}$.

Our instances consist of sets of polynomials, for example,
$\\{x_{1}^{2}-x_{2},x_{3}^{3}-1\\}$ for which we can determine, by computing
and comparing CADs, that the optimal variable ordering to compute an CAD for
this set is $x_{2}\succ x_{1}\succ x_{3}$. Now observe that simply by swapping
the names of the variables $x_{1}$ and $x_{2}$ we may obtain the new set of
polynomials $\\{x_{2}^{2}-x_{1},x_{3}^{3}-1\\}$, in which we know, without any
further CAD computation, that the optimal variable ordering is $x_{1}\succ
x_{2}\succ x_{3}$.

This process of how an instance with a different label can be obtained from an
existing instance is illustrated in Figure 2 for our example of Section 4.1.3.

Figure 2. Data augmentation by swapping $x_{1}$ and $x_{2}$ for the
illustrative example

####  4.3.1. Three datasets

We will refer to the dataset described in Section 3.1 as the “ _imbalanced
dataset_ ”. Similar to how the arrow image dataset can be balanced by randomly
rotating, our dataset can be balanced by randomly permuting the variable
names: we refer to the dataset obtained this was as the the “ _balanced
dataset_ ”. We then go further and fully augment the dataset by including all
possible variable permutations, obtaining six instances from each original
one: creating the “ _augmented dataset_ ”. The distribution of instances to
optimal orderings is illustrated in Figure 5 $-$ Figure 5.

Note that in these two new datasets, instances are first separated in folds
and then either balanced or augmented. This ensures that even when augmenting
the dataset there is no data leakage.

$\succ_{123}$$\succ_{132}$$\succ_{213}$$\succ_{231}$$\succ_{312}$$\succ_{321}$$406$$93$$135$$51$$202$$132$Ordering#
Imbalanced training instances

Figure 3. Instances in the classes in the imbalanced classification dataset.

$\succ_{123}$$\succ_{132}$$\succ_{213}$$\succ_{231}$$\succ_{312}$$\succ_{321}$$188$$170$$153$$158$$188$$162$Ordering#
Balanced training instances

Figure 4. Instances in the classes in the balanced classification dataset.

$\succ_{123}$$\succ_{132}$$\succ_{213}$$\succ_{231}$$\succ_{312}$$\succ_{321}$$1{,}019$$1{,}019$$1{,}019$$1{,}019$$1{,}019$$1{,}019$Ordering#
Augmented training instances

Figure 5. Instances in the classes in the augmented classification dataset.

####  4.3.2. Other ideas to augment the dataset

In computer vision, not only rotations are used as a tool to balance and
augment datasets, but also other operations such as flipping or zooming.

The equivalent of flipping an image for a set of polynomials would be making
changes of variables of the form $y_{i}=(-1)^{j_{i}}x_{i}$, where $j_{i}$ is
an integer for all $i$. This change of variables would not change the
computation of the CAD and therefore the label would remain the same; however,
it does not affect the features used to describe the set of polynomials; so
the instances obtained by this change of variables would be just copies of
existing instances.

The equivalent of zooming an image for a set of polynomials could be making
changes of variables of the form $y_{i}=j_{i}x_{i}+k_{i}$, where
$j_{i},k_{i}\in\mathbb{R}$ for all $i$. These changes of variables do affect
the features used to describe the set of polynomials, mainly because they tend
to change the sparsity of the features, one of the values reflected by the
features used, so they would definitely create new instances. However, these
changes in sparsity also affect the computations of resultants and
discriminants needed to build a CAD, so the label of the instance may change;
meaning that constructing CADs for all possible orderings would be necessary
to find the real label of the instance.

###  4.4. Replicating prior work

To replicate the work done by Florescu and England [20] we used the biased
training dataset to train ML classifiers, and we tested it in the biased
testing dataset. As can be seen in Figure 6, these models perform similarly to
existing heuristics, some outperforming them.

However, these models are trained in a biased dataset, and so likely to learn
to replicate these biases. The biased dataset contains a large percentage of
instances with label $\succ_{123}$, and therefore, the models may simply learn
to predict this class more often. So when these models are tested on a dataset
that has the same bias, their performance may be misleading.

To identify if this is the case, we may evaluate those models trained using
the biased training dataset on the balanced testing dataset. As expected, all
models suffer a very significant performance drop, as illustrated in Figure 7.

Figure 6. Existing heuristics and ML models trained on the biased dataset,
evaluated over the biased dataset. Figure 7. ML models trained on a biased
dataset tested on both imbalanced (I) and balanced (B) datasets

###  4.5. ML classifiers obtained when balancing and augmenting the training
dataset

So models trained imbalanced dataset perform poorly on a balanced one. We will
test whether using the balanced dataset for training the models will improve
the performance: this should be the case since the models will no longer learn
the biases they got when trained in an imbalanced dataset. We will also
evaluate if using the augmented dataset described in Section 4.3 offer further
benefits: it has six times the number of instances of the imbalanced and
balanced datasets.

The results in Tables 4.5 $-$ 4.5 show the performance of models trained on
our three datasets when evaluated on the balanced dataset and confirm our
hypotheses. Balancing the data avoided the biases and the additional data from
further augmentation had a further positive effect.

Training dataset | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 2. Metrics over the balanced testing dataset for the KNN classifier

Training dataset | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 3. Metrics over the balanced testing dataset for the MLP classifier.

Training dataset | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 4. Metrics over the balanced testing dataset for the RF classifier.

Training dataset | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 5. Metrics over the balanced testing dataset for the SVM classifier.

Training dataset | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 6. Metrics over the balanced testing dataset for the XGB classifier.

##  5\. Changing from the Classification to the Regression Paradigm

As we described in Section 1.1, although prior work on ML to make choices for
our problem has employed the classification paradigm, since the choices seek
to minimise a continuous metric the problem may also be conceived as ML
regression. We explore the effects of this paradigm change in this section:
first describing how regression instances are created in Section 5.1, then
presenting an experimental comparison in Section 5.2.

###  5.1. Creating a regression instance

A regression instance consists of a pair: an input and a target. In our case,
the input is formed from the set of polynomials and variable ordering, and the
target will be the time taken to build a CAD for these. The embedding that we
will use to encode the input will be formed by the same three vectors of
features introduced previously in Section 4.1.1 for classification. However
here, as illustrated in Figure 8, the order in which we append the vectors
will be determined by the input variable ordering.

Figure 8. Regression training workflow showing how a single regression
instance is created from just 1 of the 6 orderings for the example of Section
4.1.3; 5 further instances may be created similarly.

This embedding eliminates all existing symmetries in the classification
embedding, so it is not possible to augment this dataset as we did in Section
4.3 for classification. However, the number of instances in the regression
dataset is already as large as that of the augmented classification dataset
since each classification instance becomes six regression instances.
Furthermore, the amount of information encoded in this regression dataset is
greater than in the augmented classification dataset: the latter only includes
information on which is the fastest ordering, but the former has information
about the exact time each ordering took.

Our ML regression models will predict how long it takes to build a CAD for a
given set of polynomials using a given variable ordering. However, this is not
our final goal: we are interested in choosing variable orderings to build a
CAD for a given set of polynomials as fast as possible. Thus, for a given set
of polynomials in the testing dataset, we must ask the regression model to
estimate how long it would take to build a CAD for each of the variable
orderings, and then we will choose the ordering that was estimated to take the
shortest time, as illustrated in Figure 9. This final choice can then be
evaluated using the same metrics introduced in Section 3.7.

Figure 9. Overview of how the regression model is used.

###  5.2. Results comparing classification with regression

Figure 10 compares the total time required to build the CADs in our test
dataset using the variable ordering suggested by each model. We see that the
KNN, RF, and SVM, models all perform better under the regression paradigm,
while the MLP and XGBoost models perform worse. Overall, the best performance
on the dataset is achieved by a model under the regression paradigm. So the
results partially validate our hypothesis that regression can use extra
information to improve performance on the choice, but with the substantial
caveat that it is model dependent.

Figure 10. Comparing the total times to build CADs for the balanced dataset
with the variable ordering suggested by classifiers (Class) and regressors
(Reg)

We also reflect that the scope of choices that can be made using regression is
broader than those that can be made using classification. For example, when
using CAD for Quantifier Elimination, we must project variables in the order
of quantification but still have freedom to change order within quantification
blocks (and the free variables). In this case, if a classifier returns an
option that does not satisfy these restrictions the recommendation is useless;
however, using the regression paradigm, one can simply take the best choice
that meets the restrictions.

###  5.3. Limitations with respect to number of variables

The number of possible outputs the classification models have to choose from
is factorial of the number of variables. A classification model trained for
$n$ variables cannot study a problem with more variables; and although the
methodology could generalise (i.e., we may train new classifiers with a
dataset of problems in more variables), the factorial growth means this will
get harder quickly.

In comparison the regression models presented in this section always produced
a single real number regardless of the number of variables and possible
orderings. The difficulty in generalising will be the embedding used to input
sets of polynomials into both the regression and classification models: this
will still grow with the number of variables, but only linearly.

If we want to choose variable orderings for an arbitrary number of variables,
then ideally we should find an embedding that has an invariant size with
respect to the number of variables. We consider one approach to this in
Section 6.

##  6\. Using Regression to Rank Variables

In Section 5 we trained regression models to estimate how long it would take
to build a CAD for a problem with a given variable ordering. In this section
we will use ML to rank the variables themselves instead of the variable
orderings, allowing for an easier generalisation to more variables.

This is similar to how the human-designed heuristics in Section 2.3 choose a
variable ordering. Human heuristics assign some measure of complexity to the
variables and pick the simpler variables first in the ordering, but their
measure of complexity is defined by the creator of the heuristic and,
therefore, is fixed. Instead, we will train ML models so that they learn their
own measures of complexity, and we will pick the variables that the model
considers to be simpler first in the ordering. This shares a similarity with
Chen et al. [11] who also proposed to train models to choose variables instead
of orderings. However, they still trained classification models and thus
suffer from the limitations discussed above.

###  6.1. Creating instances for regression on variables

Our instances now concern the polynomials and a single variable. For an
embedding we use just the features for that variable, i.e. $f_{x_{i}}(S)$: the
features describing variable $x_{i}$ in a set of polynomials $S$.

In Section 5 we trained ML models to learn the complexity of a variable
ordering and there was a clear output to use: the time necessary to build a
CAD using such variable ordering. In this section, for estimating the
complexity of a variable, we have available the timings of the orderings that
start with that variable: in our three-variable case study there are two
possible orderings that begin with each variable. We use the quickest of these
to label the instance, as illustrated in Figure 11.

Figure 11. Illustration of how the instance for variable $x_{1}$ is encoded
for the example of Section 4.1.3. Note that two further instances for the
other variables will be created similarly.

###  6.2. Results

Tables 6.2 $-$ 6.2 compare the classification paradigm (trained with the
augmented dataset), the regression paradigm on the orderings, and the
regression paradigm on the variables. Interestingly, we see that the two
models which did poorest under the regression paradigm to pick an ordering,
MLP and XGBoost, do better under this alternative regression paradigm (while
the others do worse). The lowest timings overall remains the SVM under the
previous regression paradigm, but given the wider applicability of this
alternative paradigm we think it worthy of consideration.

In Figure 12 we show the spread of timings for the all the key strategies
presented in this paper, represented by letters as below. They show that for
all models the original approach of training on an unbalanced dataset does not
generalise to a balanced dataset (A vs B); but that this performance is
regained and sometimes exceeded by the new approaches of this paper (C $-$ F).
The optimal paradigm does seem to depend on the ML model type being used.

Short name | Training dataset | Testing dataset | Paradigm
---|---|---|---
A | Imbalanced (see Section 4.2) | Imbalanced | Classification
B | Imbalanced | Balanced | Classification
C | Balanced (see Section 4.3) | Balanced | Classification
D | Augmented (see Section 4.3) | Balanced | Classification
E | Regression orderings (See Section 5.1) | Balanced | Regression
F | Regression variables (see Section 6) | Balanced | Regression

Strategy | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 7. Metrics for different strategies using a KNN model.

Strategy | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 8. Metrics for different strategies using a RF model.

Strategy | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 9. Metrics for different strategies using an SVM model.

Strategy | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 10. Metrics for different strategies using a MLP model.

Strategy | Total time | Completed | Accuracy | Markup
---|---|---|---|---
[late after line= |  |  |  |
|  |  |  |

Table 11. Metrics for different strategies using an XGB model.

(a) KNN models.

(b) RF models.

(c) SVM models.

(d) MLP models.

(e) XGBoost models.

Figure 12. The total times achieved by models on the balanced testing dataset
under different strategies

##  7\. Final Thoughts

###  7.1. Conclusions on data balance and augmentation

####  7.1.1. The importance of data exploration

We found in Section 4 that this well known dataset was imbalanced for our
problem and that if we trained classifiers with such imbalanced data they
could not perform well on balanced data. This demonstrates the importance of
exploring the data before moving to ML. Imbalance is not always inappropriate
for ML: some applications will naturally have imbalanced data, and 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 that general CAD applications favour one ordering over
another333except perhaps the existence of the SMT-LIB data!. Thus, our advice
is to ensure that ML models for such applications are trained on balanced
data.

####  7.1.2. Recovering performance through balancing and augmentation

The good news is that ML performance can be improved simply by training on
balanced data, reducing the total time by 28% on average, re-validating the
value of the data science-led approach. A key conclusion here is that it is
beneficial to go further and use maximum data augmentation: all models
benefited from this beyond just balancing the data, no matter which dataset
they are tested on. Training in an augmented dataset of six times the size of
the original dataset reflected in an increase in accuracy of 40% on average
and a reduction of 38% in the total time on average. In fact, the performance
lost from the original imbalanced case is almost fully recovered this way.

####  7.1.3. Comparison with the work of Hester et al. (2023)

Some of these conclusions were also drawn in a recent paper [22]. Table 2 in
[22] presents the accuracies of trained models on different datasets: note
that both their “ _Training Set 2_ ” and “ _Dataset 1_ ” contain instances in
which the models have been trained, meaning that the former is the most
appropriate column for evaluation in that table: that column shows results
similar to ours.

We note that the original dataset in [22] contained 6895 instances, while in
our paper the initial dataset only contained 1019 instances. This is because,
even though both datasets have the same ultimate source (the SMT-LIB), our
dataset had been stripped of potential duplicate instances (sets of
polynomials whose CAD tree structures are potentially identical for every
variable ordering), as described in detail in Section 3.1. We view this as a
necessary step to make meaningful use of the QF_NRA section of the SMT-LIB
where there are many _very_ similar problems.

This comparison with [22] shows that the size alone of the dataset is not what
matters (since [22] has a similar accuracy to the models presented here
despite training with much more data). Rather, it is the _number of
qualitatively different problems within the dataset_. That is, there is little
benefit to including multiple very similar problems. It may seem that data
augmentation adds no new information, but since the ML models are not aware of
these symmetries by exposing them with augmentation, we actually give them
access to this information.

###  7.2. Conclusions on ML paradigms

Despite the fact that the regression dataset contains more information than
the classification one, such as the specific timings of each ordering, this
did not always lead to improvement in the performance of regression models
compared to classification models: it seemed that some models were better able
to do this than others and this choice of paradigm should be optimised along
with model and hyperparameter selection in the ML workflow.

The overall lowest timings were achieved by one of the new regression
approaches. The differences in performance were not huge: as argued in Section
5.2, we suggest that more important than performance statistics is the wider
scope of choices that can be made in symbolic computation using the new
regression methodologies. Consider for example an application to $S$-pair
selection in Buchberger’s algorithm: we do not know in advance of a decision
how many pairs there will be to choose from, but this may be tackled using the
paradigm presented in Section 6, and still under a supervised learning
paradigm rather than using reinforcement learning [32].

###  7.3. Future work

A key area for future work could be the embeddings: those we use still ignore
much information from the polynomials such as all coefficient information. Jia
et al. [26] already proposed a graph embedding that allows inputting a lot of
information about a set of polynomials into a GNN model, and they experience a
performance similar to that of the heuristic gmods in the SMT-LIB dataset and
even beat this heuristic in a randomly generated dataset.

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

Finally, we note that all these ideas would 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.
Further, the lessons we illustrated on the importance of exploratory data
analysis and paradigm choice would be useful to many other choices available
in symbolic computation.

### Acknowledgments

Tereso del Río is supported by Coventry University and a travel grant from the
London Mathematical Society (LMS). Matthew England is supported by UKRI EPSRC
Grant EP/T015748/1, _Pushing Back the Doubly-Exponential Wall of Cylindrical
Algebraic Decomposition_ (the DEWCAD Project).

## References

  * [1] Jiakang Bao, Yang-Hui He, and Edward Hirst.  Neurons on amoebae.  Journal of Symbolic Computation, 116:1–38, 2023.  doi:10.1016/j.jsc.2022.08.021.
  * [2] Clark Barrett and Cesare Tinelli.  Satisfiability Modulo Theories.  In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 305–343. Springer International Publishing, Cham, 2018.  doi:10.1007/978-3-319-10575-8_11.
  * [3] Edgar A. Bernal, Jonathan D. Hauenstein, Dhagash Mehta, Margaret H. Regan, and Tingting Tang.  Machine learning the real discriminant locus.  Journal of Symbolic Computation, 115:409–426, 2023.  doi:10.1016/j.jsc.2022.08.001.
  * [4] R. Bradford, J. H. Davenport, M. England, and D. Wilson.  Optimising problem formulations for cylindrical algebraic decomposition.  In J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger, editors, Intelligent Computer Mathematics, volume 7961 of Lecture Notes in Computer Science, pages 19–34. Springer Berlin Heidelberg, 2013.  doi:10.1007/978-3-642-39320-4_2.
  * [5] Russell Bradford, James H. Davenport, Matthew England, Hassan Errami, Vladimir Gerdt, Dima Grigoriev, Charles Hoyt, Marek Košta, Ovidiu Radulescu, Thomas Sturm, and Andreas Weber.  Identifying the parametric occurrence of multiple steady states for some biological networks.  Journal of Symbolic Computation, 98:84–119, May 2020.  doi:10.1016/j.jsc.2019.07.008.
  * [6] Christopher W. Brown.  Improved projection for cylindrical algebraic decomposition.  Journal of Symbolic Computation, 32(5):447–465, November 2001.  doi:10.1006/jsco.2001.0463.
  * [7] Christopher W Brown.  Companion to the Tutorial Cylindrical Algebraic Decomposition.  In International Symposium on Symbolic and Algebraic Computation - ISSAC, pages 1–14, 2004.  URL: https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf.
  * [8] Christopher W. Brown and James H. Davenport.  The complexity of quantifier elimination and cylindrical algebraic decomposition.  Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC, pages 54–60, 2007.  doi:10.1145/1277548.1277557.
  * [9] Christopher W. Brown and Glenn Christopher Daves.  Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving.  In A. Bigatti, J. Carette, J. H. Davenport, M. Joswig, and T. de Wolff, editors, Mathematical Software – ICMS 2020, volume 12097 of Lecture Notes in Computer Science, pages 292–301. Springer International Publishing, 2020.  doi:10.1007/978-3-030-52200-1_29.
  * [10] C. Chen and M. Moreno Maza.  Cylindrical algebraic decomposition in the RegularChains library.  In H. Hong and C. Yap, editors, Mathematical Software – ICMS 2014, volume 8592 of Lecture Notes in Computer Science, pages 425–433. Springer Heidelberg, 2014.  doi:10.1007/978-3-662-44199-2_65.
  * [11] Changbo Chen, Zhangpeng Zhu, and Haoyu Chi.  Variable Ordering Selection for Cylindrical Algebraic Decomposition with Artificial Neural Networks.  In Lecture Notes in Computer Science, volume 12097 LNCS, pages 281–291. Springer, 2020.  doi:10.1007/978-3-030-52200-1_28.
  * [12] George E. Collins.  Quantifier elimination for real closed fields by cylindrical algebraic decomposition.  Lecture Notes in Computer Science, 33 (Proc. of the 2nd GI Conference on Automata Theory and Formal Languages):134–183, 1975.  doi:10.1007/3-540-07407-4_17.
  * [13] James H. Davenport and Joos Heintz.  Real quantifier elimination is doubly exponential.  Journal of Symbolic Computation, 5(1-2):29–35, February 1988.  doi:10.1016/S0747-7171(88)80004-X.
  * [14] Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli.  Advancing mathematics by guiding human intuition with AI.  Nature, 600:70–74, 2021.  doi:10.1038/s41586-021-04086-x.
  * [15] T. del Rio and M. England.  Data augmentation for mathematical objects.  In E. Ábrahám and T. Sturm, editors, Proceedings of the 8th Workshop on Satisfiability Checking and Symbolic Computation ($\mathsf{SC}^{2}$ 2023), number 3455 in CEUR Workshop Proceedings, pages 29–38, 2023.  URL: http://ceur-ws.org/Vol-3455/.
  * [16] Tereso del Río and Matthew England.  New Heuristic to Choose a Cylindrical Algebraic Decomposition Variable Ordering Motivated by Complexity Analysis.  In François Boulier, Matthew England, Timur M. Sadykov, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing, volume 13366 of Lecture Notes in Computer Science, pages 300–317. Springer International Publishing, Cham, 2022.  doi:10.1007/978-3-031-14788-3_17.
  * [17] Andreas Dolzmann, Andreas Seidl, and Thomas Sturm.  Efficient projection orders for CAD.  In Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation - ISSAC, pages 111–118, New York, New York, USA, 2004. ACM Press.  doi:10.1145/1005285.1005303.
  * [18] Matthew England and Dorian Florescu.  Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition.  In Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, volume 11617 of Lecture Notes in Computer Science, pages 93–108. Springer International Publishing, Cham, 2019.  doi:10.1007/978-3-030-23250-4_7.
  * [19] Dorian Florescu and Matthew England.  Algorithmically generating new algebraic features of polynomial systems for machine learning.  In J. Abbott and A. Griggio, editors, Proceedings of the 4th Workshop on Satisfiability Checking and Symbolic Computation ($\mathsf{SC}^{2}$ 2019), number 2460 in CEUR Workshop Proceedings. CEUR-WS, 2019.  URL: http://ceur-ws.org/Vol-2460/.
  * [20] Dorian Florescu and Matthew England.  Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness.  In D. Slamanig, E. Tsigaridas, and Z. Zafeirakopoulos, editors, Mathematical Aspects of Computer and Information Sciences (Proc. MACIS ’19), volume 11989 of Lecture Notes in Computer Science, pages 341–356. Springer, 2020.  doi:10.1007/978-3-030-43120-4_27.
  * [21] Alessandro Giovini, Teo Mora, Gianfranco Niesi, Lorenzo Robbiano, and Carlo Traverso.  “One sugar cube, please” or selection strategies in the Buchberger algorithm.  In Proceedings of the 1991 International Symposium on Symbolic and Algebraic Computation, ISSAC ’91, pages 49–54, New York, NY, USA, June 1991. Association for Computing Machinery.  doi:10.1145/120694.120701.
  * [22] John Hester, Briland Hitaj, Grant Passmore, Sam Owre, Natarajan Shankar, and Eric Yeh.  An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning.  In Catherine Dubois and Manfred Kerber, editors, Intelligent Computer Mathematics, Lecture Notes in Computer Science, pages 297–302, Cham, 2023. Springer Nature Switzerland.  doi:10.1007/978-3-031-42753-4_21.
  * [23] Z. Huang, M. England, J. H. Davenport, and L. Paulson.  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), pages 45–52. IEEE, 2016.  doi:10.1109/SYNASC.2016.020.
  * [24] Z. Huang, M. England, D. Wilson, J. Bridge, J. H. Davenport, and L. Paulson.  Using machine learning to improve cylindrical algebraic decomposition.  Mathematics in Computer Science, 13(4):461–488, 2019.  doi:10.1007/s11786-019-00394-8.
  * [25] Zongyan Huang, Matthew England, David Wilson, James H. Davenport, Lawrence C. Paulson, and James Bridge.  Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition.  In S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, editors, Lecture Notes in Computer Science, volume 8543 of Lecture Notes in Artificial Intelligence, pages 92–107. Springer Verlag, 2014.  doi:10.1007/978-3-319-08434-3_8.
  * [26] Fuqi Jia, Yuhang Dong, Minghao Liu, Pei Huang, Feifei Ma, and Jian Zhang.  Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning.  In Thirty-Seventh Conference on Neural Information Processing Systems, November 2023.  URL: https://openreview.net/forum?id=vNsdFwjPtL.
  * [27] M. Kauers and J. Moosbauer.  Good pivots for small sparse matrices.  In F. Boulier, M. England, T. M. Sadykov, and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing, volume 12291 of Lecture Notes in Computer Science, pages 358–367. Springer International Publishing, 2020.  doi:10.1007/978-3-030-60026-6_20.
  * [28] Max Kuhn and Kjell Johnson.  Applied Predictive Modeling.  Springer, New York, NY, 2013.  doi:10.1007/978-1-4614-6849-3.
  * [29] Guillaume Lample and François Charton.  Deep Learning for Symbolic Mathematics.  Proc. International Conference on Learning Representations, 2020.  doi:10.48550/ARXIV.1912.01412.
  * [30] Haokun Li, Bican Xia, Huiying Zhang, and Tao Zheng.  Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure.  Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC, pages 281–288, 2021.  doi:10.1145/3452143.3465520.
  * [31] Lawrence C. Paulson.  MetiTarski: Past and Future.  In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, Lecture Notes in Computer Science, pages 1–10, Berlin, Heidelberg, 2012. Springer.  doi:10.1007/978-3-642-32347-8_1.
  * [32] Dylan Peifer, Michael Stillman, and Daniel Halpern-Leistner.  Learning selection strategies in Buchberger’s algorithm.  In International Conference on Machine Learning, pages 7575–7585. PMLR, 2020.  URL: https://proceedings.mlr.press/v119/peifer20a.html.
  * [33] Lynn Pickering, Tereso Del Rio Almajano, Matthew England, and Kelly Cohen.  Explainable AI insights for symbolic computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition.  Journal of Symbolic Computation, TBC:TBC, 2024.  URL: https://doi.org/10.1016/j.jsc.2023.102276.
  * [34] Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh.  MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.  TACAS 2021: Tools and Algorithms for the Construction and Analysis of Systems, pages 303–325, March 2021.  doi:10.1007/978-3-030-72013-1_16.
  * [35] Connor Shorten and Taghi M. Khoshgoftaar.  A survey on Image Data Augmentation for Deep Learning.  Journal of Big Data, 6(1):60, 2019.  doi:10.1186/s40537-019-0197-0.
  * [36] Matthew C. Simpson, Qing Yi, and Jugal Kalita.  Automatic Algorithm Selection in Computational Software Using Machine Learning.  In 15th IEEE Intl. Conf. on Machine Learning and Applications, pages 355–360, 2016.  doi:10.1109/ICMLA.2016.0064.
  * [37] Robert Vajda and Zoltán Kovács.  GeoGebra and the realgeom Reasoning Tool.  In Pascal Fontaine, K. Korovin, I.S. Kotsireas, P. Rümmer, and S. Tourret, editors, Proceedings of the 5th Workshop on Satisfiability Checking and Symbolic Computation (SC-square 2020), volume 2752 of CEUR Workshop Proceedings, pages 204–219, November 2020.  URL: http://ceur-ws.org/Vol-2752/.
  * [38] David Wilson, Matthew England, Russell Bradford, and James H. Davenport.  Using the distribution of cells by dimension in a cylindrical algebraic decomposition.  Proceedings - 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, pages 53–60, 2015.  doi:10.1109/SYNASC.2014.15.
  * [39] Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown.  SATzilla: Portfolio-based Algorithm Selection for SAT.  Journal of Artificial Intelligence Research, 32:565–606, July 2008.  doi:10.1613/jair.2490.