Neuro-Symbolic Data Generation for Math Reasoning

Authors: zenan  li
zhi  zhou
yuan  yao
yu-feng  li
chun  cao
fan  yang
xian  zhang
xiaoxing  ma
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-14 13:34:38

Abstract: A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning is inherent, or merely a result of insufficient exposure to high-quality mathematical data. To explore this, we developed an automated method for generating high-quality, supervised mathematical datasets. The method carefully mutates existing math problems, ensuring both diversity and validity of the newly generated problems. This is achieved by a neuro-symbolic data generation framework combining the intuitive informalization strengths of LLMs, and the precise symbolic reasoning of math solvers along with projected Markov chain Monte Carlo sampling in the highly-irregular symbolic space.
Empirical experiments demonstrate the high quality of data generated by the proposed method, and that the LLMs, specifically LLaMA-2 and Mistral, when realigned with the generated data, surpass their state-of-the-art counterparts.

Main paper: 
 introduction: 
 Despite recent progress [1] [2] [3] [4] [5] [6] , both proprietary and open-source LLMs are still far from satisfactory in mathematical reasoning [7] [8] [9] . It is an open question whether LLM's subpar reasoning capability is inherent or due to the the extreme scarcity of high-quality mathematical datasets [10] [11] [12] [13] . As an initial step towards answer this question, a data generation framework that could create high-quality math datasets is required. To this end, current two lines of research struggle in the diversity-validity dilemma: (1) to produce diverse math data, the prompt-based method effectively rephrases math problems using LLMs, but may induce errors thus ruining the validity, especially considering the rigor of maths; (2) to ensure the validity, template-based methods are often used by rewriting math problems with certain rules, sacrificing the diversity and thus confining data scale.To address this dilemma, we propose a novel neuro-symbolic framework that automatically generates high-quality, supervised mathematical data. The merit of this paradigm lies in leveraging both neural and symbolic strengths: (1) the math problem is generated in the symbolic space, achieving diversity through systematic sampling, while maintaining validity through symbolic solvers; (2) the translation from the symbolic space back to the natural language space can be effectively supported by LLMs, ensuring the consistency between newly generated formal problems and their corresponding natural language versions. Our framework, as illustrated in Figure 1 , initiates with the formalization of the original problem expressed via the math symbolic tools. Next, it mutates the formal problem into an evolved version, and then derives a new natural language problem by informalization. Specifically, we design a mutation mechanism, including various simplification and complication strategies, such that the new problems can be generated with a controllable complexity. As shown in Figure 2 , our mutation mechanism can properly adjust the complexity of generated problems, and the exposure to more A rectangle has a perimeter of 30 units. The length of the rectangle is 14 units more than twice its width. However, due to a mistake in measurement, the actual perimeter is 4 units less than twice the sum of its width and length. What is the width of the rectangle? Q: A rectangle has a width and a length. The perimeter of the rectangle is 17 units. The length is calculated using the expression: first, multiply the width by 8, then add 31, subtract 38, and finally, multiply the result by 16 . The perimeter is also given by another expression: add 76 to twice the sum of the width and length, then subtract 63 and 30. What is the width of the rectangle? A: 1Seed problem Generated problems with controlled difficulty levels. 3) Translate the variants in symbolic form back to the natural language version. Additionally, we prompt GPT-4 to generate reasoning paths, which are verified by symbolic solvers, as part of the supervision. complex math problems can improve the LLM's reasoning capability. Moreover, to ensure the data validity and achieve higher generation diversity, we combine the symbolic solving with the random sampling through the projected Markov chain Monte Carlo technique [14, 15] . Empirical evaluation on GSM8K [10] and MATH [11] demonstrates the effectiveness of the proposed method. Particularly, we use the proposed framework to generate a mathematical dataset of 620K examples for supervised fine-tuning. The experimental results show that, the fine-tuned models on LLaMA-2 [16] and Mistral-7B [17] significantly outperform the existing open-source counterparts on both GSM8K and MATH datasets, as well as two out-of-domain datasets SVAMP [12] and ASDiv [18] . On the GSM8K dataset, the model fine-tuned on Mistral-7B even outperforms GPT-3.5-Turbo (by 2.4%), a proprietary model with an order of magnitude larger parameters. Additionally, we evaluate the scalability of our method, and observe consistent performance improvements, as the size of training data increases. This upward trajectory suggests a promising avenue for further enhancing LLMs' mathematical capabilities. Initalize random operations ⊕ i and interpreted functions e ′ i .3:Mutate g ′ = g ⊕ 0 e ′ (z 0 ), h ′ i = h i ⊕ i e ′ (z i ) with parameter z i . 4:Randomly perturb a subset {z 1 , . . . , z j } for j < n.Solve the rest subset {z j+1 , . . . , z n }.if {z 1 , . . . , z n } is solvable then7:Instantiate the new problem by {z 1 , . . . , z n }.Stop the complication process Initalize a random tactic from {simplify, qe, simplify, . . . }.Apply the tactic to the problem g ′ and constraints h ′ 1 , . . . , h ′ n . 14: end for 
