AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs
symbolic;math;integration;neurosymbolic;transformer;proof;search;symbolic engine
Yes
No ethics review needed.
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?
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.).
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.
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.
Yes
No ethics review needed.
* 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.
* 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.
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.
Please see the questions below.
Yes
No ethics review needed.
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.”
The paper is clearly written and easy to follow. 

The paper implements a learning approach to perform step-by-step integration.
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.
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.
Yes
No ethics review needed.
- 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?
- 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.
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.
- 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.
We train a transformer based engine to do exact symbolic integration through finding step-by-step proofs using synthetic data.
@inproceedings{
anonymous2024alphaintegrator,
title={AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=lJdgUUcLaA},
note={under review}
}
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.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
symbolic math integration neurosymbolic transformer proof search symbolic engine
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/091aa90e26d1bee2854d39145067414ed5ce1791.pdf
neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
/attachment/80d4153bff6e22ed6ecf6146c24b8fa9199b640c.zip
AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission