Neuro-Symbolic Data Generation for Math Reasoning

Summary

This paper introduces a methodology for generating mathematics data in a neurosymbolic fashion. Starting with existing math problems, they perform two different mutation operations: simplification and complication. The simplification operation performs variable and expression unfolding, whereas the complication operation adds additional complexity to the problem statements by adding auxiliary variables. Both operations are performed on the formalized problem statement (which is formalized in SMT-lib) format. Symbolic solvers attempt to solve the formal problem in a way which mimicks GPT-4 generated solution. The resulting procedure is applied with seed mathematics problems (like from GSM8K, MATH) and produces a dataset which they demonstrate to be of higher quality than prior approaches when fine-tuning open source models for mathematical reasoning.

Strengths

1. Performing the data synthesis process with formal specifications and using symbolic solvers is a nice idea, and is useful towards generating higher quality training datasets. 2. The evaluations indicate that their data generation process produces higher quality data compared to other existing approaches for synthetic data generation. This in particular indicates that the work is fairly significant and resultant dataset is likely to be used among the research community. 3. In general, the writing is clear and easy to follow. This makes the paper easily digestable. I noted some typos, see in a later section.

Weaknesses

1. In Section 3 you mention that a faithful conversion from the natural language to the formal specification cannot be automatically checked, and mention that you use GPT-4 to generate an informal solution and measure this against the solution produced by the symbolic solver. I am skeptical of a zero positive rate, and there does not seem to be any numerical results indicating a zero false positive rate. Is the consistency check performed by checking if the numerical solutions are the same? Or if the reasoning path produced by GPT-4 and by the solver are similar? If the latter case, how can you perform this check? 2. In the abstract the authors mention that a main component of their approach is the projected MCMC method. However, it is only mentioned briefly in the main content of the paper (lines 100-104) and the definition of what projected MCMC is is not included. I think it would be beneficial to include a more detailed discussion of this in the paper. 3. While grounding the methodology with formal specifications in SMT-Lib is a nice idea, they mention that for the MATH dataset the symbolic solvers are not usually capable of solving such problems, which hampers the applicability of this method. For the MATH dataset, they mention that of 7500 problems, 822 cannot be formalized in the SMT-Lib format and ~3600 are inaccurate so they bypass the solution verification (a central component of their approach) by prompting GPT-4 directly. Thus, I am worried about the scalability of this approach to harder mathematics (or reasoning) problems. Typos: Line 69: involes -> involves Line 157: effecitveness -> effectiveness Table 3 caption: illusrate -> illustrate Line 338: repsectively -> respectively

Questions

1. What do GPT-4 generated solutions look like? No examples are provided in the paper. Similarly, no solution outputs from the symbolic solvers are provided. Figure 1 mentions that reasoning paths are produced by GPT-4 but are never shown. 2. In the complication section, can you provide specific details about the choice of interpreted functions $foo$? It is only mentioned at the top of page 4 as far as I know. It would be good to include (perhaps in the appendix). Why is a random (uniform) selection among them a good choice? It might be unnatural to include too many problems including arcsin, for example. 3. Which symbolic solvers are used? SMT Solvers may not return a reasoning path for solution to a problem, only indicating a truth value and a final answer. On page 2 they mention that sympy & scipy are not directly amenable for smt-lib but it can be extended pretty easily. Are sympy and scipy used?

Rating

7

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

I believe the authors have adequately addressed limitations of their work.

Summary

This paper proposes a neural-symbolic framework to generate valid and diverse mathematical training data at scale. The framework consists of three steps: formalization, mutation, and reformalization. The first two steps are achieved using symbolic solvers, while the last step is accomplished using large language models (LLMs). The mutation step is controllable. The experiments demonstrate that the proposed method is more effective, efficient, and scalable.

Strengths

- The paper is clearly structured and easy to follow. - The proposed method is novel, particularly the reliable and controllable mutation mechanism. I believe this will be very beneficial to the community and has the potential to scale up significantly beyond the current capabilities. - The experiments are solid and contain interesting findings, such as the increasing lengths of the generated solutions and the accuracy improvement with the increasing difficulty of the problems.