formalization: 
 We first provide the formalization of math problems, based on which the mutation mechanism is operated. Specifically, we adopt the SMT-LIB language [19] , a standard notation compatible with prevalent SMT solvers (e.g., Z3 [20] , CVC5 [21] , and MathSAT [22] ). It can also be easily extended for symbolic calculators (e.g., SymPy [23] ) and numerical solvers (e.g., SciPy [24] ). With SMT-LIB language, the math problem in the following structure is enabled: Goal g := min | max | solve f (x) Constraints h := h 1 ∧ h 2 | h 1 ∨ h 2 | ite(h 1 , h 2 , h 3 ) | ∀x. e 1 (Domains D := N | N + | R | Cwhere c denotes a constant, x denotes an n-dimensional variable, ite denotes the if-then-else structure, foo refers to an interpreted function (e.g., trigonometric, logarithmic or user-defined ones) on the domain, and g and h represent any function of interest (can include quantifiers). In particular, we pre-defined a series of interpreted functions, such as summation, binomial, gcd, lcm, derivate, and integral, which facilitate the formalization of most high-school level mathematical problems (excluding geometry) within the above SMT-LIB language.We perform simplification by systematically considering expression reduction and constraint reduction, which can be attained through heuristic tactics provided by standard symbolic solvers [25] .Specifically, we apply the simplify tactic for expression reduction, which involes operations such as constant or variable folding (e.g., x + 0 ⇒ x or y + x -x ⇒ y), expression expansion (e.g., (x + 1) 2 ⇒ x 2 + 2x + 1), and function application (e.g., (x = 2) ∧ (y = log(x)) ⇒ y = log(2)); we also perform symbolic and numerical computations for further reductions (e.g., gcd(2x, 6y) ⇒ 2gcd(x, 3y) and sin(π/6) ⇒ 0.5).For constraint reduction, we mainly employ the Gaussian elimination tactic gaussian_elim (e.g.,x = 2 ∧ y ≤ x + z ⇒ y ≤ 2 + z).To handle the if-then-else term, we apply the elim_term_ite tactic to decompose it by introducing a fresh variable (e.g., ite(x > y, x, y) > z ⇒ (k > z) ∧ (x > y → k = x) ∧ (x ≤ y → k = y)).For constraints involving quantifiers, we strive to eliminate them using the qe tactic (e.g., ∃y.(y > 0) ∧ (x = y + 2) ⇒ x > 2). Appendix B provides more examples illustrating these simplifications.To complicate the expressions, a straightforward strategy is to incorporate additional operators. For example, given an atomic constraint h = e 1 ▷◁ e 2 , we can introduce an additional expression, denoted by e ′ , and derive a more complex constraint h = e 1 ▷◁ (e 2 ⊕ e ′ ).(M 1 )     a(b + c) = 152 b(c + a) = 162 c(a + b) = 170 a, b, c ∈ N + ⇒ (M 2 )      a(b + c) = 152 ⊕ 1 e ′ 1 (z 1 ) b(c + a) = 162 ⊕ 2 e ′ 2 (z 2 ) c(a + b) = 170 ⊕ 3 e ′ 3 (z 3 ) a, b, c ∈ N + , z 1 , z 2 , z 3 ∈ R ⇒ (M 3 )              a(b + c) + z 1 = 152 b(c + a) -z 2 = 162 c(a + b) = 170 z 1 = 114 z 2 = 36 a, b, c ∈ N + ⇒ (M 4 )              a(b + c) + d = 152 b(c + a) -e = 162 c(a + b) = 170 d + e = 150 d -e = 78 a, b, c, d, e ∈ N +However, such a strategy is non-trivial in practice. The first challenge lies in the validity aspect, i.e., the math problem is often carefully designed, and thus a random mutation may ruin their well-defined structure. Consider the running example problem (M 1 ), which has been normalized for simplicity. In this problem, a reckless mutation can easily violate the positive integer constraints, causing the problem ill-defined and unsolvable.To address this issue, we equip each mutation with an auxiliary variable, followed by symbolic solvers to ensure the problem remains well-defined. Continuing with the previous example, we introduce three auxiliary variables, denoted by z 1 , z 2 , z 3 , and then mutate the problem as (M 2 ), where ⊕ 1 , ⊕ 2 , ⊕ 3 ∈ {+, -, ×, ÷} represent three random operators. Furthermore, we instantiate e ′1 , e ′ 2 , e ′ 3 by interpreted functions, i.e., e ′ 1 = foo 1 (z 1 ), e ′ 2 = foo 2 (z 2 ), and e ′ 3 = foo 3 (z 3 ), where foo 1 , foo 2 , foo 3 are randomly selected from foo(z) = z | log(z) | exp(z) | arcsin(z) | • • • .For our running example, we simply choose the identity function for foo 1 , foo 2 , foo 3 , and set ⊕ 1 = -, ⊕ 2 = +, ⊕ 3 = ×. Using symbolic solvers to compute a feasible solution of (z 1 , z 2 , z 3 ), we derive a new and well-defined problem (M 3 ).The subsequent challenge is to ensure the diversity of the mutated problems, which now becomes how to make the solutions of auxiliary variables sufficiently diverse. This is essentially a model counting problem [26, 27] , and current symbolic solvers still underperform in this regard [28] . To this end, we instead opt for auxiliary variable solution generation via the projected Markov chain Monte Carlo (projected MCMC) [14, 15] . Simply put, projected MCMC first perturbs a subset of variables (projected random walk), and then resolves the remaining part (inverse projection via symbolic solvers), which ensures both diversity and validity of the variable solutions.Finally, to complicate the constraints, one can easily reverse the process of simplification. For our running example, we can reverse the Gaussian elimination with refreshed variables, obtaining the final form (M 4 ), which is then included as a new problem in the dataset.Question: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes] Justification: The limitation is thoroughly discussed in Appendix ??.Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
