Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition
arXiv:2304.12154 · doi:10.1016/j.jsc.2023.102276
Abstract
In recent years there has been increased use of machine learning (ML) techniques within mathematics, including symbolic computation where it may be applied safely to optimise or select algorithms. This paper explores whether using explainable AI (XAI) techniques on such ML models can offer new insight for symbolic computation, inspiring new implementations within computer algebra systems that do not directly call upon AI tools. We present a case study on the use of ML to select the variable ordering for cylindrical algebraic decomposition. It has already been demonstrated that ML can make the choice well, but here we show how the SHAP tool for explainability can be used to inform new heuristics of a size and complexity similar to those human-designed heuristics currently commonly used in symbolic computation.
arXiv comment40 pages
References in corpus (8)
- Scikit-learn: Machine Learning in Python
- Stop ordering machine learning algorithms by their explainability! A user-centered investigation of performance and explainability
- Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks
- Cylindrical Algebraic Decomposition with Equational Constraints
- Using Machine Learning to Improve Cylindrical Algebraic Decomposition
- Understanding the Learners' Actions when using Mathematics Learning Tools
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Data Augmentation for Mathematical Objects
Cited by in corpus (4)
- Lessons on Datasets and Paradigms in Machine Learning for Symbolic Computation: A Case Study on CAD
- Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
- Understanding Multistationarity of Fully Open Reaction Networks
- Faster Gröbner bases for Lie derivatives of ODE systems via monomial orderings