AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs

Authors: Mert Unsal, Timon Gehr, Martin Vechev
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
Keywords: symbolic, math, integration, neurosymbolic, transformer, proof, search, symbolic engine

Abstract:
We present the first correct-by-construction learning-based system for step-by-step mathematical integration. The key idea is to learn a policy, represented by a GPT transformer model, which guides the search for the right mathematical integration rule, to be carried out by a symbolic solver. Concretely, we introduce a symbolic engine with axiomatically correct actions on mathematical expressions, as well as the first dataset for step-by-step integration. Our GPT-style transformer model, trained on this synthetic data, demonstrates strong generalization by surpassing its own data generator in accuracy and efficiency, using 50\% fewer search steps. Our experimental results with SoTA LLMs also demonstrate that the standard approach of fine-tuning LLMs on a set of question-answer pairs is insufficient for solving this mathematical task. This motivates the importance of discovering creative methods for combining LLMs with symbolic reasoning engines, of which our work is an instance.

Decision: reject
Reviewer scores: 5, 5, 3, 6

Reviews and discussion:
<thread>
creation date:
1730286736333

thread_type:
official_review

<thread_object>
creator: reviewer_qbvw

<content>
summary:
This paper presents a novel mathematical integration system that fuses neural models with symbolic solvers. In this approach, a GPT transformer model guides the selection of the appropriate integration rule, while a symbolic solver executes the precise calculations. To fine-tune the language models, the authors propose augmenting seed data to create a large-scale dataset of step-by-step integration. The experimental results demonstrate the proposed method's efficiency and comprehensiveness.

strengths:
- Although the high-level insight is inspired by AlphaGeometry and AlphaProof, the application task and designed framework are very interesting and innovative.
- The authors provide the implementation of the proposed methods, offering valuable resources to the research community.
- The experimental results are promising, demonstrating that the proposed method significantly outperforms the baseline approaches.
- The differentiation analysis between the symbolic solvers and the proposed system could be useful for identifying bugs or limitations in existing heuristics.

weaknesses:
- I am struggling to understand the practical motivation behind the research problem. First, the authors use SymPy as an example, which is notably inefficient compared with other symbolic tools. Second, I cannot see the necessity of employing an LLM is unclear, especially considering the model size is very small and the possible action space is well-defined and finite.
- The paper lacks comparisons with additional baselines. Although the proposed method is open-sourced, it would be helpful to include comparisons with proprietary systems, such as Wolfram's integral calculator, to serve as a point of reference.

questions:
- The authors mention that SymPy's *manualintegrate* is slow and prone to failure. Could this be more of an implementation issue rather than an algorithmic one? For example, the SymPy is implemented fully on Python, causing low calculation efficiency.
- I am also curious about the time consumption. What is the average runtime for SymPy and the fine-tuned model on the test set? Additionally, is the model inference performed on CPUs?
- The data contamination problem should be further discussed. With the generation of approximately 45 million data points, there is a potential risk of overlap between training and testing datasets. Could the generated data lead to contamination issues, and how can these risks be mitigated during data generation?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730578429036

thread_type:
official_review

<thread_object>
creator: reviewer_zjwe

<content>
summary:
This paper introduced AlphaIntegerator which trains a decoder-only transformer model to perform step-by-step integration. The expression to be integrated is represented by a mathematical expression tree and converted to a sequence in a depth-first manner. The model is then trained to predict single-step rules to be applied to the expression. Trained and evaluated on a synthetic dataset, the paper finds that AlphaIntegerator outperforms sympy and GPT-4o-mini.

strengths:
The paper is clearly written and easy to follow. 

The paper implements a learning approach to perform step-by-step integration.

weaknesses:
The model’s ability for generalization could be limited, since the operators, variables, and actions are all represented as special tokens, and it doesnt seem like new operators, variables, or actions can be easily introduced without re-training the model. The model also currently only include 7 symbols to represent variables, which suggests that it cannot generalize to harder problems from the same distribution with more variables.

The experiments conducted are not extensive. Only the synthetic dataset is used and only 2 other methods are compared. Furthermore, the proposed method’s improvement from existing methods is not substantial (83.3% -> 87.3% accuracy).

Part of the synthetic data generation process is augmenting the dataset based on integration by parts, which later is shown to be a failure mode for the sympy solver. The comparison on the synthetic data may therefore favor the proposed model over sympy.

The motivation for this method is unclear to me. The paper states that it aims to “combine LLMs with symbolic reasoning engine”, but the model implemented is a 6-layer transformer trained from scratch.