informalization: 
 Informalization aims to translate a formal problem back to natural language without the loss of soundness [29] . As shown in Example 1, a simple, one-line instruction follows the formally posed SMT-LIB problem, serving as the input. Then, GPT-4 interprets the formal problem as a new math word problem.The key challenge of informalization lies in ensuring a consistent conversion, i.e., the natural language problem informalized by GPT-4 should align with the formal solution given by symbolic solvers. Since it is difficult to directly measure this consistency, we instead use GPT-4 to generate a solution for each informalized problem, and then calculate the consistency rate between the solutions from GPT-4 and those from symbolic solvers as a surrogate metric. Furthermore, we observe that, if the problem is incorrectly informalized, GPT-4's solutions almostly cannot be confirmed by symbolic solvers (i.e., zero false positive). Therefore, the surrogate consistency rate can be regarded as a lower bound to the true consistency rate. Translate the math problem formulated with SMT-LIB back to a natural language problem.Sara bought a pair of shoes for $50.00 and a dress for $200.00. If Rachel has twice the amount that Sara spent in total, how much is Rachel's budget?To further improve conversion consistency, in addition to the basic zero-shot learning template in Example 1, we investigate the effects of the following operations, whose detailed examples are available in Appendix C. (1) Mutation. Mutation complicates the problem, making the informalization more difficult. Therefore, we first analyze the informalization error caused by the mutation.(2) Few-shot learning. Few-shot examples offer a stronger instruction to the LLM, and also introduce the randomness when aided by random retrieval.(3) Comment generation. Recognizing that GPT-4 is unfamiliar with SMT-LIB's prefix expressions, we automatically convert these into the infix format, included as comments.(4) Math-word instruction. We simply append one more sentence "Ensure to be a math word problem" in the prompt. With this instruction, informalization tends to imbue digits with some practical meaning (e.g., 7 ⇒ one week).(5) Problem modification. For mutated problems, rather than generating a new informalization, we prompt GPT-4 to modify the original informalization result.(6) Variable refresh. We standardize the naming of all introduced variables (e.g., rachel_budget ⇒ x_1), to eliminate the impact of math word problems.Different combinations of the above operations result in different patterns. The effects of some typical patterns are shown in Table 1 , where the results are evaluated on 1,000 problems randomly sampled from GSM8K. The basic pattern in Example 1 yields a consistency rate of 75.6%. The mutation operation alone indeed degrades the consistency, but its combination with other operators can further boost the informalization performance. In practice, we use two different patterns for different informalization styles: the first pattern (P1) tends to generate math word problems, whereas the problems generated by the second pattern (P2) tend to be pure math problems.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?Answer: [NA]Answer: [Yes] Justification: We provide the code for our data generation framework, as well as a small part of our generated data, in the supplementary material. Guidelines: Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 
