Constrained Neural Networks for Interpretable Heuristic Creation to Optimise Computer Algebra Systems
Dorian Florescu, Matthew England
TL;DR
The paper addresses optimizing CAD variable ordering by constraining a neural network to replicate a human-designed heuristic (Brown's), enabling ante-hoc explainability in symbolic computation. It formalises Brown's three-metric heuristic as a two-layer NN with outputs $y_v=F^1(d_v)w^2+F^2(d_v)w+F^3(d_v)$ and shows the resulting ordering matches Brown's under suitable weights. Through feature-selection and weight-tuning on 3-variable polynomial datasets (including NLSAT tests), it identifies a superior, human-interpretable heuristic and achieves tangible CAD-time improvements (e.g., from $10{,}580$ s to $10{,}181$ s; later reductions to $9{,}908$ s after training). The work demonstrates a pathway to extract interpretable ML-driven heuristics in CAS with potential applicability to other symbolic algorithms and provides a framework for future mathematical insights derived from ML patterns.
Abstract
We present a new methodology for utilising machine learning technology in symbolic computation research. We explain how a well known human-designed heuristic to make the choice of variable ordering in cylindrical algebraic decomposition may be represented as a constrained neural network. This allows us to then use machine learning methods to further optimise the heuristic, leading to new networks of similar size, representing new heuristics of similar complexity as the original human-designed one. We present this as a form of ante-hoc explainability for use in computer algebra development.