Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transformers to Predict the Applicability of Symbolic Integration Routines

Rashid Barket, Uzma Shafiq, Matthew England, Juergen Gerhard

TL;DR

This work trains transformers that predict whether a particular integration method will be successful, and compares against the existing human-made heuristics that perform this task in a leading CAS to find the transformer can outperform these guards.

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.

Transformers to Predict the Applicability of Symbolic Integration Routines

TL;DR

This work trains transformers that predict whether a particular integration method will be successful, and compares against the existing human-made heuristics that perform this task in a leading CAS to find the transformer can outperform these guards.

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.

Paper Structure

This paper contains 13 sections, 1 theorem, 1 equation, 5 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Dataset
  3. Training Transformers to Predict Method Success
  4. Experiment Setup
  5. Results
  6. Layer Integrated Gradients to Interpret the Classifiers
  7. Conclusions
  8. Future Work
  9. Integration Methods and their Guards
  10. Data Generation and Preprocessing
  11. Generation Methods
  12. Data Preprocessing
  13. Model Architecture and Code

Key Result

Theorem 1

: Let $D$ be a differential field with constant field $K$ (whose algebraic closure is $L$). Suppose $f \in D$ and there exists $g$, elementary over $D$, such that $g'=f$. Then, $\exists \, v_0,\dots,v_m \in D, c_1,\dots,c_m \in L$ such that

Figures (5)

  • Figure 1: A high-level overview of how the indefinite integral command works in Maple to calculate $F(x) = \int f(x) dx$.
  • Figure 2: Frequency of each method being successful on 1.5M examples from six data generators.
  • Figure 3: Example sequence to depict the attribution scores corresponding to different tokens where blue is positive and red is negative. Note the strongly negative score for the abs token.
  • Figure 4: Aggregated attribution scores for all test samples containing the abs token for the Risch method. Note the abs token has a strongly negative score.
  • Figure 5: An example output from the indefinite integration command when all the methods are called. Some answers have a different form but are all mathematically equivalent.

Theorems & Definitions (1)

  • Theorem 1: Liouville's theorem