experiments: 
 In this section, we conduct a series of experiments to answer the following four research questions:RQ1: Efficacy -Using our data generation framework, can the fine-tuned model achieve better performance compared with existing models?RQ2: Efficiency -Given the same data generation budget, is the generated data from our framework better than that from the state-of-the-art data generation framework?RQ3: Generability -Is the effecitveness achieved by our framework due to potential data contamination introduced during the generation process?RQ4: Scalability -With more data generated, can our approach be continually effective in further improving model performance?Dataset. We conduct our data generation on the training sets of two popular mathematical reasoning benchmarks: GSM8K [10] and MATH [11] . GSM8K is a dataset comprising high-quality grade school math problems, which contains 7,473 training data and 1,319 testing data. MATH is a dataset comprised of challenging competition math problems, spanning seven subjects including Prealgebra, Algebra, Number Theory, Counting and Probability, Geometry, Intermediate Algebra, and Precalculus. There are 7,500 training data and 5,000 testing data in the MATH dataset. Additionally, we include two mathematical reasoning datasets, i.e., SVAMP [12] and ASDiv [18] , to evaluate the out-of-domain generalizability of the models fine-tuned on the data generated from GSM8K and MATH datasets.Comparison Methods. In our experiments, we compare the models trained using our generated data with existing state-of-the-art open-source mathematical reasoning models, including WizardMath [30] , MuggleMATH [31] , MAmmoTH [32] , and MetaMath [33] . We also conduct a thorough comparison between our math generation method and the bootstrapping method employed in MetaMathQA [33] , which is presently the most extensive open-source dataset for mathematical reasoning.Data Generation Details. We use our mutation mechanism to generate a series of problems with varying levels of difficulty, and the specifics are as follows. Starting with a problem from the original dataset as a seed, we first perform simplification to the problem, and define this new version as level-0. Then, we randomly apply one expression complication step and one constraint complication step to the level-0 version, deriving a more difficult problem (level-1 version); and such complications can be repeated to obtain more difficult problems. For the GSM8K dataset, we create datasets across five levels of difficulty, with 30K examples at level-0 and 100K examples for the remaining four levels.As for the MATH dataset, we establish four levels of difficulty, where level-0, level-1, level-2, and level-3 contain 70K, 120K, 120K, and 120K examples, respectively. Particularly, for some problems in the MATH dataset that cannot be solved by symbolic solvers, we directly prompt GPT-4 to rephrase the problem and ignore the solution verification. The number of generated problems without solution verification varies across problem categories, and the details can be referred to Appendix D. In total, we generated 860K math problems based on the proposed framework to construct our dataset.Each generated math problem consists of a natural language problem description informalized by GPT-4 (version 0710), a final answer outputted by the symbolic solver, and a reasoning path from the problem to the final answer. The reasoning path for each problem is also generated by GPT-4, which is further verified by the corresponding answer derived from symbolic solvers.More implementation details about training hyperparameters, instruction prompts, and symbolic solver integration, are included in Appendix D.RQ1: Efficacy. Using the generated math dataset, we fine-tune the LLaMA-2 base models of 7B and 13B parameter sizes, as well as the Mistral 7B base model. The fine-tuned models, as well as the comparison methods, are evaluated on the GSM8K and MATH datasets. In addition to the above competitors, we also compare our models with tool-based models, and provide the results in Appendix E.2. We summarize two observations here. First, tool-based models tend to over-rely on external tools, and thus do not necessarily improve the inherent reasoning ability of LLMs. Second, although the tool-based models perform better on the MATH dataset (which frequently entails complex calculations), they still underperform on the GSM8K dataset (which emphasizes knowledge reasoning but involves simpler calculations).RQ2: Efficiency. To illustrate the data efficiency of our method, we carry out a comparative experiment with current SOTA method MetaMathQA [33] . The MetaMathQA dataset comprises 240K data bootstrapped from the GSM8K training dataset and 155K data from the MATH training dataset. To ensure a fair comparison with MetaMathQA, we use the same data budget. Additionally, we expand the MATH data of the MetaMathQA dataset to 430K, aligning its size with that of our generated data. Then, we fine-tune LLaMA-2-7B models on the 240K GSM8K augmented data, as well as the 155K and 430K MATH augmented data, respectively.The performance of fine-tuned models are given in Table 3 . We also evaluate the models on two out-of-domain datasets, SVAMP and ASDiv. The results confirm the efficiency of our framework. With an equal generation budget of 240K for the GSM8K dataset and 155K for the MATH dataset, our method exhibits accuracy improvements, ranging from 2.1% to 24.4% across the four datasets. This superiority is consistent with the model trained on 430K MATH generation data, with improvements of 19.9%, 3.2%, 12.7%, and 19.2%, respectively.RQ3: Generability. Despite we carefully ensure that our mutations on the training set do not access the test set, we still provide a series of analysis about the potential data contamination or overfitting issues. We first use the memorization detection method introduced in Minerva [34] . Specifically, we select 150 problems with the highest majority vote score and then compute the BLUE score [35] on solutions of trained Mistral 7B, GPT-4, and the ground-truth. The results of our method and MetaMath are provided in Figure 3 , which show that our BLUE score on the test set is (1) much lower than our BLUE score on the training set; (2) is consistent with that of MetaMath. Hence, there is no evidence that the mutation contaminates the test set.Second, in addition to the two out-of-distribution datasets SVAMP and ASDiv, we conduct experiments on another benchmark DyVal [9] , which avoids the leak of test set through dynamically generating new benchmarks. The results of our models, alongside those of the comparison models, are provided in Appendix E.3. In summary, our models demonstrated superior performance in 11 out of 12 cases and delivered competitive results in the remaining case. Particularly, as the complexity of the tasks increased, our models exhibited a relatively robust performance compared to other models.Finally, we include an additional experiment on the Hungarian High School National Finals Exam dataset [36] , whose problems are newly collected at 2023. We manually check 33 testing problems based on the provided ground-truth answer, and our model correctly solved 14 problems and partially solved 6 problems, resulting in an exam score of 44. The result is comparable to GPT3.5-turbo (i.e., 41 exam score), conforming the generalizability of our method. The two datasets are generated by our approach and MetaMath (MMQA). The performance can be consistently enhanced by increasing the amount of data generated using the proposed framework.RQ4: Scability. To explore the scalability of our framework, we fine-tune the LLaMA-2 7B model using our generated datasets of various sizes and difficulties. To be specific, we progressively incorporate a 30K dataset, along with four additional 70K datasets generated from GSM8K. Note that these five datasets are randomly sampled from five different levels of difficulty. Five LLaMA-2-7B models are fine-tuned based on these datasets, and the scalability curves are shown in Figure 4 . We also include MetaMathQA with the same data settings as a reference. Since MetaMathQA cannot inherently group the dataset into various difficult levels, we construct five datasets by incrementally random sampling from the GSM8K subset of the MetaMathQA dataset.The results presented in Figure 4 indicate the promising scalability of our method. That is, as the size of data increases, the accuracy of the model consistently improves. In contrast, the performance enhancement observed in MetaMathQA is limited and starts to diminish as the data size reaches 70K. We also present the models' performance on the other three out-of-domain datasets in this case, i.e., SVAMP, ASDiv, and MATH datasets. The results demonstrate that the scalability of our method is robust and generalizable, while MetaMathQA hardly guarantees such consistency.We also investigate the diversity gain relative to the original dataset for each difficulty level. The results are provided in Appendix E.4. It is observed that the dataset consisting of the same difficulty level cannot further improve the diversity with a larger data budget. On the contrary, the diversity gain of the dataset comprising all difficulty levels continues to increase as the data budget grows. 
