arXiv subjects

Matthew England

Publications and source records attributed to Matthew England.

At least 55 records · Page 3Linked to original sources

arXiv2019

Cylindrical Algebraic Decomposition with Equational Constraints

Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding prominence in the Satisfiability Checking community as a tool to identify satisfying solutions of problems in nonlinear real arithmetic. The original algorithm produces decompositions according to the signs of polynomials, when what is usually required is a decomposition according to the truth of a formula containing those polynomials. One approach to achieve that coarser (but hopefully cheaper) decomposition is to reduce the polynomials identified in the CAD to reflect a logical structure which reduces the solution space dimension: the presence of Equational Constraints (ECs). This paper may act as a tutorial for the use of CAD with ECs: we describe all necessary background and the current state of the art. In particular, we present recent work on how McCallum's theory of reduced projection may be leveraged to make further savings in the lifting phase: both to the polynomials we lift with and the cells lifted over. We give a new complexity analysis to demonstrate that the double exponent in the worst case complexity bound for CAD reduces in line with the number of ECs. We show that the reduction can apply to both the number of polynomials produced and their degree.

cs.SC↗

arXiv2018

Computing with Codio at Coventry University: Online virtual Linux boxes and automated formative feedback

We describe our experience using Codio at Coventry University in our undergraduate programming curriculum. Codio provides students with online virtual Linux boxes, and allows staff to equip these with guides written in markdown and supplemental tasks that provide automated feedback. The use of Codio has coincided with a steady increase in student performance and satisfaction as well as far greater data on student engagement and performance.

cs.CY↗

arXiv2018

A Combined CNN and LSTM Model for Arabic Sentiment Analysis

Deep neural networks have shown good data modelling capabilities when dealing with challenging and large datasets from a wide range of application areas. Convolutional Neural Networks (CNNs) offer advantages in selecting good features and Long Short-Term Memory (LSTM) networks have proven good abilities of learning sequential data. Both approaches have been reported to provide improved results in areas such image processing, voice recognition, language translation and other Natural Language Processing (NLP) tasks. Sentiment classification for short text messages from Twitter is a challenging task, and the complexity increases for Arabic language sentiment classification tasks because Arabic is a rich language in morphology. In addition, the availability of accurate pre-processing tools for Arabic is another current limitation, along with limited research available in this area. In this paper, we investigate the benefits of integrating CNNs and LSTMs and report obtained improved accuracy for Arabic sentiment analysis on different datasets. Additionally, we seek to consider the morphological diversity of particular Arabic words by using different sentiment classification levels.

cs.CL↗

arXiv2018

Towards Incremental Cylindrical Algebraic Decomposition in Maple

Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems for polynomial systems over the reals. It has long been studied by the Symbolic Computation community and has found recent interest in the Satisfiability Checking community. The present report describes a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and then refined as additional polynomial constraints are added. The aim is to make CAD suitable for use as a theory solver for SMT tools who search for solutions by continually reformulating logical formula and querying whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard valuation).

cs.SC↗

arXiv2018

Quantifier Elimination for Reasoning in Economics

We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating to the 1970s. There is a great body of work considering its application in science and engineering but we show here how it can also find application in the social sciences. We explain how many suggested theorems in economics could either be proven, or even have their hypotheses shown to be inconsistent, automatically; and describe the application of this in both economics education and research. We describe a bank of QE examples gathered from economics literature and note the structure of these are, on average, quite different to those occurring in the computer algebra literature. This leads us to suggest a new incremental QE approach based on result memorization of commonly occurring generic QE results.

cs.SC↗

arXiv2018

Using Machine Learning to Improve Cylindrical Algebraic Decomposition

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

cs.SC↗

arXiv2018

Summer Research Report: Towards Incremental Lazard Cylindrical Algebraic Decomposition

