Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
From MaRDI portal
Publication:6149145
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.
Cites work
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 1273640 (Why is no real title available?)
- scientific article; zbMATH DE number 2145000 (Why is no real title available?)
- scientific article; zbMATH DE number 3078997 (Why is no real title available?)
- A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs
- Advancing mathematics by guiding human intuition with AI
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Code optimization in FORM
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Computing cylindrical algebraic decomposition via triangular decomposition
- Cylindrical algebraic decomposition using validated numerics
- Cylindrical algebraic decomposition with equational constraints
- Efficient projection orders for CAD
- Efficient subformula orders for real quantifier elimination of non-prenex formulas
- Fully incremental cylindrical algebraic decomposition
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Machine learning the real discriminant locus
- MetiTarski: past and future
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- On using Lazard's projection in CAD construction
- Open non-uniform cylindrical algebraic decompositions
- Optimising problem formulation for cylindrical algebraic decomposition
- Partial cylindrical algebraic decomposition for quantifier elimination
- Pattern recognition and machine learning.
- Real World Verification
- Real quantifier elimination is doubly exponential
- Scikit-learn: machine learning in Python
- Solving non-linear arithmetic
- Special issue on algebraic geometry and machine learning
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
- Using machine learning to improve cylindrical algebraic decomposition
- Validity proof of Lazard's method for CAD construction
- Variable ordering selection for cylindrical algebraic decomposition with artificial neural networks
Cited in
(8)- Bilinear-form and similarity-reduction visit to a variable-coefficient generalized dispersive water-wave system concerning Acta Mech. 233, 2527 and 233, 2415
- Constrained neural networks for interpretable heuristic creation to optimise computer algebra systems
- Exploring alternative machine learning models for variable ordering in cylindrical algebraic decomposition
- Symbolic integration algorithm selection with machine learning: LSTMs vs tree LSTMs
- Lessons on datasets and paradigms in machine learning for symbolic computation: a case study on CAD
- A dataset for suggesting variable orderings for cylindrical algebraic decompositions
- Algebraic representations for faster predictions in convolutional neural networks
- Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk)
This page was built for publication: Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149145)