related work: 
 Recent surveys [37] [38] [39] have comprehensively discussed the current advances in the mathematical reasoning of LLMs. Here, we review three main lines of existing work on enhancing the mathematical reasoning for LLMs related to our study: prompt-based methods, rephrasing-based methods, and tool-based methods.Prompt-based Method. Prompt-based methods aim to harness the inherent capabilities of LLMs by carefully designing appropriate input prompts without tuning the model parameters. This line of work starts from the observation that LLMs can effectively tackle more math problems when provided with a simple Chain-of-Thought (CoT) prompt, i.e., "Let's think step by step" [40] . Building upon the CoT prompt, Wang et al. [41] further propose to consolidate multiple reasoning paths based on the self-consistency of correct answers. Later, several researchers propose to prompt LLMs to decompose complex problems. For example, Zhou et al. [42] introduce the least-to-most strategy that prompts LLMs to break down the original problem into a series of sub-problems. Khot et al. [43] further boost this strategy, by assigning each sub-problem to the corresponding LLM that is specifically optimized for it. Finally, few-shot prompting, e.g., Few-shot CoT [44] and Complex CoT [45] , has also been studied to enhance the reasoning performance of LLMs. To further improve the few-shot prompting, the prompt retrieval is proposed to automatically select high-quality examples [46, 47] , while the prompt compression is explored to include more examples in restricted context by pruning each example [48] .Rephrasing-based Method. The second line of existing work aims to generate additional math data, based on which the mathematical reasoning capability of LLMs can be established via supervised fine-tuning. To address the data scarcity issue, current research mainly focuses on rephrasing the problem or the answer. For the answer rephrasing, Magister et al. [49] adopt the PaLM and GPT-3 to generate CoT math data, resulting in improved performance of the T5 model on math reasoning tasks. To mitigate the inclusion of incorrect answers during the supervised fine-tuning, RFT [50] introduces a rejection sampling strategy, whereas AFT [51] trains an LLM to categorize them.Regarding the problem rephrasing, WizardMath [30] proposes a reinforced evol-instruct method. It instructs ChatGPT and trains a new LLM to rephrase the problem, equipped by a reward model for evaluating the quality of generated problems. Combining the rephrasing of problems and answers together, MuggleMATH [31] builds the AugGSM8K dataset based on prompting GPT-3.5 and GPT-4.MetaMath [33] develops a question bootstrapping method based on LLMs, unifying rephrasing, self-verification [52] , FOBAR [53] , and answer augmentation strategies, obtaining the MetaMathQA. Xwin-Math [54] is a peer study that significantly enhances the reasoning capacity of LLMs using problems generated by GPT-4 Turbo. In contrast, our work focuses on generating verifiable problems through controllable mutations, rather than relying entirely on the GPT model.Our proposed method also falls into this category. In contrast to existing methods directly prompting LLMs to rephrase the problem, we mutate the problem in the formal symbolic space, resulting in a more controllable mutation mechanism that ensures both the validity and diversity of the generated problems. Moreover, the quality of reasoning paths is also guaranteed by the symbolic solvers.Tool-based Method. Tool-based methods aim to enhance the math solving performance of LLMs by instructing them to use external math tools. For instance, PoT (Program of Thought) [55] and PAL [56] propose to prompt the LLMs to delegate the computation to a program interpreter, which can be executed to obtain the final answer. To further improve the tool-using ability of LLMs, MathCoder [57] constructs a math dataset containing problems and their code-based solutions for the supervised fine-tuning; MAmmoTH [32] builds a dataset that combines CoT and PoT reasoning, enabling LLMs to perform hybrid inference. Since the interaction with math tools can further boost the performance of LLMs, TVA [58] includes the Isabelle theorem prover to check each reasoning step and guide the reflection of LLMs; Tora [59] generates interactive tool-use trajectories on mathematical datasets and then performs imitation learning on the annotations.Our proposed method shares some similarities with tool-based approaches as both involve symbolic solvers. However, rather than using external tools to solve mathematical problems, our approach aims to explore the inherent reasoning capability of LLMs. Therefore, symbolic solvers are only used to ensure the validity of the generated data as well as the correctness of the generated reasoning paths. 
