Embedding Machine Learning within Quantifier Elimination Procedures

EPSRC Project EP/R019622/1
EPSRC First Grant for Dr Matthew England (Coventry University)

Latest News:

August 2020: The project is formerly finished. But collaboration continues between Coventry and Dorian Florescu (now at Imperial College London) on a journal paper. A PhD student has been recruited to continue this work - they are due to start in September 2020 (COVID19 allowing).

July 2020: There was a concluding workshop for the grant, as a session at ICMS 2020, titled Artificial Intelligence and Mathematical Software.

July 2020: Dr England was invited to give a tutorial on Machine Learning and Computer Algebra at ISSAC 2020. Sadly it was cancelled due to COVID19 but the abstract was included in the proceedings: DOI: 10.1145/3373207.3403981.

November 2019: Project work presented at the conference on Mathematical Aspects of Computer and Information Sciences (MACIS) in Istanbul, Turkey. Link to paper in the list below. Link to Slides.

October 2019: Project work presented at The The Maple Conference in Waterloo, Ontario Canada. Link to Slides.

July 2019: We won the Best Paper Award at CICM 2019.

July 2019: Project work presented at both:
The Conference on Intelligent Computer Mathematics (CICM) in Prague, Czech Republic. Link to paper in the list below. Link to Slides.
The SIAM Conference on Applied Algebraic Geometry (SIAM AG) in Bern, Switzerland. Link to paper in the list below. Link to Slides.

June 2019: Poster of project results presented at the Conference on Effective Methods in Algebraic Geometry (MEGA) in Madrid, Spain.
Link to Poster (pdf).

May 2019: Postdoctoral Researcher Dorian Florescu gives a talk to the general public as part of the 2019 Pints of Science festival: Event Link.

May 2019: Project work discussed at the 8th LMS Workshop on Applied Algebraic Geometry in Glasgow, UK.

April 2019: Project work discussed at the British Colloquium for Theoretical Computer Science (BCTCS) in Durham, UK.

December 2019: Postdoctoral Researcher Dorian Florescu starts working full time for the project.

September 2018: Recruitment begins for PhD Student. Job Advert.

July 2018: Kick off Session at ICMS 2018. The topic, Machine Learning for Mathematical Software was broader than the project, with the aim of learning from best practice in similar fields. This Webpage contains slides from the presentations. The session considered the use of Machine Learning in: multiple real QE procedures (England, Kobayashi, Sturm), computer algebra systems / graph theory (Forrest), SMT solvers (Abraham), mathematical knowledge management (Dong), group theory (Gryak) and theorem proving (Urban).

July 2018:Recruitment begins for project Postdoc. Job Advert.

July 2018: Project officially starts.

Dec 2017: EPSRC confirms that the project is to be funded. EPSRC Grant Page.

Project Summary for a General Audience

This project concerns computational mathematics and logic. The aim is to improve the ability of computers to perform ``Quantifier Elimination'' (QE). We say a logical statement is ``quantified'' if it is preceded by a qualification such as "for all" or "there exists". Here is an example of a quantified statement: "there exists x such that ax^2 + bx + c = 0 has two solutions for x". While the statement is mathematically precise the implications are unclear - what restrictions does this statement of existence force upon us? QE corresponds to replacing a quantified statement by an unquantified one which is equivalent. In this case we may replace the statement by: "b^2 - 4ac > 0", which is the condition for x to have two solutions.

You may have recognised this equivalence from GCSE mathematics, when studying the quadratic equation. The important point here is that the latter statement can actually be derived automatically by a computer from the former, using a QE procedure. QE is not subject to the numerical rounding errors of most computations. Solutions are not in the form of a numerical answer but an algebraic description which offers insight into the structure of the problem at hand. In the example above, QE shows us not what the solutions to a particular quadratic equation are, but how in general the number of solutions depends on the coefficients a, b, and c.

QE has numerous applications throughout engineering and the sciences. An example from biology is the determination of medically important values of parameters in a biological network; while another from economics is identifying which hypotheses in economic theories are compatible, and for what values of the variables. In both cases, QE can theoretically help, but in practice the size of the statements means state-of-the-art procedures run out of computer time/memory.

The extensive development of QE procedures means they have many options and choices about how they are run. These decisions can greatly affect how long QE takes, rendering an intractable problem easy and vice versa. Making the right choice is a critical, but understudied problem and is the focus of this project. At the moment QE procedures make such choices either under direct supervision of a human or based on crude human-made heuristics (rules of thumb based on intuition / experience but with limited scientific basis). The purpose of this project is to replace these by machine learning techniques. Machine Learning (ML) is an overarching term for tools that allow computers to make decisions that are not explicitly programmed, usually involving the statistical analysis of large quantities of data. ML is quite at odds with the field of Symbolic Computation which studies QE, as the latter prizes exact correctness and so shuns the use of probabilistic tools making its application here very novel. We are able to combine these different worlds because the choices which we will use ML to make will all produce a correct and exact answer (but with different computational costs).

