Transformers to Predict the Applicability of Symbolic Integration Routines

Authors: rashid  barket
uzma  shafiq
matthew  england
jürgen  gerhard
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-25 21:58:24

Abstract: Symbolic integration is a fundamental problem in mathematics: we consider how machine learning may be used to optimise this task in a Computer Algebra System (CAS). We train transformers that predict whether a particular integration method will be successful, and compare against the existing human-made heuristics (called guards) that perform this task in a leading CAS. We find the transformer can outperform these guards, gaining up to 30\% accuracy and 70\% precision. We further show that the inference time of the transformer is inconsequential which shows that it is well-suited to include as a guard in a CAS. Furthermore, we use Layer Integrated Gradients to interpret the decisions that the transformer is making. If guided by a subject-matter expert, the technique can explain some of the predictions based on the input tokens, which can lead to further optimisations.

Main paper: 
 introduction: 
 Symbolic integration is well-studied, proven to be undecidable (see e.g. discussion in Chapter 22 in Gerhard and Von zur Gathen [2013] ). The most widely applicable method is the Risch algorithm (Risch [1969] ). However, the original algorithm does not work with special functions, and implementations of this algorithm has trouble with algebraic extensions. It is also complicated, taking more than 100 pages to explain in (Geddes et al. [1992] ): no Computer Algebra System (CAS) has a full implementation. Hence, researchers in CA have designed a variety of other symbolic implementation methods.More recently have there been attempts to use Machine Learning (ML) to perform symbolic integration. First, Lample and Charton [2020] implemented a transformer to directly integrate an integrand, outperforming several mature CASs on the generated test data. Further attempts have been made using LLMs (Noorbakhsh et al. [2021] ), and by chaining explainable rules (Sharma et al. [2023] ). More generally, there has been work developing a single LLM to perform a variety of mathematical reasoning tasks including (in)definite integration such as (Drori et al. [2022] , Hendrycks et al. [2021] ).We are interested in improving the efficiency of indefinite integration within a CAS using ML, while still ensuring that correctness of the answer is guaranteed, through ML-based optimisation and algorithm selection. Recent work applied TreeLSTMs to show there is room for significant performance improvements (Barket et al. [2024a] ). We focus on the popular commercial CAS, Maple. Maple's user-level integration call is essentially a meta-algorithm: it can employ several different methods for symbolic integration. They are currently tried in a deterministic order until one succeeds, at which point the answer is returned without trying the other methods. A key part of this Figure 1 : A high-level overview of how the indefinite integral command works in Maple to calculateF (x) = f (x)dx.implementation is what we call the guards: code that is run prior to calling one of the methods to decide whether or not attempting to use the method is worthwhile. The reasoning behind having a guard is that some of the methods are computationally expensive: it is a waste of time to go through a complex algorithm just to find out that it fails. Figure 1 gives a high-level overview of this idea.Not all methods have a guard, and some guards do partial work for the method making them expensive for a quick check. Appendix A gives a list of methods and their guard (should they exist). We create small ML models to predict success for methods and investigate whether these can provide guards for methods that lack them, or replace the computationally expensive guards (provided they do better). We also investigate whether interpretations of these models might inform further guard development. 
dataset: 
 Our dataset is composed of integrable expressions in their prefix notation. The data comes from six different data generators: the FWD, BWD, and IBP generators from Lample and Charton [2020] ; the RISCH generation method from Barket et al. [2023] ; the SUB generation method from Barket et al. [2024a] ; and the LIOUVILLE generation method from Barket et al. [2024b] . For more information see Appendix B.1. We obtain the labels for each integrand by recording which methods succeed (1) and which fail (0) for each expression. We note that this labelling is considerably more computationally expensive than the ML training later. The data is stored as a list where, for position i in the list, the value records if method i is a success or failure.The data goes through several pre-processing steps to shrink the vocabulary size and to avoid having expressions of similar form over-represented in the dataset, as described in Appendix B.2. In total, there are 1.5M and 60K samples for training and testing respectively, with an equal split from each data generator. The labels do not occur equally however: some methods have a much higher rate of success than others. This is because some of the methods are only made for certain types of integrands (e.g. Elliptic) whereas others are more general-purpose (e.g. Risch). Figure 2 shows the frequency of integrating successfully over the train set from each method. 3 Training Transformers to Predict Method Success 