Cylindrical Algebraic Decomposition (CAD) is an important tool within computational real algebraic geometry, capable of solving many problems to do with polynomial systems over the reals, but known to have worst-case computational complexity doubly exponential in the number of variables. It has long been studied by the Symbolic Computation community and is implemented in a variety of computer algebra systems, however, it has also found recent interest in the Satisfiability Checking community for use with SMT-solvers. The SCSC Project seeks to build bridges between these communities. The present report describes progress made during a Research Internship in Summer 2017 funded by the EU H2020 SCSC CSA. We describe a proof of concept implementation of an Incremental CAD algorithm in Maple, where CADs are built and refined incrementally by polynomial constraint, in contrast to the usual approach of a single computation from a single input. This advance would make CAD of use to SMT-solvers who search for solutions by constantly reformulating logical formula and querying solvers like CAD for whether a logical solution is admissible. We describe experiments for the proof of concept, which clearly display the computational advantages when compared to iterated re-computation. In addition, the project implemented this work under the recently verified Lazard projection scheme (with corresponding Lazard evaluation). That is the minimal complete CAD method in theory, and this is the first documented implementation.

cs.SC↗

arXiv2018

Improving Sentiment Analysis in Arabic Using Word Representation

The complexities of Arabic language in morphology, orthography and dialects makes sentiment analysis for Arabic more challenging. Also, text feature extraction from short messages like tweets, in order to gauge the sentiment, makes this task even more difficult. In recent years, deep neural networks were often employed and showed very good results in sentiment classification and natural language processing applications. Word embedding, or word distributing approach, is a current and powerful tool to capture together the closest words from a contextual text. In this paper, we describe how we construct Word2Vec models from a large Arabic corpus obtained from ten newspapers in different Arab countries. By applying different machine learning algorithms and convolutional neural networks with different text feature selections, we report improved accuracy of sentiment classification (91%-95%) on our publicly available Arabic language health sentiment dataset [1]

cs.CL↗

arXiv2018

OpenMath and SMT-LIB

OpenMath and SMT-LIB are languages with very different origins, but both "represent mathematics". We describe SMT-LIB for the OpenMath community and consider adaptations for both languages to support the growing SC-Square initiative.

cs.SC↗

arXiv2017

The Potential and Challenges of CAD with Equational Constraints for SC-Square

Cylindrical algebraic decomposition (CAD) is a core algorithm within Symbolic Computation, particularly for quantifier elimination over the reals and polynomial systems solving more generally. It is now finding increased application as a decision procedure for Satisfiability Modulo Theories (SMT) solvers when working with non-linear real arithmetic. We discuss the potentials from increased focus on the logical structure of the input brought by the SMT applications and SC-Square project, particularly the presence of equational constraints. We also highlight the challenges for exploiting these: primitivity restrictions, well-orientedness questions, and the prospect of incrementality.

cs.SC↗

arXiv2017

Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks

We investigate models of the mitogenactivated protein kinases (MAPK) network, with the aim of determining where in parameter space there exist multiple positive steady states. We build on recent progress which combines various symbolic computation methods for mixed systems of equalities and inequalities. We demonstrate that those techniques benefit tremendously from a newly implemented graph theoretical symbolic preprocessing method. We compare computation times and quality of results of numerical continuation methods with our symbolic approach before and after the application of our preprocessing.

cs.SC↗

arXiv2017

A Case Study on the Parametric Occurrence of Multiple Steady States

We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters.

cs.SC↗

arXiv2017

Arabic Language Sentiment Analysis on Health Services

The social media network phenomenon leads to a massive amount of valuable data that is available online and easy to access. Many users share images, videos, comments, reviews, news and opinions on different social networks sites, with Twitter being one of the most popular ones. Data collected from Twitter is highly unstructured, and extracting useful information from tweets is a challenging task. Twitter has a huge number of Arabic users who mostly post and write their tweets using the Arabic language. While there has been a lot of research on sentiment analysis in English, the amount of researches and datasets in Arabic language is limited. This paper introduces an Arabic language dataset which is about opinions on health services and has been collected from Twitter. The paper will first detail the process of collecting the data from Twitter and also the process of filtering, pre-processing and annotating the Arabic text in order to build a big sentiment analysis dataset in Arabic. Several Machine Learning algorithms (Naive Bayes, Support Vector Machine and Logistic Regression) alongside Deep and Convolutional Neural Networks were utilized in our experiments of sentiment analysis on our health dataset.