limitations: 
 The Capability of Symbolic Solvers. The effectiveness of our approach significantly hinges on the symbolic solvers. However, existing mathematical tools (e.g., Z3 [20] , SymPy [23] , and SciPy [24] ) face limitations when it comes to expressing and solving a wide array of mathematical problems. For instance, the Z3 SMT solver struggles with expressing higher-order concepts like gcd and lcm, while the SymPy encounters difficulties in solving inequalities involving multiple variables. In our framework, we integrate five mathematical tools, i.e., Z3, CVC4 [60] , MathSAT [22] , SymPy, and SciPy, and employ SMT-LIB [19] as a unified formal language to enhance the performance of symbolic solving.The Expressiveness of Mutations. The mutation operators used within our framework remain limited, especially in generating more difficult problems (e.g., college-and even IMO-level math problems). One of our future work is to introduce more mutation operators, further increasing the problem difficulty. A possible strategy is the problem fusion [61] , which fuses two formal problems into a single, new problem, rather than merely modifying an individual problem. Moreover, the informalization facilitated by LLMs can effectively mitigate the unnaturalness issue stemming from brute-force fusion.The Dependence on GPT-4. GPT-4 is involved in our framework to carry out the informalization and generate the reasoning paths. We also consider the possible solutions that the dependence on GPT-4 can be gradually removed. First, by leveraging our generated formal-informal pairs, we can fine-tune a new LLM specifically for the informalization. Second, it is possible to bypass the generation of reasoning paths, through curriculum learning [62, 63] instead of supervised finetuning. Particularly, the reward in the curriculum learning can be determined by whether the generated solution is consistent with symbolic solvers , and the curriculum progresses by incorporating problems of various difficulty levels.The paper aims to advance the field of math data generation. There are many potential societal consequences of our work, and we firmly believe that the majority of these impacts are positive and none which we feel must be highlighted here. 