questions:
What were the design decisions behind including 7 symbols for variables? How easy is it for the model to handle more complex integration problems?

The model is required to generate subexpressions for integration, is the subexpression generated always valid? Is it being enforced?

Did you consider other methods for representing the expression other than using an expression tree + DFS? The transformer takes a sequence as input, can’t it handle the mathematical expression directly? (for example, INT+ 3 + x instead of + INT+ 3 x)

How does your work relate to existing work such as [1] combining symbolic solvers and LLMs?

Minor Comment:
The example in section 3.2 is a bit confusing to me, what does * INT+ 2 refer to in the expression? 

[1] Pan, Liangming, et al. "Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning.”
</content>
</thread_object>

</thread>
<thread>
creation date:
1730713396545

thread_type:
official_review

<thread_object>
creator: reviewer_jvis

<content>
summary:
This paper introduces a correct-by-construction learning-based system for step-by-step mathematical integration. Concretely. LLMs interact with a symbolic engine with a set of handcraft rules. This paper also contributes a dataset for rigorous step-by-step derivation proofs for indefinite integration. The proposed model is trained and tested on the synthesized dataset and compared with two baselines, SymPy and GPT-4o-mini.

strengths:
* The paper introduces a new approach to integrating LLMs with symbolic reasoning engines for mathematical integration.
* The paper is clearly written and easy to follow.

weaknesses:
Please see the questions below.

questions:
* The representation of mathematical expressions and theorems are trees consisting of operands/functions with fixed arities. For example, addition and multiplication only have two children. Therefore, the proposed method seems challenging to extend to general situations. 
* The data synthesis results in 4.9 expressions. What is the diversity of the synthetic expressions? Are there specific types of expressions that are underrepresented in the training data, and how might this affect the model's performance?
* While the paper compares AlphaIntegrator with SymPy and GPT-4o-mini, it would be informative to see a comparison with other state-of-the-art symbolic solvers or theorem provers. 
* Are there specific types of integrals or mathematical expressions where AlphaIntegrator excels or falls short compared to these tools?
* How does AlphaIntegrator perform on open-source math datasets? 
* The listed references are not formal. For example, 'Deep Learning For Symbolic Mathematics' has already been published in ICLR, but the citation is still CoRR.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730720742340

thread_type:
official_review

<thread_object>
creator: reviewer_1ca8

<content>
summary:
The paper presents AlphaIntegrator -- a learning-based system for computing antiderivatives of mathematical expressions in a step-by-step manner. The system is a hybrid of a symbolic engine checking for correctness of each step, predefined symbolic "actions", and a transformer-based policy pretrained on a sizable set of synthetic examples. 

The authors evaluate their system on a synthetic dataset and show its superiority compared to the symbolic approach implemented in SymPy, as well as GPT-4o-mini model.