Weaknesses

- It would be beneficial to compare the proposed method with other mathematical models that have comparable SFT data sizes, such as those in [1][2]. [1] MathScale: Scaling Instruction Tuning for Mathematical Reasoning [2] Augmenting Math Word Problems via Iterative Question Composing

Questions

What is the cost of synthesizing 860k data? For example, what is the CPU cost (e.g., how many CPU hours) needed for the symbolic solvers?

Rating

7

Confidence

5

Soundness

4

Presentation

4

Contribution

4

Limitations

Yes

Summary

To solve the dilemma of diversity and validity involved in current math problem generation methods, this paper proposes a neuro-symbolic framework that initially generates formal mathematical problems and then informalizes them back into natural language versions. By casting the data generation into the formal language space, the diversity and validity of the generated math problems can be effectively ensured. Then, a mutation mechanism is adopted to establish the math dataset encompassing various difficulty levels, and prompt the LLMs to accomplish informalization with consistency between formal language problem and its natural language version guaranteed by symbolic solvers. Experimental results demonstrate that the synthetic data can significantly enhance the performance of various LLMs in mathematical reasoning tasks.

Strengths

1.the proposed framework is promising to both guarantee the diversity and accuracy of the synthetic mathematical data, based on the formal language. 2.experimental results have shown the effectiveness of the whole approach.

Weaknesses

1.the motivation of this work is obvious, but it is not clear how to convert the natural language into the well-formulated SMT-LIB language. The cost and examples about the whole pipeline should be depicted in the paper. Also, I am wandering if the formulation process is not also compatible for all the natural language questions, should human effort be involved for controlling the quality? 2.the whole approach is also similar to existing work that using program with tools to process natural language questions. It is not clear what is the major difference between the SMT-LIB language and the program-aided language in existing work. Why not using programming language for the whole pipeline? 3.the experimental setting is not fully fair. For the main results, all the compared baselines are trained using 1/2 fewer data. I suggest authors to report the results using the same data amount as the best-performed baselines for comparison.

Questions

Please refer to the weaknesses

Rating

5

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

None

Summary

This paper describes a framework to transform natural language math problems into a formal setting (e.g., in SMT-LIB format), mutate the problems in a user-specified way, and auto-informalise those mutated problems into natural language ones. Through this pipeline, a larger synthetic dataset can be generated to bootstrap the math reasoning performance of existing LLMs (e.g., via fine-tuning). Improved performance has been achieved against previous SOTA including MetaMath.

Strengths

- relatively well-written, good performance against prior works - I especially appreciate the ideo of mutating the problem in a controllable ways, which leads to slightly more transparent LLMs. - More importantly, a promising scalability of this method has been demonstrated in Figure 4: as the size of the synthesised dataset grows, the performance of the fine-tuned model LLaMA-2-7B is more consistently enhanced (in comparison to the baseline approach MetaMath).

Weaknesses

- As a trade-off for controllability, the math problems need to be formalized into a user-specified structure. This requirement may significantly hinder the proposed approach from being adapted to problems beyond high school competition level. - Although the authors demonstrate that this approach performs comparably or even better than many existing tool-use methods, I am uncertain if it serves as a suitable replacement for these frameworks, which may be more efficient and reliable. Perhaps we could conduct experiments to explore combining this approach with existing tool-use frameworks? - The complication process could be better formulated. In a formal setting, I would appreciate a more rigorous definition of validity and diversity, along with a clearer explanation of what has been preserved and enhanced during the mutation process. Additionally, I would like to see more details on how the projected MCMC method enhances the diversity of mutated problems. Including some pseudocode would be helpful. Minor: - line 157, typo: 'effecitveness' -> 'effectiveness'

Questions

- As a methodology that heavily relies on fine-tuning that sometimes cause catastrophic forgetting, I am curious to know the performance of the fine-tuned models on other non-math tasks.

Rating

7

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

N.A.