AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs

Thank you for your review.

W1: The practical motivation of this paper is to improve existing open-source baselines on step by step theorem proving, and SymPy is the best existing alternative out there. The reason to use LLMs is that, on the contrary to your comment, action space is not finite. The model needs to pick exactly what subexpression to apply the action. In addition, the model needs to pick action parameters whenever it wants to apply the substitution rule or integration by parts. As the space of mathematical expressions is infinite, our action space is infinite.

W2: Since Mathematica is closed-sourced, we found it difficult to make experiments at scale (with thousands of expressions) which is what we need to obtain an accurate number.

Q1: As explained, the SymPy's algorithm works in a brute force manner, as you can see from the source code here: https://github.com/sympy/sympy/blob/master/sympy/integrals/manualintegrate.py

Q2: We took data contamination seriously and made sure that integration steps that appear in the training set do not appear in the test set. However, integration is a problem that you can inherently just overfit as it is an algorithmic task (i.e. if the model discovered an almighty algorithm to integrate, it would be overfitting to the entire set of expressions in a way).

We would be happy to answer if you have further questions.

Dear Reviewer,

Thank you for your comments.

1. We believe you misunderstand what we mean by allowing 7 variables: these variables are used for applying the substitution rule such as u = sqrt(x^2 +1). We just had to set an upper limit as a token needs to be initialized for each such variable - this doesn't have anything to do with the capabilities of the model.

2. The generated subexpressions were almost always valid, but it is not necessary that this will be the case. We discard the proposed action whenever the subexpression is invalid.

3. Note that the proposed Polish notation is just another way of writing mathematical expression: representing expressions this way removes the redundancy due to parentheses. For example, the infix expression (3 + 4) * (5 - 2) can be written in Polish notation as * + 3 4 - 5 2, eliminating the need for parentheses and reducing token usage.

4. Regarding the example in Section 3.2, * INT+ 2 alone doesn't mean anything - you should rather look at it as * (param 1) (param 2) which represents multiplication of param1 and param2. In this case, we have * INT+ 2 POW cosh x INT+ 2 x which represents 2 * cosh^2(x).

We don't really understand how training a 6-layer transformer from scratch is not compatible with the goal of "combining LLMs with symbolic reasoning engine." Note that the model we trained is a large language model - it doesn't have to be the case that it is pretrained or outputs natural language.

We also see that you gave score of 1 for Soundness and 2 for Presentation but didn't have any comments on what are the problems with soundness and how the presentation could be improved. We would be happy to see your feedback so that we can improve our paper.

We are happy to address the questions:

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

2. Synthetic dataset generation: Thank you for pointing out this discrepancy! We indeed used the data of Lample and Charton (2019) directly and we will make this clear in the next version of the paper.

3. Predefined actions: There is a lot of freedom around how one can choose actions for such a system: we used two critera 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. We did not experiment with another action space than the one that we present in the paper.

4. Comparison to other types of tree search: The SymPy baseline uses a different type of tree search without log-probabilities and expores more nodes while solving fewer integrals. One might indeed also consider what happens when one uses a non-guided search method with actions generated from the model, but it appears that would be strictly worse than the SymPy baseline, so we had not considered such an experiment. In general, experimenting with different types of tree search is an interesting direction for future work.

5. AlphaIntegrator vs SymPy overlap: For integration problems solved by both approaches, there is ~98% overlap in actions taken. We will add this statistic to the paper.

6. TreeNNs: Maybe. We have not tried this so far, but it would be an interesting comparison to make. However, our approach is more flexible and we demonstrated that it works well even though we did not make any specific accommodations for the structure of the input data. Simpler ML heuristics, like k-NN: That is an interesting suggestion for a baseline. However, it is not so clear to us how to make k-NN work in our setting. E.g., how to compute distances between integration states? It seems that ranking all the applicable actions that are present in the training dataset is itself a tricky problem, and even just testing all of those actions for applicability in each step does not seem feasible.

7. Higher SymPy timeouts: Yes, it is correct that the SymPy baseline timeout was significantly higher. This is to make up for the inefficient implementation of SymPy, as our goal was to show that SymPy cannot solve these integrals rather than to show that the Python interpreter is slow. We will increase the time limit also for our own approach and report a more quantitative analysis of the running times (e.g., a plot of integrals solved over time for the different approaches).

8. Adapting to other approaches: AlphaIntegrator demonstrates that our way of applying actions to subtrees is effective in this setting. The approach is in principle generalizable to any step-by-step reasoning task. However, significant effort is required to identify a suitable action space in those different contexts, particularly because we need to then be able to generate a data set that demonstrates how to effectively apply these actions. So while we think exploring other applications of the same kind of method is promising, we think such follow-up work would likely still require interesting research.

