SearcharxivSearch

arXiv subjects

Matthew England

Publications and source records attributed to Matthew England.

At least 19 recordsLinked to original sources

Letting Homogeneity Entropy Select S-Pairs in Buchberger's Algorithm

We present a novel S-pair selection strategy called Homogeneity Entropy, for deciding the sequence of S-polynomials to construct in Buchberger's algorithm to compute a Groebner basis. The strategy uses an information theoretic measure derived from the distribution of degrees among the monomials of the S-polynomial: a very different approach to the classical heuristics such as Degree, Normal and Sugar, or indeed the more recent machine learning approaches to the problem. We implement this strategy and evaluate it on two different datasets: (1) variations of randomly generated polynomial systems with controlled numbers of variables, degrees, densities and number of polynomials per system; and (2) the PHCpack benchmark dataset sourced from real world problems. The Homogeneity Entropy strategy significantly outperforms classical strategies on random polynomial datasets, but on the PHCpack dataset the classical strategies perform better. This suggests the right strategy varies with the shape of the data and we explore this in several experiments. The new strategy offers practically meaningful gains on certain distributions, and represents the first use of such information-theoretic guidance in the optimisation of symbolic computation algorithms.

cs.IT

Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints

This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $\phi^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $\phi^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $\nu$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $\nu$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems.

cs.SC

Optimising Cylindrical Algebraic Coverings for use in SMT by Solving a Set Covering Problem with Reasons

The Conflict-Driven Cylindrical Algebraic Covering algorithm has proven well suited for performing theory validation checks in the satisfiability modulo theories paradigm for non-linear real arithmetic. CDCAC repurposes the theory underpinning classical cylindrical algebraic decomposition for SMT solving and is implemented in the SMT solvers cvc5 and SMT-RAT, as well as the computer algebra system Maple. It was previously observed that when using cylindrical algebraic decomposition for an SMT theory call, the output can be optimised by solving a single set covering problem instance that minimises the conflict clause. In this paper we consider the corresponding optimisation for CDCAC and observe that CDCAC naturally gives rise to multiple such optimisations within a single call. Each time a covering is generalised in one dimension, the resulting cell in the next dimension is labelled with theory constraints that cannot be satisfied together. We seek the smallest subset of constraints whose union covers all labels from the cells in the current covering. We call this optimisation problem a set covering problem with reasons. To simplify this problem, we introduce a data reduction step that generalises Beasley reduction for the classical set covering problem and show that this step alone solves many of the instances arising from SMT-LIB benchmarks. We then propose an exact solver based on linear programming to efficiently solve the remaining cases. Integrating these techniques into CDCAC has the potential to significantly improve SMT solver performance for non-linear real arithmetic problems.

cs.DS

Tree-Based Deep Learning for Ranking Symbolic Integration Algorithms

Symbolic indefinite integration in Computer Algebra Systems such as Maple involves selecting the most effective algorithm from multiple available methods. Not all methods will succeed for a given problem, and when several do, the results, though mathematically equivalent, can differ greatly in presentation complexity. Traditionally, this choice has been made with minimal consideration of the problem instance, leading to inefficiencies. We present a machine learning (ML) approach using tree-based deep learning models within a two-stage architecture: first identifying applicable methods for a given instance, then ranking them by predicted output complexity. Furthermore, we find representing mathematical expressions as tree structures significantly improves performance over sequence-based representations, and our two-stage framework outperforms alternative ML formulations. Using a diverse dataset generated by six distinct data generators, our models achieve nearly 90% accuracy in selecting the optimal method on a 70,000 example holdout test set. On an independent out-of-distribution benchmark from Maple's internal test suite, our tree transformer model maintains strong generalisation, outperforming Maple's built-in selector and prior ML approaches. These results highlight the critical role of data representation and problem framing in ML for symbolic computation, and we expect our methodology to generalise effectively to similar optimisation problems in mathematical software.

cs.SC

Projective Delineability for Single Cell Construction

The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.

cs.SC

Predicting At-Risk Programming Students in Small Imbalanced Datasets using Synthetic Data

This study is part of a larger project focused on measuring, understanding, and improving student engagement in programming education. We investigate whether synthetic data generation can help identify at-risk students earlier in a small, imbalanced dataset from an introductory programming module. The analysis used anonymised records from 379 students, with 15\% marked as failing, and applied several machine learning algorithms. The first experiments showed poor recall for the failing group. However, using synthetic data generation methods led to a significant improvement in performance. Our results suggest that machine learning can help identify at-risk students early in programming courses when combined with synthetic data. This research lays the groundwork for validating and using these models with live student cohorts in the future, to allow for timely and effective interventions that can improve student outcomes. It also includes feature importance analysis to refine formative tasks. Overall, this study contributes to developing practical workflows that help detect disengagement early and improve student success in programming education.

cs.CY

On Projective Delineability

We consider cylindrical algebraic decomposition (CAD) and the key concept of delineability which underpins CAD theory. We introduce the novel concept of projective delineability which is easier to guarantee computationally. We prove results about this which can allow reduced CAD computations.