experiment setup: 
 For each of the methods in Maple 2024, we train a classifier to determine whether it is worthwhile attempting said method. We use an encoder-only transformer Vaswani et al. [2017] to predict success or failure, with architecture similar to Lample and Charton [2020] and Sharma et al. [2023] .Hyper-parameters and the full model architecture are discussed in Appendix C. The results are then compared to the guards implemented by human experts in Maple. In this scenario, a false positive is considered worse than a false negative. This is because trying a method and failing wastes compute time, whereas skipping an algorithm that may succeed may be okay because another method could possibly succeed (and if none do, we could always then try the guarded ones at the end). Thus, we evaluate accuracy and precision when comparing each transformer to each guard.Table 1 shows the results for methods that do not have a guard. In this case, the transformers are compared to a hypothetical guard that simply predicts a positive label every time, since the current workflow would always attempt such methods. These transformers range in accuracy from 93% to 98%. Hence, there is much scope for using ML to prevent wasteful computation. An example of such a case is for Risch and Norman: both have an operation, Field, that creates the base field along with its field extensions before proceeding with the algorithm. This operation takes nearly 20% of their runtime before determining whether to run the rest of the algorithm or output fail. On a batch of 1024 examples, the mean transformer runtime was only 0.0895s compared to Field which took 0.125s (39.7% longer). In such a case, the transformers can help save computation time before performing the Field operation.Table 2 shows the results for the methods that do already have a guard. In each of these cases, we see that a transformer can beat the guards, and some by a margin of over 30%. We note that the guards for Trager and PseudoElliptic are particularly weak compared to the transformers, with much lower accuracy and precision. The transformers can avoid the false positives that the guards cannot.The number of positive samples for PseudoElliptic is scarce and future work may include an anomaly detection approach for this method. A caveat is that the inference time of the transformers is higher than the existing guards. As mentioned above, the transformers took 8.95e-2s on average per sample whereas Trager, MeijerG, PseudoElliptic, and Gosper took 1.1e-6, 1.4e-6, 4.7e-7, and 4.7e-7s respectively. The transformers take magnitudes longer to complete inference. However, we hypothesize that the huge gains in precision over these guards will help prevent a lot of wasteful computation and so overall, Maple's integration algorithm would save time, to be confirmed in future work.Some guards are known to be perfect at predicting incorrectness: i.e. if such a guard outputs that a method will not work, then it is a mathematical proof that it will never succeed. Although such guards will always predict the true negatives correctly, they may make mistakes on the true positives. Table 3 reports performance after we filter the data with such guards, by removing the samples the guard finds negative (the first two have a similar guard which caused them to have the same filtered dataset). Note that because these guards are perfect at predicting the negative target class, their accuracy and precision in Table 3 are exactly that of the precision on the full dataset in Table 2 . We see that, unlike the guards, the transformers have good performance on both classes. 
layer integrated gradients to interpret the classifiers: 
 We have seen that ML can optimise the work of CASs here, but we are also interested in how the ML models make their decisions: both to give confidence in their results and perhaps to inform better hard-coded guards. This proved to be the case when SHAP values were used to explain the predictions of traditional ML models optimising Cylindrical Algebraic Decomposition (Pickering et al. [2024] ). However, transformers are most widely used in Math-AI Zhou et al. [2024] , Sharma et al. [2023] , Charton [2024] and their explanation remains a challenge. Sharma et al. [2023] proposed an explainable approach for symbolic integration: computing integrals by applying rules step-by-step to form a chain from input to output. However, while this explains how the integral may be computed, it does not explain the decisions the transformers make to select these rules.We further experiment with interpreting the transformers using Layered Integrated Gradients (LIGs) Sundararajan et al. [2017] ; an extension of Integrated Gradients that gives insight into different layers of a neural network. We used LIGs with the embedding layer of our model to compute the attribution score of each input token as the embedding layer converts the input tokens into a dense vector space. We used 50 steps and the default baseline as described in Kokhlikyan et al. [2020] .One interesting observation concerns the Risch method and the attribution scores found for the token of the absolute value function (abs). These always contribute negatively, usually highly so, in the observed samples which indicates that the presence of this token will adversely impact the prediction for use of this method. A visualisation for a particular example is shown in Figure 3 .After discussing with domain experts, we find this a satisfying interpretation: the Risch algorithm is suited for elementary functions and the absolute value function does not fall in this category. In fact, the Risch algorithm is not proven to work when the absolute value function is included in the field defined in the algorithm (Gerhard and Von zur Gathen [2013] ). Note this explanation also suggests a simple edit to improve the existing guard code!The attribution scores for all the samples were calculated and aggregated to plot the graph in Figure 4 . It can be observed that the attribution scores for abs are the most negative, further demonstrating the alignment of the interpretation and the human expert. Of course, this is just one observation for a single method and domain expertise remains crucial for validating the insight. But it points to potential for further progress through XAI tools.  