conclusion: 
 This paper explores the question of whether sufficient exposure to high-quality mathematical data could enhance LLMs' inherent mathematical reasoning capability. We identify a key challenge in balancing diversity and validity in current math problem generation methods. To tackle this challenge, we propose 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 by the systematic sampling and symbolic solvers. Building upon this, we carefully devise a mutation mechanism, establishing the math dataset encompassing various difficulty levels, and prompt the LLMs to accomplish informalization. Through empirical experiments, we demonstrate that our neuro-symbolic data generation framework significantly enhances the performance of various LLMs in mathematical reasoning tasks, surpassing the current state-of-the-art open-source models.The results also suggest a promising pathway for further enhancing LLMs' mathematical capabilities.In future work, we intend to expand the expressiveness of mutations and enhance the capability of symbolic solvers to support more types of problems, such as inequality problems. Our goal is to offer a data generation framework to automatically generate high-quality, supervised datasets for LLMs. We expect that our neuro-symbolic data generation framework can provide a potential solution for LLMs to solve the problem of data scarcity, and thereby facilitate in building more LLMs in downstream tasks. Further, our framework has the potential to be integrated with recent studies [64] , which only require problems and final answers.for the learning rate, which is set to 5e-6. Moreover, we adopt the instruction template Prompt 1 used in Alpaca [67] for fine-tuning each model. 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes]Justification: Social impacts are discussed in ??.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.• The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA]Justification: The paper does not pose such risks.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [Yes] Justification: Code packages and datasets are properly cited.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. 
 
 Appendix: Below is an instruction that describes a task. Write a response that appropriately completes the request.\n\n### Instruction:\n{instruction}\n\n### Response:\n Evaluation Details. We evaluate fine-tuned model using a zero-shot evaluation protocol with the corresponding recommended instruction template. Our model is evaluated using the following instruction template Prompt 2, which is consistent with our training instruction template.For answer extraction and accuracy calculation, we follow the code of WizardMath [30] to extract the answer after the phrase "The answer is".Symbolic Solvers. We integrate five symbolic solvers, Z3, CVC4, MathSAT, SymPy, and SciPy based on the PySMT framework [68] . To be specific, the PySMT intrinsically includes Z3, CVC4, and MathSAT, and we further extend its support to encompass SMT-LIB version 2.5, which incorporates more commands like define-rec. Next, we proceed to serialize the SMT-LIB format into SymPy expressions, and attempt to find solutions using SymPy's solve function. In addition, the SymPy expressions are also encoded as NumPy [69] functions, thereby enabling the using of SciPy's optimization modules, such as differential_evolution and minimize. Note that we introduce a fuzzy-logic-like strategy [70] [71] [72] in the encoding, which combines the equalities and inequalities into a loss function, subsequently enabling optimization methods for problem-solving tasks.We present detailed results across different categories in the MATH dataset in Table 5 . The numbers 1-7 correspond to Algebra, Counting and Probability, Geometry, Intermediate Algebra, Number Theory, Prealgebra, and Precalculus, respectively. The results indicate that Algebra is easier to improve, as evidenced by its higher mutation success rate. It is worth noting that improvements in Counting and Number Theory are reasonable because related mutation operators (e.g., binomial, gcd, lcm, etc.) are included in our framework. However, Precalculus and Geometry are still not well-supported. For example, the concept of triangle cannot currently be correctly expressed in the SMT-LIB format, resulting in relatively low improvement rates. We compare our model with the tool-based models in Table 6 . Although tool-based models achieve good performance with tools, they meet severe performance degradation when tools are not available. This result indicates that training a model using code-based and language-based rationales does not necessarily enhance the intrinsic reasoning ability; instead, it often promotes excessive dependence on external tools. For datasets that involve complex calculations, such as the MATH dataset, toolbased methods offer certain advantages due to their utilization of the strong capabilities of external tools. For datasets that emphasize knowledge reasoning but involve simpler calculations, such as the GSM8K dataset, they underperform our proposed methods, proving that their reasoning ability is still inadequate.We also compare our models and existing mathematical reasoning models using DyVal [9] datasets to further evaluate the generalization ability of our models. DyVal is a flexible evaluation protocol for dynamic evaluation of LLMs, which generates evaluation samples with controllable complexities using directed acyclic graphs (DAGs). We focus on Arithmetic tasks using three DAGs' orders: topological (TOPO), reversed topological (REVERSED), and random orders (RAND). Following the same setting, we generate testing four increased complexity levels {D1, D2, D3, D3}, with tree depths and widths set to (. The performance comparison between models fine-tuned on LLaMA2-7B and Mistral-7B are respectively shown in Table 7 and Table 8 . The results show that our models achieve the best performance in 11/12 cases and give a competitive performance in the remaining one case. As the complexity increases, our models achieves a relatively robust performance compared with the other models. To illustrate the need for various difficulty levels, we calculate the diversity gain relative to the original dataset for each difficulty level. We apply the same method as in MetaMath [33] to compute diversity gain but use the BERT model [73] as a feature extractor instead. We select data budgets of 35K, 50K, and 100K, respectively, and investigate the diversity across four levels, from level-1 to level-4. Additionally, we create a mixed version by sampling data from all levels. The results are shown in Figure 5 , and we can observe that: (1) The higher the difficulty level, the greater the diversity of generated data; (2) The mixed version increases with the growing data budget, and achieves the highest diversity gain. Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 