The project follows pilot studies undertaken by the PI which experimented with one ML technique and found it improved upon existing heuristics for two particular decisions in a QE algorithm. We will build on this by working with the spectrum of leading ML tools to identify the optimal techniques for application in Symbolic Computation. We will demonstrate their use for both low level algorithm decisions and choices between different theories and implementations. Although focused on QE, we will also demonstrate ML as being a new route to optimisation in Computer Algebra more broadly and work encompasses Project Partners and events to maximise this. Finally, the project will deliver an improved QE procedure that makes use of ML automatically, without user input. This will be produced in the commercial Computer Algebra software Maple in collaboration with industrial Project Partner Maplesoft.

Project Staff

The Project is led by Principle Investigator Dr Matthew England, who is an Associate Professor at Coventry University.

The project employed full time Research Associate Dr Dorian Florescu.

Project Partners

The Project has four partners who have expressed interest in the outcomes for potential incorporation into their software. They have committed time, guidance, discussions and software licences to the project.

Related Publications

  • [FE20a]
    D. Florescu and M. England.
    Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness.
    Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '19), pp. 341-356, (Lecture Notes in Computer Science, 11989). Springer International Publishing, 2020.
    Digital Object Identifier: 10.1007/978-3-030-43120-4_27
    Preprint arXiv:1911.12672.
  • [FE20b]
    D. Florescu and M. England.
    A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs.
    Mathematical Software (Proc. ICMS '20), pp. 302-311, (Lecture Notes in Computer Science, 12097). Springer International Publishing, 2020.
    Digital Object Identifier: 10.1007/978-3-030-52200-1_30
    Preprint arXiv:2005.11251.
  • [FE19]
    D. Florescu and M. England.
    Algorithmically generating new algebraic features of polynomial systems for machine learning.
    Proceedings of the 4th Workshop on Satisfiability Checking and Symbolic Computation (SC2 '19), 12 pages. CEUR Workshop Proceedings 2460, 2019.
    Publication website. Final version (OA) pdf.
    Preprint arXiv:1906.01455.
  • [EF19]
    M. England and D. Florescu.
    Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition.
    In: C. Kaliszyk, E. Brady, A. Kohlhase and C.C. Sacerdoti eds., Intelligent Computer Mathematics (Proceedings of CICM 2019), pp. 93-108, (Lecture Notes in Computer Science, 11617). Springer International Publishing, 2019.
    Publication website. Digital Object Identifier: 10.1007/978-3-030-23250-4_7
    Preprint arXiv:1904.11061.
    Data supporting the paper is hosted by Zenodo: DOI:10.5281/zenodo.2658626
  • [HEWBDP19]
    Z. Huang, M. England, D.J. Wilson, J. Bridge, J.H. Davenport and L.C. Paulson
    Using Machine Learning to Improve Cylindrical Algebraic Decomposition.
    Mathematics in Computer Science, 13:4, pp. 461 - 488, Springer, 2019.
    Publication website. Digital Object Identifier: 10.1007/s11786-019-00394-8
    Final version (Gold OA) pdf.
    Preprint arXiv:1804.10520.
  • [England2018]
    M. England
    Machine Learning for Mathematical Software
    In: J.H. Davenport, M. Kauers, G. Labahn and J. Urban, eds. Mathematical Software - ICMS 2018, pp. 165-174. (Lecture Notes in Computer Science 10931). Springer, 2018.
    Publication website. Digital Object Identifier: doi:10.1007/978-3-319-96418-8_20
    Preprint arXiv:1806.10920.
  • [HEDP16]
    Z. Huang, M. England, J.H. Davenport and L.C. Paulson.
    Using Machine Learning to decide when to Precondition Cylindrical Algebraic Decomposition with Groebner Bases.
    Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC '16), pp. 45--52. IEEE, 2016.
    Publication website. Digital Object Identifier: doi:10.1109/SYNASC.2016.020
    Preprint arXiv:1608.04219 or University repository.
  • [HEWDPB14]
    Z. Huang, M. England, D. Wilson, J.H. Davenport, L.C. Paulson and J. 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, eds. Intelligent Computer Mathematics, pp. 92-107. (Lecture Notes in Artificial Intelligence, 8543). Springer Berlin Heidelberg, 2014.
    Publication website. Digital Object Identifier: doi:10.1007/978-3-319-08434-3_8
    Preprint: arXiv:1404.6369 or University repository.