math.AG

Transformers to Predict the Applicability of Symbolic Integration Routines

Symbolic integration is a fundamental problem in mathematics: we consider how machine learning may be used to optimise this task in a Computer Algebra System (CAS). We train transformers that predict whether a particular integration method will be successful, and compare against the existing human-made heuristics (called guards) that perform this task in a leading CAS. We find the transformer can outperform these guards, gaining up to 30% accuracy and 70% precision. We further show that the inference time of the transformer is inconsequential which shows that it is well-suited to include as a guard in a CAS. Furthermore, we use Layer Integrated Gradients to interpret the decisions that the transformer is making. If guided by a subject-matter expert, the technique can explain some of the predictions based on the input tokens, which can lead to further optimisations.

cs.LG

Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition

This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.

cs.SC

Understanding Multistationarity of Fully Open Reaction Networks

This work addresses multistationarity of fully open reaction networks equipped with mass action kinetics. We improve upon the existing results relating existence of positive feedback loops in a reaction network and multistationarity; and we provide a novel deterministic operation to generate new non-multistationary networks. This is interesting because while there were many operations to create infinitely many new multistationary networks from a multistationary example, this is the first such operation for the non-multistationary counterpart. Such tools for the generation of example networks have a use-case in the application of data science to reaction network theory. We demonstrate this by using the new data, along with a novel graph representation of reaction networks that is unique up to a permutation on the name of species of the network, to train a graph attention neural network model to predict multistationarity of reaction networks. This is the first time machine learning tools are used for studying classification problems of reaction networks.

q-bio.MN

The Liouville Generator for Producing Integrable Expressions

There has been a growing need to devise processes that can create comprehensive datasets in the world of Computer Algebra, both for accurate benchmarking and for new intersections with machine learning technology. We present here a method to generate integrands that are guaranteed to be integrable, dubbed the LIOUVILLE method. It is based on Liouville's theorem and the Parallel Risch Algorithm for symbolic integration. We show that this data generation method retains the best qualities of previous data generation methods, while overcoming some of the issues built into that prior work. The LIOUVILLE generator is able to generate sufficiently complex and realistic integrands, and could be used for benchmarking or machine learning training tasks related to symbolic integration.

cs.SC

Constrained Neural Networks for Interpretable Heuristic Creation to Optimise Computer Algebra Systems

We present a new methodology for utilising machine learning technology in symbolic computation research. We explain how a well known human-designed heuristic to make the choice of variable ordering in cylindrical algebraic decomposition may be represented as a constrained neural network. This allows us to then use machine learning methods to further optimise the heuristic, leading to new networks of similar size, representing new heuristics of similar complexity as the original human-designed one. We present this as a form of ante-hoc explainability for use in computer algebra development.

cs.SC

Symbolic Integration Algorithm Selection with Machine Learning: LSTMs vs Tree LSTMs

Computer Algebra Systems (e.g. Maple) are used in research, education, and industrial settings. One of their key functionalities is symbolic integration, where there are many sub-algorithms to choose from that can affect the form of the output integral, and the runtime. Choosing the right sub-algorithm for a given problem is challenging: we hypothesise that Machine Learning can guide this sub-algorithm choice. A key consideration of our methodology is how to represent the mathematics to the ML model: we hypothesise that a representation which encodes the tree structure of mathematical expressions would be well suited. We trained both an LSTM and a TreeLSTM model for sub-algorithm prediction and compared them to Maple's existing approach. Our TreeLSTM performs much better than the LSTM, highlighting the benefit of using an informed representation of mathematical expressions. It is able to produce better outputs than Maple's current state-of-the-art meta-algorithm, giving a strong basis for further research.

cs.LG

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

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.

cs.SC

Iterated Resultants and Rational Functions in Real Quantifier Elimination

This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic. First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport and England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum and Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an unhelpful typo and provide a proof missing from that paper. We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative.

cs.SC

Iterated Resultants in CAD

Cylindrical Algebraic Decomposition (CAD) by projection and lifting requires many iterated univariate resultants. It has been observed that these often factor, but to date this has not been used to optimise implementations of CAD. We continue the investigation into such factorisations, writing in the specific context of SC-Square.

cs.SC

SMT-Solving Induction Proofs of Inequalities

This paper accompanies a new dataset of non-linear real arithmetic problems for the SMT-LIB benchmark collection. The problems come from an automated proof procedure of Gerhold--Kauers, which is well suited for solution by SMT. The problems of this type have not been tackled by SMT-solvers before. We describe the proof technique and give one new such proof to illustrate it. We then describe the dataset and the results of benchmarking. The benchmarks on the new dataset are quite different to the existing ones. The benchmarking also brings forward some interesting debate on the use/inclusion of rational functions and algebraic numbers in the SMT-LIB.

cs.SC

Data Augmentation for Mathematical Objects

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 effect. We finish the paper by reflecting on how this idea could be applied in other uses of machine learning in mathematics.

cs.SC