Algorithmically generating new algebraic features of polynomial systems for machine learning

Abstract

There are a variety of choices to be made in both computer algebra systems (CASs) and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness. Such choices are candidates for machine learning (ML) approaches, however, there are difficulties in applying standard ML techniques, such as the efficient identification of ML features from input data which is typically a polynomial system. Our focus is selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm implemented in several CASs, and now also SMT-solvers. We created a framework to describe all the previously identified ML features for the problem and then enumerated all options in this framework to automatically generation many more features. We validate the usefulness of these with an experiment which shows that an ML choice for CAD variable ordering is superior to those made by human created heuristics, and further improved with these additional features. We expect that this technique of feature generation could be useful for other choices related to CAD, or even choices for other algorithms with polynomial systems for input.

To appear in Proc SC-Square Workshop 2019. arXiv admin note: substantial text overlap with arXiv:1904.11061

References in corpus (8)

• Satisfiability Checking meets Symbolic Computation (Project Paper)
• A Case Study on the Parametric Occurrence of Multiple Steady States
• Improving the use of equational constraints in cylindrical algebraic decomposition
• Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting
• Using Machine Learning to Improve Cylindrical Algebraic Decomposition
• Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
• Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
• Machine Learning for Mathematical Software

Cited by in corpus (3)

• Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
• A machine learning based software pipeline to pick the variable ordering for algorithms with polynomial inputs
• Verified Quadratic Virtual Substitution for Real Arithmetic