cs.CL↗

arXiv2016

Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition

In the paper which inspired the SC-Square project, [E. Abraham, Building Bridges between Symbolic Computation and Satisfiability Checking, Proc. ISSAC '15, pp. 1-6, ACM, 2015] the author identified the use of sophisticated heuristics as a technique that the Satisfiability Checking community excels in and from which it is likely the Symbolic Computation community could learn and prosper. To start this learning process we summarise our experience with heuristic development for the computer algebra algorithm Cylindrical Algebraic Decomposition. We also propose and discuss standards and benchmarks as another area where Symbolic Computation could prosper from Satisfiability Checking expertise, noting that these have been identified as initial actions for the new SC-Square community in the CSA project, as described in [E.~Abraham et al., SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper)}, Intelligent Computer Mathematics (LNCS 9761), pp. 28--43, Springer, 2015].

cs.SC↗

arXiv2016

Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases

Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, particularly for quantifier elimination over real-closed fields. However, it can be expensive, with worst case complexity doubly exponential in the size of the input. Hence it is important to formulate the problem in the best manner for the CAD algorithm. One possibility is to precondition the input polynomials using Groebner Basis (GB) theory. Previous experiments have shown that while this can often be very beneficial to the CAD algorithm, for some problems it can significantly worsen the CAD performance. In the present paper we investigate whether machine learning, specifically a support vector machine (SVM), may be used to identify those CAD problems which benefit from GB preconditioning. We run experiments with over 1000 problems (many times larger than previous studies) and find that the machine learned choice does better than the human-made heuristic.

cs.SC↗

arXiv2016

Need Polynomial Systems be Doubly-exponential?

Polynomial Systems, or at least their algorithms, have the reputation of being doubly-exponential in the number of variables [Mayr and Mayer, 1982], [Davenport and Heintz, 1988]. Nevertheless, the Bezout bound tells us that that number of zeros of a zero-dimensional system is singly-exponential in the number of variables. How should this contradiction be reconciled? We first note that [Mayr and Ritscher, 2013] shows that the doubly exponential nature of Gröbner bases is with respect to the dimension of the ideal, not the number of variables. This inspires us to consider what can be done for Cylindrical Algebraic Decomposition which produces a doubly-exponential number of polynomials of doubly-exponential degree. We review work from ISSAC 2015 which showed the number of polynomials could be restricted to doubly-exponential in the (complex) dimension using McCallum's theory of reduced projection in the presence of equational constraints. We then discuss preliminary results showing the same for the degree of those polynomials. The results are under primitivity assumptions whose importance we illustrate.

cs.SC↗

arXiv2016

The complexity of cylindrical algebraic decomposition with respect to polynomial degree

Cylindrical algebraic decomposition (CAD) is an important tool for working with polynomial systems, particularly quantifier elimination. However, it has complexity doubly exponential in the number of variables. The base algorithm can be improved by adapting to take advantage of any equational constraints (ECs): equations logically implied by the input. Intuitively, we expect the double exponent in the complexity to decrease by one for each EC. In ISSAC 2015 the present authors proved this for the factor in the complexity bound dependent on the number of polynomials in the input. However, the other term, that dependent on the degree of the input polynomials, remained unchanged. In the present paper the authors investigate how CAD in the presence of ECs could be further refined using the technology of Groebner Bases to move towards the intuitive bound for polynomial degree.

cs.SC↗

arXiv2015

Truth Table Invariant Cylindrical Algebraic Decomposition

When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

cs.SC↗