strengths:
1. The paper tackles an important and interesting problem of synergizing learning-based and formal/symbolic methods.
2. AlphaIntegrator is shown to perform better that GPT-4o-mini and SymPy. Additionally, it is demonstrated that AlphaIntegrator is less "symbolically brittle" than the approach by Lample and Charton (2019) computing antiderivatives directly.
3. As a byproduct of the project, the authors contributed a few fixes to SymPy's integration algorithm. 
4. The paper is very clearly written, providing enough background and helpful examples.
5. The authors provide the code for reproducing the experiments (the code looks runnable, although I didn't test it.).

weaknesses:
1. There is no comparison of AlphaIntegrator with the approach by Lample and Charton (2019). I find it a serious omission. 
2. There is no comparison of AlphaIntegrator with the integration algorithm in Mathematica (which, I think, is stronger than this implemented in SymPy).
3. The achieved improvement is rather small compared to SymPy's performance.
4. The proposed approach is not super novel: there is already quite a large body of research dealing with ML-based formal theorem proving, where the setting is similar as in AlphaIntegrator: an ML model suggests actions (proof steps, aka "tactics") constrained by the formal/symbolic environment. 
5. The target problem -- integration -- seems somewhat not very well suited for that kind of approach. I suppose that the purely symbolic approaches deal with most of the integration problems efficiently. Moreover, it is not crucial to have a step-by-step derivation of the antiderivative: once we have a antiderivative, verifying its correctness is easy, and step-by-step solution is irrelevant. 
6. The authors claim that their approach can be adapted to other kinds of math problems, but I find this claim unjustified. 
7. The authors did not release the test dataset, which makes it more difficult to compare with AlphaIntegrator in the future. (Or did you release? I'm not sure here.)
8. The authors instantiate the learning component of AlphaIntegrator with a transformer model, and do not test any other ML approaches.

questions:
1. Am I right that you input the expressions to the transformer using prefix Polish notation? Why did you prefer this notation over the standard one? Did you run an experiment justifying this choice?
2. Did you generate the synthetic dataset yourself or reused the one provided by Lample and Charton (2019)? You mention that you generate it in line 193, but in the provided code I see you download the data of Lample and Charton.
3. Where do the predefined actions come from? Did you experiment with different sets of actions?
4. Did you experiment with other types of tree search? For instance, breadth-first search instead of best-first search induced by the log-probs?
5. To what extent the set of solutions by AlphaIntegrator overlaps with the solutions by SymPy?
6. Do you think TreeNN architectures would be better suitable as the learning component of AlphaIntegrator? Or maybe even simpler ML approaches or heuristics would be applicable given the predefined list of actions? (Like k-NN?)
7. You write "We run SymPy and our own model with timeouts of 120 and 10 seconds, respectively." Why different timeouts? Is that correct that SymPy got more time than AlphaIntegrator?
8. How and to what other math problems can AlphaIntegrator be adapted?
8. How did you split the data into training and testing parts? Could you release both datasets for inspection?
</content>
</thread_object>

</thread>
<thread>
creation date:
1732100008823

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
General Response

comment:
Dear reviewers, 

We greatly appreciate all of your feedback. As there are a lot of overlapping questions, we decided to reply to all in this comment. 

1. We did not explicitly compare with Lample and Charton (2019) as it does not provide steps to solve the integral but only the antiderivative itself. The focus our work is *step-by-step* integration, as this generalizes well beyond finding the antiderivative. In fact, you can only do the antiderivative check for single variable integrals: multivariable integrals over complex domains require step by step solution. 

2. Some reviewers claim that improvement is minimal, however we disagree that %4 improvement is small, given that the model was trained on synthetic data generated by SymPy. 

3. Symbolic approaches indeed work quite well on the task of finding the antivderivative. - however they rarely give step by step solutions which is important in many cases. To give a concrete example, a similar methodology can be applied to solving multidimensional integrals where the domain is non-standard or rewriting inequalities in a desired way. This is a great example on how our model can be extended to different problems as well.

4. For the test dataset, we used the same one from Lample and Charton to ease up comparisions. For the dataset of random expressions, we used the dataset generated by Lample and Charton, however, we generated the data for the step by step solutions. This datasets can be found on the GitHub page of the Lample and Charton paper: https://github.com/facebookresearch/SymbolicMathematics 

5. Our first experiments indicated that the Polish notation indeed makes training easier for our tasks which is why we decided to stick with it. 

6. There is a lot of freedom around how one can choose actions for such a system: we used 2 criterion to design the action space. First, it had to be comprehensive enough to cover a wide range of integrals. Second, it had to be suitable for converting the steps generated by SymPy. 

7. We did not have time to try different search methods, but we believe that our results could only further improve with better search methods - we will work on such improvements in the next steps of the project.

8. We ran SymPy with a longer timeout to make sure that we get its saturated performance that is not affected by the slow execution time of Python.

We hope this answers your questions and we're looking forward to your further feedback.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732707083775

thread_type:
official_comment

<thread_object>
creator: authors

<content>
comment:
We thank the reviewers again for their initial feedback. As we have not yet received replies to our rebuttal and the discussion period is closing shortly, we would like to kindly ask the reviewers to let us know if our responses addressed their concerns, and raise any follow-up questions.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper presents, AlphaIntegrator, which is a decoder-only transformer model trained to predict stepwise integration rules for computing antiderivatives of mathematical expressions. Groundtruth integration rules are collected by running SymPy over a synthetic dataset collected by the previous work Lample and Charton (2019). The experimental evaluation shows that AlphaIntegrator (combined with a symbolic engine) outperforms the baseline SymPy and GPT-4o-mini. 

The general idea of using a language model to guide the search of an underlying symbolic engine is not new, but the specific application to math expression integration is new. The main concerns shared by reviewers and the AC are twofolds: a limited experimental evaluation setup and several unjustified claims. The authors emphasize that the new approach gives step-by-step integration rules which are further validated by the underlying symbolic engine, while many existing approach does not, which is indeed a nice property (or byproduct) of the proposed approach (or more broadly any ML-guided theorem proving approaches). However, simply excluding important baselines like the previous work Lample and Charton (2019) is problematic. Applying the same criteria, GPT-4o-mini should be excluded as well. Secondly, whether Polish notation is superior to other representations is vaguely hinted but not backed up with quantitative results. Other claims like dataset generation (line 193) turn out to be factually false.