9. Training/test data: We used the original split from Lample and Charton (2019). In the interest of full transparency and reproducibility, we are happy to upload the final datasets derived from Lample and Charton that we used for training and testing.

Thank you for the detailed review.

Regarding the weaknesses pointed out by the reviewer:

1. Comparison to Lample and Charton (2019). This paper solves a different problem (we generate correct steps that may or may not lead to a full solution, they generate a possibly incorrect guess for the antiderivative). However, as we used the same datasets of integration problems, our numbers are directly comparable to the extent that that is meaningful.

2. Comparison to Mathematica: It is tricky to compare at scale to a baseline that is not open source. It seems more fruitful for Wolfram to eventually adopt an approach like ours to improve Mathematica. We would of course have done this instead if it were open, but it seems unfair to expect us to compete with a for-profit organization that is not bound by basic best practices for computer science research. We are however also curious and will see at what level such a comparison is possible (e.g. by subsampling the test set).

3. Only small improvement over SymPy: We disagree with this point. Given that all the training data stems from SymPy, which the model is instructed to imitate, we think that beating it by 4% while exploring only half of the search space on average, with fewer outliers, is an impressive result. We did not expect the model to outperform the training data.

4. Novelty: The main novel contribution is the specific action space, action encoding, implementation, and the evaluation. What we propose is certainly not a paradigm shift in symbolic reasoning, but we think it would be unreasonable to expect every publication that generates correct-by-construction results to deviate from the obvious "actions in symbolic environment" high-level setting in a non-trivial manner.

5. Integration steps not crucial to obtain final result, as it is easy to verify: Verifying the final result is an algorithmically undecidable problem, equivalent to the zero problem. We however agree that it is often easy in practice. The step-by-step approach is interesting when reasoning steps are actually important (it is not a coincidence that wolframalpha.org puts reasoning steps behind a paywall), and it enables more interesting applications down the line, such as non-trivial combination of multiple action spaces that operate on the same underlying representation. Also, AlphaIntegrator beats the open source symbolic step-by-step baseline by a respectable margin.

6. Adaptibility to other domains not justified. We make two references to adaptability. One is that transformer models are more versatile than TreeNN, which we think does not require additional justification. The other one is in future work, and therefore indeed speculative.

7. Test dataset not released: We released all code that is required to run our evaluation. However, that indeed does not include the specific test dataset as there is some randomness in how it is derived from Lample and Charton, due to shuffling. We did not run with a fixed seed. We will release the full training and test sets that we used in our evaluation, though we think the standard for reproducibility should be that new runs from scratch still produce results compatible with the mean and error margin reported in our paper.

Dear Reviewer,

We hope our general rebuttal answered most of your questions. We wanted to clarify a few more points specific to your questions as well:

1. Note that the only requirement is that an operation has "fixed" arity, but the same model is generalizable to expressions of any arity.

2. Existing theorem provers are usually unable to carry out this kind of computations to solve integrals, as they're more focused on mathematical theorem proving in fields such as number theory and algebra. Likewise, symbolic solvers do not necessarily output steps as we discussed in our general rebuttal.

3. In our evaluation, we find that AlphaIntegrator performs strictly better than the existing step by step solvers. However, solving integration step by step is not always possible, in which cases the model is unable to get to such solution.

4. Note that the integrals generated by are a lot more difficult than the standard textbook problems - our model is able to successfully solve most problems (>%95) in standard calculus textbooks. We promise to include more detailed analysis in the final version of the paper.

5. Thanks for this feedback - we will fix the citation in the final version.

We hope this clarifies your concerns and we kindly invite you to update your scores!

Thank you for the comment. I have some further questions:

You write

We did not explicitly compare with Lample and Charton

but also

For the test dataset, we used the same one from Lample and Charton to ease up comparisions.

So why didn't you show and discuss the comparison with Lample and Charton in the paper when your setup was designed to facilitate such a comparison? I understand that your method has the advantage of providing the step-by-step solution whereas Lample and Charton's method does not, but it would still be informative to compare the numbers.

you can only do the antiderivative check for single variable integrals: multivariable integrals over complex domains require step by step solution.

That seems to be a good point, but in that case you could make your paper more convincing by showing experiments with multivariable integrals. In its current state, the paper only studies expressions for which having the step-by-step solution is not crucially important.

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

Do you have some numerical results supporting this claim? Such an insight is valuable in itself, but we would need some evidence supporting it.