conclusions: 
 In summary, we have demonstrated how we may improve the symbolic integration function in Maple without risking its mathematical correctness, by using transformers to predict when an integration method in Maple will succeed. The transformers were compared to heuristics crafted by domain experts: Table 1 shows that when a heuristic does not exist, a transformer is a suitable guard at predicting success, achieving between 93-98% accuracy. For the four methods that do have a guard, we also show that transformers make better predictions than these guards. In some cases, accuracy and precision increase significantly compared to the guards, over 30% and 70% respectively.The models, specifically the embedding layers, were then analysed using LIGs to try to interpret the models. We demonstrated that this approach can give a satisfying explanation for some predictions (the presence of the abs token being heavily associated with a negative label for the Risch method) although we note that domain knowledge is needed to understand why LIGs produce this result. This explanation in turn suggests improvements to the human-designed guards.We have shown the potential for ML optimisation of the Maple integration meta-algorithm. As next steps we will embed the transformers and evaluate the savings: measured both in number of methods tried (by trying them in order of probability of success) and in overall CPU time.The existence of some perfect guards suggests there is scope for a hybrid approach between algebraic tools and transformers which we will also explore in future work. After that, we will seek to implement our best approach into the actual workflow of Maple's symbolic integration algorithm. We would then be able to empirically measure how much time is saved in the algorithm rather than analysing each method individually.We will also continue to experiment with XAI tools to see if the transformers are learning the same rules as the integration method it is learning about, inspired by the insight observed above. The LIGs only offered explanations at a token level and most likely we need a tool that can also analyse the presence and prevalence of sequence and groups of tokens. While LIGs provided us with some insight, there was a need for a domain expert to validate this, and that is likely to remain the case.Finally, we note again that in similar applications such as Pickering et al. [2024] and Coates et al. [2023] , the authors were able to discover new interpretable heuristics based on the observations from the ML models. Being able to understand the predictions is interesting, but the ultimate goal would be to discover new interpretable heuristics for the methods that do not have a guard using XAI tools. This can give better insight on how we understand symbolic integration as a whole and discover new mathematical properties associated with these methods.• They have a hard time generating integrands of certain forms (see Barket et al. [2024b] for more on this point).Prior work by the authors creates several different generators to help address such issues based on mathematical properties of integrands. Liouville is the first to have described the general form of an elementary integral if it exists. Two of the generators are based on the work of Liouville so we first state Liouville's theorem (Section 12.4 in Geddes et al. [1992] ) for symbolic integration.Theorem 1 (Liouville's theorem) : Let D be a differential field with constant field K (whose algebraic closure is L). Suppose f ∈ D and there exists g, elementary over D, such that g′ = f . Then, ∃ v 0 , . . . , v m ∈ D, c 1 , . . . , c m ∈ L such that f = v ′ 0 + m i=1 c i v ′ i v i =⇒ g = v 0 + m i=1 c i log(v i ).The two generators based on Liouville's theorem are:• RISCH: (Barket et al. [2023] ) Reverse engineer the steps of the Risch algorithm, whose correctness is underpinned by Liouville's Theorem, which outputs the integral of a given input. We generate an expression f = R b such that b is a fixed expression and R are represented as symbolic coefficients. We then follow the steps of the Risch algorithm to determine what values these symbolic coefficients can be in order to satisfy integrability. This guarantees f is integrable and the Risch algorithm outputs the integral of f .• LIOUVILLE: (Barket et al. [2024b] ) Similar to the BWD method but follows the form of Liouville's theorem. Generate a random rational expression N D and also generate two sums of logarithms A = Finally, similar to IBP, we also have one more data generator based on the substitution rule from calculus and an existing dataset.• SUB: (Barket et al. [2024a] ) Given f and g, calculate g ′ and let u = g(x). If f is already known, then the following holds (substitution rule): f (g(x))g ′ (x)dx = f (u)du. We add (f (u), f (u)) to our dataset. 
 
 Appendix: The data preprocessing steps are primarily the same as described in Barket et al. [2024a] and we list them here for ease of access.Each number is preceded by an INT+ or INT-token to denote whether the integer being encoded is positive or negative. Then, we replace the actual numbers in the following manner:1. if the number is 0, 1or2, then create a corresponding token;2. if the number is a single-digit number that is not 0, 1or2, replace the number with a CONST token;3. if the number has two digits, replace by a CONST2 token; and 4. for all other cases, replace by a CONST3 token.As this is a classification task, the value of the constant does not (usually) matter and this helps simplify the data without losing much information. We keep the integers in the range [-2, 2] as they can end up being important (e.g. (x + 1) 1 and (x + 1) -1 integrate very differently). If any integrands match after this transformation, we only keep one unique copy to ensure a variety of expressions in the data. Lastly, we follow Devlin et al. [2019] and include a [CLS] token at the start of every sequence as a representation of the entire sequence. The output of this token after going through the encoding layers is used for the classification task. 



Reviews: review: title: title: Review
main_review: main_review: Strengths:
* Demonstrates an interesting application of transformers, i.e., to predicting the applicability of symbolic integration routines
* Successfully demonstrates it outperforms human-engineered heuristics

Weaknesses:
* Evaluation can benefit from more complete reporting (see suggestions below)
* Lack of evaluation in the context of the extra cost incurred by running the Transformer guard vs. the original guard. Lack of evaluation of total savings of solving actual integration problems due to the Transformer guard (although it’s said that this is future work).

Questions:
* Line 9: “Symbolic integration is well-studied, proven to be #P-complete (Kawamura [2011]).” The reference seems to be about numerical integration and makes no mention about symbolic integration? Also, it is unclear to me how symbolic integration can be formulated as a counting problem, a prerequisite for talking about whether a problem is #P-complete.
* Why is atan missing in Figure 4?

Suggestions:
* Line 23: “Barket et al. [2024a]” -> “(Barket et al. [2024a])”
* In Table 1, for the methods that don’t have guards, I recommend comparing with the “trivial” baseline guard that just always says yes (which is effectively what happens for methods without guards in Maple). Otherwise it is difficult to argue that having the transformer guard in these cases would be helpful at all vs. simply not having a guard.
* Although you argued precision is more important than recall, I think it would still be helpful to report recall to give the reader a more comprehensive picture. For example, you say in the text that some guards have perfect recall—it would be helpful to see that in the table.
Writing in Section 4 can be improved. Some citations in Section 4 lack parentheses and there are typos and grammatical mistakes.
* It may be helpful to explain a bit of background on LIGs in Section 4 (or at least refer to an appendix that provides more background on it)
title: title: The paper is overall well-written and the main ideas are clearly explained.
main_review: main_review: Paper Summary:
This paper considers how machine learning may be used to optimize this task in a Computer Algebra System. The authods train a transformer that predicts whether particular integration methods will be successful, compare the existing human-made heuristics, and find the transformer can outperform these methods.

Weakness and Strength:

(+) The paper is well-structured and clearly presents the problem, methodology, and findings. 

(+) This paper studies an interesting and well-motivated research question: how machine learning may be used to optimise this task in a Computer Algebra System (CAS).

(-) It would be beneficial to briefly highlight the implications of your findings. For example, explain how the ability of the transformer to outperform existing guards impacts the field of symbolic integration or CAS.
title: title: This paper explores the use of a transformer model to optimize symbolic integration within Computer Algebra Systems (CAS), and outperforms the established heuristics (guards) in Maple, suggesting a potentially more efficient method for symbolic computations.
main_review: main_review: This paper explores the use of a transformer model to optimize symbolic integration within Computer Algebra Systems (CAS), particularly by training the model to predict the success of various integration methods, comparing its performance against traditional human-made heuristics ("guards") in Maple. The transformer model outperforms these established heuristics, suggesting a shift towards machine learning-driven strategies in automating symbolic computations.

Pros:
1. A very valuable effort to implement transformer network on predicting whether a integration method is worthy to use.

2. A large dataset of integrable expressions is provided, which will benefit for ML on symbolic integration.

Cons:
1. More novel contributions should be emphasized in this work.

2. As the author said in the section of future work, more extensive and complete experiments should be performed to further investigate the advantages.
title: title: Review for Submission75
main_review: main_review: Summary: Authors show that it's possible to train a ML model to predict which integration technique will be more powerful when a software tries to find an antiderivative for a function $f$.

Strength:
- This method can help software to decide which integration technique to use. 
- Results compared to Maple sound pretty strong.

Weakness:
- To me, it looks like the bulk of the work is on the data collection which comes from prior work and it's not novel at all. 
- There is very little understanding on how the model make any decision. It's clear that abs plays a role, but there is no additional explanation after this and this would be interesting from the interpretability point of view.
- There is little explanation apart from results.