Decision: This paper addresses the important problem of generating informative datasets to train LLMs to reason. In particular, the authors devise a neuro-symbolic pipeline that through auto-formalization generates mathematical problems in a domain-specific language, then "mutates" them and generates paraphrases in natural language. This pipeline is shown to generate data that empirically boosts the performance of a range of LLMs.

Reviewers appreciated the neuro-symbolic direction of the paper, and the provided boost in performance. At the same time, they highlighted a number of potential issues, namely, lack of discussion on scaling with data size and how costly the method could be for users. Furthermore, they requested more formal definitions for concepts of validity and diversity as used in the paper, and details for reproducibility. The authors successfully addressed these concerns during rebuttal, convincing reviewers to increase their scores. While some perplexity still remains around the quality of the presentation of the work and some related works (which however are different in practice as they use tools), I believe that the work brings enough valid contributions to the table to be accepted.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: - 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: 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.
limitations: limitations: N.A.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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: questions: Please refer to the weaknesses
limitations: limitations: None
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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: 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?
limitations: limitations: Yes
paper_summary: paper_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.
strength_weakness: strength_weakness: 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: 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?
limitations: limitations: I believe the authors have adequately addressed limitations of their work.

Comments: title: Response to Reviewer UMpg
comment: Thank you for your detailed responses, which have addressed most of my concerns. I believe I provided a fair rating and intend to maintain it.
I have read the response. Thanks for your clarification. I have increased my score.
Many thanks for the elaborated response. All my concerns have been resolved. I will increase my score.
Thanks for answering these questions. I think the authors have addressed all the questions I had in a satisfactory way. Consequently I have increased my score.
> You mean that the symbolic solver does not terminate in producing a numerical answer, right?
> 

Yes. The formalized problem is identified as unsolvable if the symbolic solver does not terminate in producing a valid answer (it may produce a symbolic answer). 

> As for the 3600 problems whose formalizations are judged to be inaccurate, this is because the numerical answer computed by the solver does not match the ground truth answer in MATH?
> 

Yes.

> Can you share numbers as to how many problems from each level 1-5 in MATH fall under the 822 or 3600?
> 

Yes. The detailed results are shown in the following.

| Level 1 | Level 2 | Level 3 | Level 4 | Level 5 | Total |
| --- | --- | --- | --- | --- | --- |
| 45 | 46 | 115 | 137 | 479 | 822 |
| 198 | 574 | 746 | 869 | 1250 | 3637 |
I thank the authors for their response which has addressed most of my questions.

>  In the MATH dataset, 822 problems are fully unsolvable by the symbolic solver, hence we bypass solution verification for these cases. As to ~3600 problems with inaccurate formalizations, although their formal versions are inconsistent to original versions, they can still serve as seed problems for subsequent mutation, and solution verification is still conducted. 

By this, you mean that the symbolic solver does not terminate in producing a numerical answer, right? And as for the 3600 problems whose formalizations are judged to be inaccurate, this is because the numerical answer computed by the solver does not match the ground truth answer in MATH? Can you share numbers as to how many problems from each level 1-5 in MATH fall under the 822 or 3600?