Neuro-Symbolic Data Generation for Math Reasoning
Authors: Zenan Li
Zhi Zhou
Yuan Yao
Xian Zhang
Yu-Feng Li
Chun Cao
Fan Yang
Xiaoxing Ma
Venue: NeurIPS 2024 poster (2024)
Keywords: Neuro-symbolic AI
Large language models
Mathemtical reasoning
Data generation
Primary area: natural_language_processing
TL;DR: A neuro-symbolic framework generating high-quality and supervised mathematical datasets

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.

Neuro-Symbolic Data Generation for Math Reasoning
Zenan Li
Zhi Zhou Yuan Yao!
Yu-Feng Li'
Chun Cao Fan Yang² Xian Zhang?
Xiaoxing Ma'
State Key Lab of Novel Software Technology, Nanjing University, China
Microsoft Research Asia
1i Lizn@smail.ng edu. cn, zhouz@lamar nju. edu. cn, zhxian@microsof crosoft. com, xxmēnju.edee cn
Abstract
A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning inherent, or merely 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-symbont 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 statc-of-the- oft-r---tttttttto- counterparts.
Introduction
Despite recent progress [1 both proprietary and open-source LLMs are still far from satisfactory
in mathematical reasoning 7 It is open question whether LLM's subpar reasoning capability is inherent or due to the the extreme scarcity of high-quality mathematical datasets [3) As an initial step towards answer this question, data generation framework that could create high-quality math datasets is required. To this end, current two lines of research struggle in the diversity dilemma: (I) 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) 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, propose 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 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 I] initiates with the formalization of the original problem expressed via the math symbolic tools. Next. it mutates the formal problem into 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 our mutation
"quual contribution. This work was partially done during Zenan's internship at MSRA.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

problem natural language
Genersted Q & sstural language
Ginceated peoélemu with controlled difficilty levels.
G. rectang e has w withh and length The perfmeter th recbogle 17 units. The legth calrddated usng the equredint flod,
Q: uihh buit tis irttl brother recianguiar wandbox the perimeter
rectangssie ganden has length that 12 more farce If the par meter garden feet. the with gardan fest?
rectongle
the suncioe is fiut and the is
boice the wishh, What the with of the sondboo?
leugth
mulripyy the with
Seed problem
A:
11, subtract St, and
mistake
finall, mubpply reslt
Formalize
Salve
Informalize
actual porimeter's uniss whtth What
givan by snother expressior.
15. The permeter
add
sum the and longn,
peeca saatn Q ar3
ddiciame the deth () uct dacclare the partasten 2xe)
witth of the recbongle
seecli percerten (1 Lit)
Mitale
(mart an1)
Mutate
A-1
rectanglul
lesert langth (a20013))
stath 33 12213
peroetar 1*2 Jength (
seart pertntar Length scotro1
(eech-aat)
gpt-ricu (iddr))
Valialiy of formal muttieer guaranived by solvers Diveriiyy of
Fonmlizedd
Mutsted fornal probiem
ackieved projected MCMCC
Figure 1: The overview of our neuro-symbolic data generation framework. The framework comprises three steps: (1) Formalize the seed problem into its symbolic version. (2) Mutate the symbolic problem to create new variants. (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.
mechanism can properly adjust the complexity of generated problems, and the exposure to more complex math problems can improve the LLM's '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 Markoy chain Monte Carlo technique 14 15
HR (Reusniigg: steps in Traiming
Rensodin min (%) Teat
6.15
Beqyoning- aloot Density
Origin
12-
66
6.12
Lavd-1
Daval-S
10-
-5
6.00
Level-5
6.0
3.00
0
10
15
#Rensoning-sepp Training
Various Difficully Levels of Mulation
Figure 2: The performance of our proposed mutation mechanism. The first figure illustrates that the generated problems with higher difficulty levels lead more reasoning steps of GPT-4. The second figure shows that the gradual incorporation of more difficult problems consistently improves the LLM's 's reasoning capability.
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 [6] and Mistral-7B [1 significantly outperform the existing open-source counterparts on both GSM8K and MATH datasets, as well as two out-of-domain datasets SVAMP [2] and ASDiv T8]. On the GSMSK dataset, the model fine-tuned on Mistral-7B even outperforms GPT-335-- Turbo (by 2.4%), proprietary model with 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 promising avenue for further enhancing LLMs' mathematical capabilities.
2 Mutation
Compared to existing data generation methods, the key feature of our framework lies in the mutation of math problems within the symbolic space, enabling systematic sampling and symbolic solving. Technically, our mutation mechanism includes several simplification and complication strategies, to control the complexity of the generated math problems. The overall framework of our problem mutation method is summarized in Algorithm I
2

---

Algorithm The overall framework of problem mutation
Input: A seed problem expressed by goal and constraints h1, Nn.
Output: A new problem expressed by goal g' and constraint hi... ii...... Ny.
> Complicate the problem using Projected MCMC 2: Initalize random operations 3 and interpreted functions e/.
1: for = l..... do
3: Mutate g' Bog c(()), A = h; @B; (2;) with parameter 2j.
4: Randomly perturb subset (21....,23) 2n} for < n.
5: Solve the rest subset (2j+1...., F.
6:
if {z1,-.., 2n } is solvable then Instantiate the new problem by {z1, ; 8: Stop the complication process
7:
9: end if
10: end for
Simplicate the problem using SMT tacties 13: Apply the tactic to the problem g' and constraints by....,hiu h1
11: for == do
12: Initalize a random tactic from (simplify, qe, simplify. ...
14: end for
2.1 Formalization
We first provide the formalization of math problems, based which the mutation mechanism is operated. Specifically, we adopt the SMT-LIB language [19], a standard notation compatible with prevalent SMT solvers (e.g.. 73 (2).. CVC5 (1], and MathSAT (22). It can also be easily extended
for symbolic calculators (e.g.. SymPy 2 and numerical solvers (e.g.. SeiPy (24). With SMT-LIB
language, the math problem the following structure enabled:
Goal
= min max solve f(x)
Constraints
: h1 h2 hı h2 ito[le,, h2,
Vx. (x) Da ex() Fx. ei (x) Da 62
61 bd 62 ME {2, ,, <,
Expressions
C c x = En) foo(x)
C1 62 -eft.-
Domains
D: |R/C |
where denotes a constant, denotes an n-dimensional variable, ite denotes the if-then-else structure, loo 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, pre-defined a series of interpreted functions, such as summation binomial, ged, cm, derivate, and integral, which facilitate the formalization of most high-school level mathematical problems (excluding geometry) within the above SMT-LIB language.
2.2 Simplification
We perform simplification by systematically considering expression reduction and constraint reduc- tion, 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 (c.g., x + 0 = I or y + I - æ + y). expression expansion (c.g., (z + 1)a = x² + 2x + 1), and function application (e.g., (I 2) A (y log(z)) y log(2)); we also perform symbolic and numerical computations for further reductions (c.g., g2d(2x, 6y) + 2ged(z, 3y) and sin(T/6) + 0.5).
For constraint reduction, we mainly employ the Gaussian elimination tactic gaussian elim (e.g.. 2 A < I + y S 2 2). To handle the if-then-else term, we apply the elim term ite tactic to decompose by introducing a fresh variable (e.g., ite(s > y, x, > = (k> 2) (x y + k = r) A (x < y k y)). For constraints involving quantifiers, we strive to eliminate them using the qe tactic (e.g., Fy-(y > 0) A (x y = 2). Appendix provides more examples illustrating these simplifications.
3

---

2.3 Complication
To complicate the expressions, straightforward strategy to incorporate additional operators. For example, given an atomic constraint h eι b-] 62, we can introduce an additional expression, denoted by e', and derive more complex constraint = e1 xa (e2 S e²).
a( c) 152
a(b c) = -152 01 (2) blo + a) = =162 02 6 6(22)
b(c + a 162
(M1)
7 (M2)
c(a b) 170
c(a =170 @3 (3
a. a.b.er C N
a, b,b,c E N 21,
E
a(b+c) + 21 = 152
abb d 152
b(c+a) 22
162
c( b(c - 162
da+ = 170
170
= (Ma)
(M₂)
114
d+e 150
= 36
d 78
a, b. N+
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 random mutation may ruin their well-defined structure. Consider the running example problem (M1), 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, introduce three auxiliary variables, denoted by 21, 22, 23, and then mutate the problem as (M2). where @1; (D2, G3 E [+,-,,,+) represent three random operators. Furthermore, we instantiate et, c2 e' by interpreted functions, i.e., ej foo, (21), eg = fo02(22), and cg = f20)(2a). where foo1; foo2, foog are randomly selected from foo(2)
log(z) exp(=) | arcsin(=) .... For our rumning example, we simply choose the identity function for f0ol, foo2, foo3, and set @ = =- 3 +, 3z x. Using symbolic solvers to compute a feasible solution of (21, 22, 23), we derive a new and well-defined problem (Mg).
The subsequent challenge is ensure the diversity of the mutated problems, which now becomes how to make the solutions of auxiliary variables sufficiently diverse. This is essentially 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 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,
reverse the Gaussian elimination with refreshed variables, obtaining the final form (M&), which is then included as a new problem in the dataset.
3 Informalization
Informalization aims to translate a formal problem back to natural language without the loss of soundness [29]. As shown in Example [ 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 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 regarded as a lower bound to the true consistency rate.

---

Example 1: Informalization
(declare-fun sara_shoes_cost Real)
(declare-fun sara_dress_cost ( Real)
(declare-fun sara_total_cost O Real)
(declare-fun rachel_budget O Real)
(assert (= sara_shoes_cost 50.0))
(assert (= sara_dress_coot 200.0))
(assert (= sara_total_cost (+ sara_shoes_cos, sara_dress_cost))
(assert (= rachel_budget (* 2 sara_total
(check-sat)
(get-value (rachel_budget))
Translate the math problem formulated with SMT-LIB back to a natural language problem.
GPT-4 output:
Sara bought a pair shoes for $50.00 and a dress for $200.00. 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 [] we investigate the effects of the following operations, whose detailed examples are available in Appendix
(1) Mutation. Mutation complicates the prob- lem, making the informalization more difficult. Therefore, we first analyze the informalization eπrоr caused by the mutation.
Table 1: Consistency rate of six different opera-
tions used in informalization: (1) Mutation; (2) Few-shot learning: (3) Comment generation; (4) Math-word instruction; (5) Problem modification; (6) Variable refresh. We recommend two patterns (i.e., Pl: 1-5 and P2: 1-3&6), both of which can achieve satisfactory results.
(2) Few-shot learning. Few-shot examples offer a stronger instruction to the LLM, and also in- troduce the randomness when aided by random retrieval.
(3) Comment generation. Recognizing that GPT-4 is unfamiliar with SMT-LIB's prefix ex- pressions, we automatically convert these into the infix format, included as comments.
Ops
(3)
(4)
(5)
(%)
X
x
x
X
X
X
75.6 (-)
/
x
x
X
X
X
41.6 (.)
x
x
x
x
76.2 (f)
(4) Math-word instruction. one more sentence "Ensure be math word problem" in the prompt. With this instruction, informalization tends imbue digits with some practical meaning (e.g..7 + one week).
We simply append
/
x
x
x
87.6 (1)
P1
x
90.5 (1)
x
x
97.1 (?)
(5) Problem modification. For mutated problems, rather than generating new informalization, prompt GPT-4 to modify the original informalization result.
(6) Variable refresh. We standardize the naming of all introduced variables (c.g., rachel_budgee + 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 Table I] where the results are evaluated on 1,000 problems randomly sampled from GSM8K. The basic pattern in Example 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 be pure math problems.

---

Experiments
In this section, we conduct a series of experiments to answer the following four research questions:
RQI: Efficacy Using 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-an data generation framework?
RQ3: Generability - Is the effecitveness achieved by our framework due to potential data contami- nation introduced during the generation process?
RQ4: Scalability With more data generated, can our approach continually effective further improving model performance?
4.1 Experimental Setup
Dataset. We conduct our data generation on the training sets of two popular mathematical reasoning benchmarks: GSM8K [10] and MATH (T]). GSM8K is 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, Numher Theory, Counting and Probability, Geometry, Intermediate A 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 [2] and ASDiv [8) 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 ofat--of-the-ar open- open-source mathematical reasoning models, including WizardMath [30,, MuggleMATH [3I], MAmmo (32), and MetaMath [33]. We also conduct thorough comparison between our math generation method and the bootstrapping method employed in MetaMathQA [3],
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-O. 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, create datasets across five levels of difficulty, with 30K examples at level-O and 100K examples for the remaining four levels. As for the MATH dataset, 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 be referred to Appendix [ In total, we generated 860K math problems based on the proposed framework to construct our dataset.
establish four levels of difficulty, where level-0, level-1, level-2, and
Each generated math problem consists of 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 Appendix [
4.2 Empirical Results
RQ1: Efficacy. Using the generated math dataset, we fine-tune the ILaMA-2 base models of 7B and 13B parameter sizes, as well as the Mistral base model. The fine-tuned models, as well as the comparison methods, are evaluated on the GSM8K and MATH datasets.

---

Table 2: Performance comparison among existing mathematical reasoning models fine-tuned on three base models (LLaMA-2 7B, LLaMA- 13B, and Mistral 7B). The best performance is in bold. The delta performance between our model and other SOTA LLMs on each dataset is also reported.
LLaMA-2 7B Base
LLaMA-2 13B Base
Mistral 7B Base
Model
#Dataset
GSM8K
MATH
GSM8K
MATH
GSM8K
MATH
WizardMath
>240K
54.9
10.7
63.9
14.0
83.2
33.0
MuggleMATH
157K
68.4
8.4
74.0
9.4
MAmmoTH
260K
50.5
10.4
56.3
12.9
61.9
17.5
MetaMath
395K
66.5
19.8
72.3
22.4
77.7
28.2
Ours
860K
79.0
30.4
84.1
33.7
86.8
37.3
A
10.66
10.6
10.1
f 11.3
3.6
4.3
1 Model performance is re-evaluated using Pass@) of CoT prompt.
As shown in Table 2 our approach achieves the best performance among the baseline models across different model scales. Compared to LLMs with the LLAMA-2 7B base model, our model demonstrates fair improvement accuracy, surpassing them by at least 10.6% the two datasets. For our model fine-tuned using the LLAMA-2 13B base model, our model achieves an accuracy of 84.1% % and 33.7%, outperforming existing SOTA model by 10.1% and 11.3%. When fine-tuned on the Mistral 7B base model, our model still attains the best performance with an increase in accuracy of 3.6% and 4.3%, respectively. Notably, our model even slightly outperforms GPT-3.5-Turbe (80.8% and 34.1 %) by 6.0% on the GSM8K dataset and 3.2% on the MATH dataset.
In addition 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 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 GSMSK dataset (which emphasizes knowledge reasoning but involves simpler calculations).
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, expand the MATH data of the MetaMathQA dataset 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.
RQ2: Efficiency. To illustrate the data efficiency of our method, we carryy
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 11 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 series of analysis about the potential data contamination or overfitting issues. We first use the memorization detection method introduced 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 no evidence that the mutation contaminates the test set.
Second, in addition to the two oft-of distriiibtt datasets SVAMP and ASDiv, we conduct exper- iments on another benchmark Val [9] which avoids the leak of test set through dynamically generating new benchmarks. The results of our models, alongside those of the comparison models, provided in Appendix E.3 In summary, models demonstrated superior performance in 11 out
7

---

Table 3: Comparison between our method and MetaMathQA (MMQA) with the same data bud- gets. The models are fine-tuned using LLaMA-2- 7B base model, and evaluated GSM8K, MATH, SVMMP, and ASDiv datasets. The results illusrate the high quality of our generated data.
Figure 3: BLUE scores between the output of our fine-tuned model, versus the ground- truth solution and GPT-4 output. The model fine-tuned the Mistral 7B base model, and MetaMath Mistral 7B model is also included as reference. The results show that our method does not induce data contamination.
Training Datasct
Performance Math
Method
GSMSK
Math
GSMSK
SVAMP
ASDiv
Traning
MMQA
240K 240K
0K
66.1
5.8
61.7
72.5
Ours
0K
72.7
8.2
78.8
79.2
MMQA
OK
155K
28.6
19.9
49.0
61.0
Ours
OK
155K
42.1
22.0
73.4
64.1
1:2.1
Test Set
MMQA
240K 240K
155K
67.5
21.7
64.1
76.0
MINQUA
Oen
Ours
155K
6.2
1:1.7
21.1
5.0
BLUU
MMQA*
OK
430K
35.0
25.6
66.4
51.1
64
430K
79.1
19.9
1.32
12.7
19.2
OSte5 07F4
MATII: Ohoenklata
MATI 0P714400444
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 other models.
Finally, we include an additional experiment on the Hungarian High School National Finals Exam dataset (36), whose problems are newly collected 2023. We manually check 33 testing problems based on the provided ground-truth answer, and our model correctly solved 14 problems and partially solved problems, resulting in an exam score of 44. The result is comparable GPT3.5-turbo (i.e.. 41 exam score), conforming the generalizability of our method.
GSMBK
SVAMP
ASDiv
MATH
80
Accuracy (%)
70-
75
70
7-
74-
60
65
70-
60
0
70
140
210
280
350
70
140
210 280
350
0
70 140 210 280 350
0 70
140
210 280 350
Size of Training Dataset (Thousands)
MMQA
Ours
Figure 4: Performance curves of the LLaMA-2-77 models fine-tuned on various scales of datasets. The two datasets are generated by 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 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-77 models are fine-tuned based on these datasets, and the scalability curves are shown in Figure 4 We reference. Since MetaMathQA cannot
also include MctaMathQA with the same data settings 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 our method 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.. 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-39] have comprehensively discussed the current advances in the mathematical reasoning of LLMss. 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. Promet-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 LLMMs can effectively tackle more math problems when provided with simple ofain-of-Though (CoT)) prompt, i.e., "Let's think step by step" 400] 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 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, c.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- 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 TS 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 [ST] trains an LLM to categorize them. Regarding the problem rephrasing, WizardMath 30 proposes 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 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, mutate the problem in the formal symbolic space, resulting in 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 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 (38) 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.
6 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 SMT solver struggles with expressing higher-order concepts like ged 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 [0], MathSAT [22], SymPy, and SciPy, and employ SMT-LIB [19] 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 the problem fusion [Л], which fuses two formal problems into 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 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, 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 fine- tuning. 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.
Broader Impact
The paper aims advance the field of math data generation. There are many potential socictal 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.
7 Conclusion
This paper explores the question of whether sufficient exposure to high-quality mathematical data could enhance LLMs' inherent mathematical reasoning capability. We identify key challenge in balancing diversity and validity in current math problem generation methods. To tackle this challenge. we propose 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 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 L.MSs to accomplish informalization. Through empirical experiments, we demonstrate that our ncuro-symbolic data generation framework significantly enhances the performance of various LLMs in mathematical reasoning tasks, surpassing the current state-of-the-an 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 data generation framework to automatically generate high- 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 be integrated with recent studies (64 which only require problems and final answers.
10

---

Acknowledgment
We appreciate the anonymous reviewers for their valuable insights and helpful comments. This work is supported by the National Natural Science Foundation of China (Grants #62025202), the Frontier Technologies R&D Program Jiangsu (BF2024059), and the Key Program Jiangsu Science Foun- dation (B (BK20243012), Xian Zhang cohxiaanmiccroooff com) and Xiaoxing Ma (xxmênju. edu.cn) are the corresponding authors.
References
[1] Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Advances in Neural Information Processing Systems 35, 2022.
[2] Artur d' Avila Garcez and Luís C. Lamb. Neurosymbolic AI: the 3rd wave. Artificial Intelligence Review, 56(1 56(11))12387-12206 2023.
[3] Wayne Xin Zhao. Kun Zhou, Junyi Li. Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, al. A survey of large language models. arXiv preprint xXiv:23303188223 2023.
[4] Lei Wang, Chen Ma. Xueyang Feng, Zeyu Zhang, Hao Yang. Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, et al. A survey on large language model based autonomous agents. arXiv preprint arXiv:2308. /432, 2023.
[5] Enkelejda Kasneci, Kathrin Seßler, Stefan Küccheman, Maria Bannert, Daryna Dementieva, Frank Fischer, Urs Gasser, Georg Groh, Stephan Günnemann, Eyke Hüllermeier, et Chatgpt for good? on opportunities and challenges of large language models for education. Learning and individual differences, 103:102274, 2023.
[6] Yupeng Chang, Xu Wang. Jindong Wang, Yuan Wu, Linyi Yang, Kaijie Zhu, Hao Chen, Xiaoyuan Yi, Cunxiang Wang, Yidong Wang, et al. survey on evaluation of large language models. ACM Transactions on Intelligent Systems and Technology, 2023.
[7] Xiaoxuan Wang, Ziniu Hu, Pan Lu, Yanqiao Zhu, Jieyu Zhang. Satyen Subramaniam, Arjun R Loomba, Shichang Zhang, Yizhou Sun, and Wei Wang. Scibench: Evaluating college scientific problem-solving abilities large language models. arXiv preprint arXiv:2307. 10635, 2023.
[8] Paulo Shakarian, Abhinav Koyyalamudi, Noel Ngu, and Lakshmivihari Mareedu. An in- dependent evaluation of chatgpt mathematical word problems (mwp). arXiv preprint arXiv:2302. 13814, 2023.
[9] Kaijie Zhu, Jiaao Chen, Jindong Wang, Neil Zhenqiang Gong, Diyi Yang, and Xing Xie. Dyval: Graph-informed dynamic evaluation large language models. CoRR, abs/2309. 17167, 2023.
[10] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichir Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:21 10, 14168, 2021.
[11] Dan Hendryeks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. In Advances Neural Information Processing Systems Track on Datasets and Benchmarks, 2021.
[12] Arkil Patel, Satwik Bhattamishra, and Navin Goyal. Are nlp models really able to solve simple math word problems? arXiv preprint arXiv:2103.07191, 2021.
[13] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.1063 2023.
11

---

[14] Weiming Feng, Kun He, and Yitong Yin. Sampling constraint satisfaction solutions in the local lemma regime. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, pages 1565-1578, 2021.
[15] Zenan Li, Yuan Yao, Taolue Chen. Jingwei Xu, Chun Cao, Xiaoxing Ma, L Jian, et al. Softened symbol grounding for seuro-symbolic systems. In The Eleventh International Conference on Learning Representations, 2023.
[16] Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale. Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami, Naman Goyal, Anthony Hartshorn, Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Maric-Anne Lachaux, Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog. Yixin Nie, Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiao- qing Ellen Tan, Binh Tang. Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, llyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aurélien Rodriguez, Robert Stojnic, Sergey Edunov, and Thomas Scialom. Llama 2: Open foundation and fine-tuned chat models. CoRR, abs/2307. N00822377009288 2023.
[17] Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chap- lot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed. Mistral 7b. CoRR, abs/23 10.06825, 2023.
[18] Shen-Yur Miao, Chao-Chun Liang, and Keh-Yih Su. A diverse corpus for evaluating and developing english math word problem solvers. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 975-984, 2020.
[19] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of lowa, 2017. Available at www. www. WWW-MMMT.BOOO org.
[20] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008.
[21] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strengee smt solver. In International Conference on Tools and Algorithmms for the Construction and Analysis of Systems, pages 415-442. Springer, 2022.
[22] Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. The mathsat 4 smt solver: Tool paper. In Computer Aided Verification: 20th International Conference. CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings 20, pages 299-303. Springer, 2008
[23] Aaron Meurer, Christopher P Smith, Mateusz. Paprocki, Ondřej Čertík, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103, 2017.
[24] Pauli Virtanen, Ralf Gommers, Travis E Oliphant, Matt Haberland, Tyler Reddy, David Courna- peau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, et al. Scipy 1.0: fundamental algorithms for scientific computing in python. Nature methods, ((3))26112722 2020.
[25] Leonardo De Moura and Grant Olney Passmore. The strategy challenge in smt solving. In Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, pages 15 5-44. Springer, 2013.
12

---

[26] Leslie G Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 83)1:100-21,, 1979.
[27] Mark Jerrum and Alistair Sinclair. The markov chain monte carlo method: an approach to approximate counting and integration. Approximation Algorithms for NP-hard problems. PWS Publishing, 1996.
[28] Stefano Ermon, Carla Gomes, and Bart Selman. Uniform solution sampling using a constraint solver as an oracle. In Proceedings of the Twenty-Eighth Conference on Uncertainty in Artificial Intelligence, pages 255-264, 2012.
[29] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368, 2022.
[30] Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. Wizardmath: Empowering mathematical rea- soning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.0955 2023.
[31] Chengpeng Li, Zheng Yuan, Hongyi Yuan, Guanting Dong, Keming Lu, Jiancan Wu, Chuanqi Tan, Xiang Wang, and Chang Zhou. Query and response augmentation cannot help out-of- domain math reasoning generalization. CoRR, abs/2310.05506, 2023.
[32] Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen. Mammoth: Building math generalist models through hybrid instruction tuning. CoRR, abs/2309.05653,, 2023.
[33] Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309.1 /2284, 2023.
[34] Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. Advances in Neural Information Processing Systems, 35:3843 3857, 2022.
[35] Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311-318, 2002.
[36] Keiran Paster. Testing language models held-out high school national finals exam. https httpe///ttttttttteeeee//r/aaaaae htwp:nngrrraannnninnn_iaaa htw_asssssaaa_seaaa_aaaea_e 2023.
[37] Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. Large language models for mathematical reasoning: Progresses and challenges. Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics, pages 225-237, 2024.
[38] Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Compulational Linguistics, pages 14605-14631, 2023.
[39] Pan Lu, Hritik Bansal, Tony Xia, Jiacheng Liu, Chunyuan Li, Hannaneh Hajishirzi, Hao Cheng, Kei-Wei Chang, Michel Galley, and Jianfeng Gao. Mathvista: Evaluating mathematical reasoning foundation models visual contexts. Proceedings of the 12th International Conference Learning Representations, 2024.
[40] Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems, pages 22199-2011 13211,,,, 2022.
13

---

[41] Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoe V. Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consisteney improves chain of thought reasoning in language models. In Proceedings of the 11th International Conference on Learning Representations, 2023.
[42] Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoe V. Le, and Ed H. Chi. Least-to-nes most prompting enables complex reasoning in large language models. In Proceedings of the I Ith International Conference Learning Representations, 2023.
[43] Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. Decomposed prompting: A modular approach for solving complex tasks. In Proceedings of the I 1th International Conference on Learning Representations, 2023.
[44] Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. Chain-of-thoute prompting elicits reasoning in large language models. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave. K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems, pages 24824-24837 2022.
[45] Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. Complexity prompting for multi-step reasoning. In Proceedings of the 11th International Conference on Learning Representations, 2023.
[46] Zhuosheng Zhang, Aston Zhang, Mu Li, and Alex Smola. Automatic chain of thought prompting in large language models. In Proceedings of the 1 11th International Conference on Learning Representations, 2023.
[47] Pan Lu, Liang Qiu, Kai-Wei Chang, Ying Nian Wu, Song-Chun Zhu, Tanmay Rajpurohit, Peter Clark, and Ashwin Kalyan. Dynamic prompt learning via policy gradient for semi-structured mathematical reasoning. In Proceedings of the 11th International Conference on Learning Representations, 2023.
[48] Xijie Huang, Li Lyna Zhang, Kwang-Ting Cheng, and Mao Yang. Boosting I1m reason- ing: Push the limits of few-shot learning with reinforced in-context pruning. arXiv preprint WiXi:2332.00890 2023.
[49] Lucie Charlotte Magister, Jonathan Mallinson, Jakub Adámek, Eric Malmi, and Aliaksei Severyn. Teaching small language models reason. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics, pages 1773-1781, 2023.
[50] Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. Scaling relationship on learning mathematical reasoning with large language models, 2023.
[51] Peiyi Wang, Lei Li. Liang Chen, Feifan Song, Binghuai Lin, Yunbo Cao, Tianyu Liu, and Zhifang Sui. Making large language models better reasoners with alignment. CORR, 0ls/2309.02144, 2023.
[52] Yixuan Weng, Minjun Zhu, Fei Xia, Bin Li, Shizhu He, Shengping Liu, Bin Sun, Kang Liu, and Jun Zhao. Large language models are better reasoners with selff-eeriiiaation. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages
2023.
[53] Weisen Jiang, Han Shi, Longhui Yu, Zhengying Liu, Yu Zhang, Zhenguo Li, and James T Kwok. Borward-backwand reasoning in large language models for mathematical verification. arXiv preprint 2rXivv2308..07558 3, 2023.
[54] Chen Li, Weiqi Wang, Jingcheng Hu, Yixuan Wei, Nanning Zheng, Han Hu, Zheng Zhang and Houwen Peng. Common 7b language models already possess strong math capabilities. CoRR. abs/2403.04706, 2024.
[55] Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W. Cohen. Program of thoughts prompt- ing: Disentangling computation from reasoning for numerical reasoning tasks. Transactions on Machine Learning Research, 2023.
14

---

[56] Luyu Gao, Aman Madaan, Shuyan Zhou, Uni Alon, Pengfei Liu, Yiming Yang. Jamie Callan, and Graham Neubig. PAL: program- aooram-aadeed language models. In Proceedings of the 40th International Conference on Machine Learning, pages 10764-10799, 2023.
[57] Ke Wang, Houxing Ren, Aojun Zhou, Zimu Lu, Sichun Luo, Weikang Shi, Renrui Zhang, Linqi Song, Mingjie Zhan, and Hongsheng Li. Mathcoder: Seamless code integration in Ilms for enhanced mathematical reasoning. arXiv preprint arXiv:2310.0373: 2023.
[58] Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't 't trust: Verify grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference Learning Representations, 2024.
[59] Zhibin Gou, Zhihong Shao, Yeyun Gong, Yujiu Yang. Minlie Huang. Nan Duan, Weizhu Chen, et al. Tora: A tool-integrated reasoning agent for mathematical problem solving. arXiv preprint arXiv:2309. 17452, 2023.
[60] Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Cve4, In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, pages 171-177. Springer, 2011.
[61] Dominik Winterer, Chengyu Zhang, and Zhendong Su. Validating smt solvers via semantic fusion. In Proceedings of the 4 ACM SIGPLAN Conference on programming language design and implementation, pages 718-730, 2020.
[62] Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Proceedings of the 26th annual international conference on machine learning, pages 41-48 2009.
[63] Petru Soviany, Radu Tudor Ionescu, Paolo Rota, and Nicu Sebe. Curriculum learning: A survey. International Journal of Computer Vision, 13066):156-15655 2022.
[64] Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Alphamath almost zero: process supervision without process. arXiv preprint arXiv:2405.00 03555,, 2024.
[65] Tim Dettmers, Artidoro Pagnoni, Ari Holtzman, and Luke Zettlemoyer. Qlora: Efficient finetuning of quantized 1lms. In Advances in Neural Information Processing Systems, 2023.
[66] Edward J. Hu, Yelong Shen, Phillip Wallis. Zeyuan Allen-Zhne Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. In Proceedings of the Ith International Conference on Learning Representations, 2022.
[67] Rohan Taori, Ishaan Gulrajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B Hashimoto. Stanford alpaca: An foolloiti llama model. Technical report, 2023.
[68] Marco Gario and Andrea Micheli. Pysmt: solver-agnoste library for fast prototyping of smt-based algorithms. In SMT Workshop 2015, 2015.
[69] Charles R Harris, K Jarrod Millman, Stéfan Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapaau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J Smith, et al. Array programming with numpy. Nature, 585(7825):357-66,, 2020.
[70] Zhoulai Fu and Zhendong Su. Xsat: a fast floating Moiti satisfiability solver. In Computer Aided Verification: 28th International Conference, CAV 2016. Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part 11 28, pages 187-209. Springer, 2016.
[71] Mare Fischer, Mislav Balunovic, Dana Brachsler-Cohen. Timon Gehr, Ce Zhang, and Martin Vechev. DI2: training and querying neural networks with logic. In International Conference on Machine Learning, pages 1931-1941. PMLR, 2019.
[72] Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, L Jian, et al. Learn- ing with logical constraints but without shorteut satisfaction. The Eleventh International Conference Learning Representations, 2022.
15

---

[73] Jacob Devlin, Ming- Sing-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint 2018.
16

---

A Broader Impacts
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.
B Examples of Simplification
Example 2: Simplification strategy on Problem (No. 41) of the GSM8K dataset.
Autoformalization:
Translate the natural language problem into SMT-LIB language: "Sara bought pair of shoes for $50.00 and a dress for $200.00. Rachel has twice the amount that Sara spent in total, how much is Rachel's budger?"
GPT-4 output:
(declare- sara_shoes_cost () Real)
(declare-fun sara_dress_com cost O Real)
(declare-fun sara_total_cost
Real)
(ueclare-fun rachel_budget () Real)
(assert (= sara_shoes_cost 50.0))
(assert (= sara_dress_cost 200.0))
(assert (= sara_total_cost (+ sara_shoes_cost sara_dress_coot))
(assert (= rachel_budget (* sara_total_cost))
(check-sat)
vget-value (rachel_budget))
Mutation Informalization:
(declare- sara_dress_cost () Real)
(declare-fun sara_shoes_cost () Real)
(ueclare-fun sara_total_cost
Real)
(assert (= sara_dress_cost 200.0))
(assert (= sara_shoes_coot 50.0))
(assert (= sara_total_cost (+ sara_shoes_cost sara_dress_cost))
(check-sat)
(get-value (sara_total_cost))
Translate the math problem formulated with SMT-LIB back to a natural language problem.
GPT-4 output:
Sara went shopping and bought a dress for $200.00 and a pair of shoes for $50.00. What is the total amount Sara spent on her shopping trip?
We elucidate the simplification strategy through Example 2 which selected from the GSM8K dataset. In this formal problem, solving and removing variable (e.g., pachel_budgett = 500). Then, we derive the new problem with its informalized version. Furthermore, we present another example, specifically Example 3 sourced from the MATH dataset. Here, the new problem is generated through the simplification strategy that randomly performs some calculations.
conduct step of Gaussian climination, i.c., randomly
C Examples of Informalization
Various prompts yield different styles of informalization. To illustrate this, provide two specific examples as follows. In Example we do not refresh the variable, and instruct the informalization by adding the prompt "Ensure to be math word problem." The result of GPT-4's informalization tends
17

---

Example 3: Simplification strategy Problem (No. 496) of the MATH dataset.
Autoformalization:
Translate the natural language problem into SMT-LIB language: "Compute SWddipllaystyle
(Ir4:22+4-8114422--0 (448116-22244-112255
GPT-4 output:
(declare- num ( Real)
(declare-fun den () Real)
(declare-fun fraction
Real)
Define the numerator and venominator expressions
(assert (= num (+ 2 (- 8) 16 32 (- 64))))
(assert (= den (+ 4 (- 16) 32 64 (- 128)))
the numerator divided by the denominator (assert (= fraction (/ num den))) (check-sat)
Define the fraction
(get-valus (fraction))
Mutation Informalization:
(declare- fun num () Real)
(declare-ful den () Real)
(declare-fun fraction () Real)
Define the numerator and denominator expressions
(assert (= num (+ (- 2) 16 (-32))))
(assert (= den (+ (- 4) 32 (- 64))))
the numerator divided by the denominator (assert (= fraction (/ num den)))
Define the fraction
(check-sat)
(get-value (fraction))
Translate the math problem formulated with SMT-LIB back natural language problem.
GPT-4 output: Calculate the value of the fraction M\lfrrcc-22 16 32) (-4 + 32 - 64)1)).
to envelop the problem with common knowledge, culminating in the creation of a math word problem. In contrast, 5xample[]involl refreshing each variable and eliminating the prompt "Ensure is math word problem. Hence, its corresponding informalization renders the new problem more abstract and devoid of extraneous elements.
D Additional Experimental Details
Generation Details. In the GSM8K dataset, each problem can be accurately formalized into the SMT-LIB format and successfully mutated into new version. However, some problems, particularly the precalculus and geometry categories of MATH dataset, cannot be formalized or mutated effectively. Overall, out of total of 7,500 problems, 822 cannot be formalized into the SMT-LIB format, and approximately 3,600 formalizations are inaccurate although they remain usable for the data generation. To address this issue, strategically added proportional number of mutated problems derived by directly prompting GPT-4, bypassing solution verification. The detailed counts of these problems are presented in Table 4
Training Details. In this paper, we fully fine-tune the LLAMA-2-7B and ALLAMA-2-13B models using four H800 NVIDIA GPUs. Each model is trained for epochs with a batch size of 128 and
learning rate of 2e-5. For the fine-tuning of the LLAMA-2-55 A-02 model, we adopt the QLoRA (65) method with learning rate of 1e-4. The rank and alpha of LoRA (66) are set to 96 and 16. respectively, with dropout rate of 0.05 between two matrices. The LoRA modules are added to both the attention and MLP layers. The 70B model is fine-tuned using eight A800 NVIDIA GPUs.
18

---

Example 4: Informalization be math word problem (Problem No.14 in GSM8K).
(declare-fur grees_per_minutee () Real)
(declare-fun total_pages () Int)
(declare-fun time_hours () Int)
(assert (= geses_per_minute (/ 2 5)))
(assert (= total_pages 144))
(time_hours (((total_pages
pages_per_minuts 1/60) 1/2))
(assert (= time_hours (* (* (/ total_pages pages_per_ _
(/ 60)) (/ 2))))
(check-sat)
(get-value (time_hours))
Translate the math problem formulated with SMT-LIB back to a natural language problem. Please ensure to be math word problem.
GPT-4 output:
Jamie has book with 144 pages that she wants to read. She reads at pace of 2/5 pages per minute. If she reads for half the time it would normally take her to read the book at this pace, how many hours will she have read?
Example 5: Informalization to be a pure math problem (Problem No. 14 in GSM8K).
(declare-fun x_0 () Real)
(ueclare-fun x_1 () Int)
(ueclare-fun x_2 () Int)
(assert (= x_0 (/ 5)))
(assert (= x_1 1))
(x_2 (2/5 x (x_1 / x_0)))
(assert (= x_2 (+ (/ 2 5) (/ x_1 x_0)))>
(check-sat)
(get (x_2))
Translate the math problem formulated with SMT-LIB back natural language problem.
GPT-4 output:
A fraction representing a number is 2/5. If you have the number 1 and you want to find out how many times this fraction fits into what would be result?
Prompt 1:
Training Prompt
Below is an instruction that describes task. Write a response that appropriately completes the request.An An in ### Instruction:nn An instruction Innnfff Response:ln
Table 4: Detailed count of problems generated by GPT-4 and mutated during the generation process of the MATH dataset. The numbers 1-7 correspond to Algebra, Counting and Probability, Geometry, Intermediate Algebra, Number Theory, Prealgebra, and Precalculus, respectively.
Category
3
4
5
6
Total
# LLM generated
20.4K
9.2K
6.4K
15,4K
8.4K
12.4K
7.8K
80K
# Mutated
97.4K
36,2K
31.2K
60.3K
40.7K
59.2K
24.1K
350K
When fine-tuning the Mistral 7B model. the same training settings LLAMA-2-7B are used, except
19

---

for the learning rate, which is set to 5e-6. Moreover, we adopt the instruction template Prompt used Alpaca [67] for fine-tuning each model.
Prompt 2: Testing Prompt
Below is an instruction that describes task. Write a response that appropriately completes the request. Anknthi Instruction:ln (instruction Innniiii Response:An
Evaluation Details. We evaluate each fine-tuned model using 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. addition, the SymPy expressions are also encoded NumPy [69] functions, thereby enabling the using of SciPy's optimization modules, such as differentialeevoll fuzzy-logic-likk strategy [70H72] in the encoding, which combines the equalities and inequalities into a loss function, subsequently enabling optimization methods for problem-sole sollvng tasks.
and minimize. Note that we introduce a
E
Additional Experimental Results
E.1
Detailed results on MATH dataset
We present detailed results across different categories in the MATH dataset in Table The numbers 1-7 correspond 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, ged, lcm, etc.) are included in our framework. However, Precalculus and Geometry still well-supported. For example, the concept of triangle cannot currently be correctly expressed in the SMT-LIB format, resulting in relatively low improvement rates.
Table 5: Comparison of performance between MetaMath and our method across different categories of MATH dataset. The used base model Mistral-7B. The best performance is in bold.
Category
5
MetaMath
41.4
23.6
15.4
20.7
47.9
15.3
22.5
Ours
59.6
35.4
16.4
32.8
58.5
18.5
25.0
A
+18.2
+11.8
+1.0
+12.1
+10.6
+3.2
+2.5
E.2 Comparison tool-based methods
We compare our model with the tool-based models in Table 6 Although rool-based models achieve good performance with tools, they meet severe performance degradation when tools are not available. This result indicates that training model using code-based and language- 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, tool- based methods offer certain advantages due to their utilization of the strong capabilities of external tools. For datascts that emphasize knowledge reasoning but involve simpler calculations, such the
rationales does not
20

---

Table 6: Performance comparison among tool- methods and our methods. We report the performance of tool-based methods w/ and w/o tools. The best performance is in bold.
Model
Base Model
GSM8k
MATH
Tora
LLaMA2-7B
68.8
40.1
MAmmo TH
LLaMA2-7B
53.6
31.5
HAmmooT((we)) tools)
LLaMA2-7B
50.5
10.4
Tora
CodeL.LaMA-7B
72.6
44.6
MAmmo T'H
CodeLLaMA-77
59.4
33.4
HoammoTH((wi))) tools)
CodeLLaMA-77
22.1
7.6
MAmmoTH
Mistral-7B
75.0
40.0
MAmmoTH(w/o tools)
Mistral-7B
61.9
17.5
Ours
LLaMA2-7B Mistral-7B
79.2
28.8
Ours
86.8
37.3
GSM8K dataset, they underperform our proposed methods, proving that their reasoning ability is still inadequate.
E.3
Experiments on Dy Val Datasets
We also compare our models and existing mathematical reasoning models using Va 9 datasets further evaluate the generalization ability of our models. Dy 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 (2, 2), (3, 2). (3, 3), (4, 2). The performance comparison between models fine-tuned on LLaMA2-7B and Mistral- -B are respectively shown in Table 7 and Table 8) The results show that models achieve the best performance in 1 11/12 cases and give competitive performance in the remaining one case. As the complexity increases, our models achieves a relatively robust performance compared with the other models.
Table 7: Performance comparison of models fine-tuned LLaMA2-7B using Dy datasets with four complexity levels and three graph orders. The best performance is in bold.
Arithmetic Topo
Arithmetic-
Arithmetic-Ran
Model
D1
D2
D3
D4
D1
D2
D3
D4
D1
D2
D3
D4
WizardMath
74.0
55.4
21.4
19.9
71.0
50.6
23.2
7.8
74.2
49.0
10.7
MAmmoTH
77.3
35.1
13.7
8.1
81.8
27.7
13.1
4.8
78.3
26.4
12.7
3.8
MetaMath
91.9
48.0
20.3
16.9
90.5
50.5
18.1
5.8
90.2
41.0
17.9
7.4
Ours
99.7
85.7
66.8
62.5
99.1
75.8
39.8
18.1
98.8
71.4
41.2
19.0
Table 8: Performance comparison of models fine-tuned Mistral-7B using Val datasets with four complexity levels and three graph orders. The best performance bold.
Arithmetic- Topo
Arithmetie-
ArithmetieRRame
Model
DI
D2
D3
D4
DI
D2
D3
D4
D1
D2
D3
D4
MAmmoTH
90.2
66.7
29.9
32.8
92.2
64.8
25.3
18.8
91.0
62.2
23.9
18.2
MetaMath
97.8
75.7
43.0
45.6
99.5
78.6
45.6
37.2
98.3
76.3
44.6
38.8
Ours
99.6
91.3
74.0
71.5
99.3
85.4
56.8
49,2
98.4
87.5
68.6
47.2
E.4
Diversity Gain across Various Difficulty Levels
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 in MetaMath [33 to compute diversity
21

---

gain but use the BERT model [73] as 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.
Level-
Level-2
Level-3
Level-4
Mix
6,34
6.33
6.51
Diversity Gain
3:85
5.75
5.34
5.33
5.34
5 4.89
4.89
4.88
35K Data Budget 70K Data Budget 100K Data Budget Figure 5: The diversity gain across all difficulty levels. The results indicate that the diversity gain of the Mix version continues to increase and reaches the highest compared with alternatives as the data budget increases.
22

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The abstract and introduction clearly state our claims.
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 perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results
be expected to generalize other settings.
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
The limitation 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 not discussed in the paper.
The authors are encouraged to create 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 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 few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low images are taken in low lighting. Or speech-to-text system might 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 address problems of privacy and faimess.
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 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question:
For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
23

---

Justification: N/A.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibiliyy
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: Details of data generation, training and inference process are discussed in Appendix[] We will public the code, as well as the fine-tuned models, for the reproducibility.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
24

---

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:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips..
public/guides//Cdeeiiiiee Sttps//oooooeummmsssooooooooioi siiooollcyy for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to to reproduce the results. See the NeurlPS code and data submission guidelines (ht
/ bttips.cc/pbbl.. http:ubllc/gguie ctte//giidee//Coeeuuu wwt.ssuumissiiiiioii.. ssionPolicyyy for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Training and test settings are detailed Appendix D Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [No]
Justification: We cannot provide statistical significance of the experiments due to the limited GPU resources.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
25

---

It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: Details of the computer resources used the experiments are provided in
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification:
We have carefully reviewed the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have 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., there a special consid- eration due to laws or regulations in their jurisdiction).
10. 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 no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no socictal impact 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.
26

---

The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is 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 being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there 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 monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The paper does not pose such risks.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have 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 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 best faith effort.
12. Lieenses for existing assets
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?
Question:
Answer: [Yes]
Justification: Code packages and datasets are properly cited.
Guidelines:
The answer NA means that the paper does not 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 URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, |paper swi thcode. com/ conasdatsess has curated licenses for some datasets. Their licensing guide can help determine the license of 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.
27

---

If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification: The paper does not release new assets up now.
Guidelines:
The answer NA means that the paper does not release new assets,
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According the NeurIPS Code of Ethies, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
28


Reviews:
[{"review_id": "w79bpI7JS7", "reviewer": "Reviewer_BS8K", "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.", "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": "N.A.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- relatively well-written, good performance against prior works\n- I especially appreciate the ideo of mutating the problem in a controllable ways, which leads to slightly more transparent LLMs. \n- 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.\n- 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?\n- 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.\n\nMinor:\n- line 157, typo: 'effecitveness' -> 'effectiveness'", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer BS8K:**\n\nThank you for the insightful feedback on our paper.  We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as good writing, good performance, and promising scalability. We have carefully read your review and addressed your concerns as follows.\n\n**[Weakness #1]  Limitations of the user-specified structure**\n\nWe agree that adapting our framework to convert more general mathematical problems into the SMT-LIB format is challenging. One potential solution is integrating our framework with existing theorem provers like Isabelle or Lean. Specifically, we could use Isabelle or Lean to formalize the problem and then employ tactics such as `by smt` in Isabelle or `lean-smt` in Lean to automatically obtain its SMT-LIB version. This could be a future direction to explore.\n\n**[Weakness #2] Combining the method with tool-use framework**\n\nWe appreciate the reviewer’s suggestion, and combining our work with tool-use methods is a promising future direction. Specifically, existing work, such as MAmmoTH [1], has demonstrated that combining the PoT and CoT data can further improve the math problem-solving capability of LLMs. Our initial experiments on AIMO Kaggle competition also confirm it (we achieved top-20 by generating CoT and ToRA [2] data using our approach). We will present a comprehensive analysis of these results in our revision.\n\n[1] MAmmoTH: Building Math Generalist Models through Hybrid Instruction Tuning. ICLR 2024.\n\n[2] ToRA: A Tool-Integrated Reasoning Agent for Mathematical Problem Solving. ICLR 2024.\n\n**[Weakness #3] Definitions of validity and diversity**\n\nThanks for the comment. Given a formal problem, the validity refers to whether the problem is solvable, and the diversity refers to whether the newly generated problem is semantically different to existing problems. We will add more formal explanations for them in the revision.\n\nTo see how the projected MCMC preserves the validity and enhances the diversity, let us start with the M3 problem,  which requires determining auxiliary variables (i.e., $z_1$ and $z_2$) to generate a valid problem. \n\n$$\n(\\text{M}_3)\\\\left\\\\{\n\\\\begin{array}{l}\na(b+c) + z_1 = 152 \\\\\\\\\nb(c+a) - z_2 = 162 \\\\\\\\\nc(a+b) = 170 \\\\\\\\\na, b, c \\in \\mathbb{N}^+\n\\\\end{array}\n\\\\right.\n$$\n\nIf we use the symbolic solver directly, it tends to produce the same result ($a=84, b=1, c=2, z_1 = -100, z_2 = -76$) due to inherent solving biases, causing the newly generated problem duplicated. Projected MCMC first randomly perturbs a variable (e.g., $a=84$ to $a=100$), and then solves the rest variables with the symbolic solver ($a=100, b=70, c=1$, $z_1=-6948, z_2=6908$), deriving a new and different problem. We will include the pseudo-code in our revised paper.\n\n**[Question #1] Results of catastrophic forgetting**  \n\nThanks for pointing this out. We evaluate our model and MetaMath model (both fine-tuned on LLaMA-2 7B) on TruthfulQA (zero-shot),  MMLU (zero-shot),  BBH (average score), IFEval (prompt-level acc.), and HumanEval (pass@1). The results are shown as follows and the result of LLaMA-2 7B is also included as a reference. It can be observed that catastrophic forgetting does occur for all tasks except TruthfulQA.  Especially, the performance of code generation is diminished due to the CoT instruction fine-tuning.\n| Model | TruthfulQA ( MC1 ) | MMLU | BBH | IFEval | HumenEval |\n| --- | --- | --- | --- | --- | --- |\n| LLaMA-2 7B | 24.6 | 40.9 | 39.3 | 20.5 | 13.7 |\n| MetaMath | 27.6 | 32.9 | 36.6 | 14.0 | 0.0 |\n| Ours | 27.0 | 30.4 | 36.5 | 15.5 | 0.0 |", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "k5TBNhJ8yP", "reviewer": "Reviewer_bEBk", "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.", "questions": "Please refer to the weaknesses", "limitations": "None", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1.the proposed framework is promising to both guarantee the diversity and accuracy of the synthetic mathematical data, based on the formal language. \n\n2.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?\n\n2.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?\n\n3.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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer bEBk:**\n\nThank you for the valuable feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as promising framework and effective approach. We have carefully read your review and addressed your concerns as follows.\n\n**[Weakness #1] Examples and costs of the whole pipeline**\n\nFor the conversion from natural language to SMT-LIB language, we have included an example of autoformalization, mutation, and informalization in Appendix E (Example 2). \n\nThe cost of the whole pipeline primarily depends on the calling of GPT-4 (it needs ~1K tokens cost per problem generated). This cost of calling GPT-4 is similar to the compared data generation methods (e.g., MetaMath). Regarding CPU cost, in our experiments, we use a 48-core CPU and take about 770s to mutate 5000 problems from the MATH dataset, i.e., 0.154s per problem. Therefore, this part of the cost is totally acceptable.  \n\nThe human effort required during the formalization stage is minimal, involving manually defining a few uninterpreted functions (e.g., arcsin, arccos, gcd, lcm, and etc.) in advance. Apart from this, our entire data generation pipeline is fully automated.\n\n**[Weakness #2] Compared with tool-used methods**\n\nWe would like to clarify that our method is fundamentally different from tool-used methods. \n\nOur framework uses formal language to formalize the problem, which ensures the problem is well-structured and thus facilitates the mutation. Benefiting from the formalized problem, we can efficiently mutate and verify problems using symbolic solvers (e.g., SymPy) to ensure the diversity and validity of the newly generated problems. \n\nHowever, PAL-like and PoT-like methods prompt the LLM to generate a program for solving the problem. Therefore, these methods are not amenable to mutation with solely programs rather than formalized problems.\n\n**[Weakness #3] Comparison on the same data amount**\n\nWe would like to first clarify that the generated data from different methods may have different convergence rates (i.e., accuracy curves) as the data size grows, which is also confirmed in Appendix E.2 of MetaMath [1]. Therefore, in Table 1, we directly compare different models according to their released datasets and models because we believe each method has already achieved its (near-)best performance.\n\nFor a comparison with equal data size, we have conducted a comparison between our method and MetaMath with the same data budget as an ablation study in Table 3. The result illustrates that our method is still better. \n\nIn addition, we will include the comparison with other models that have significantly large SFT data sizes in the revision, i.e., MathScale and MMIQC [2, 3]. Both MathScale and MMIQC methods generate approximately 2M data to fine-tune the Mistral 7B model. The results below show that our proposed data generation method achieves higher performance with less volume of generated data, demonstrating the efficiency and effectiveness of our proposal. \n\n| Model | #Dataset | GSM8K | MATH |\n| --- | --- | --- | --- |\n| MathScale | ~1,999K | 74.0 | 34.5 |\n| MMIQC | ~2,294K | 60.5 | 36.0 |\n| Ours | 860K | 86.8 | 37.3 |\n\n[1] MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models. ICLR 2024.\n\n[2] MathScale: Scaling Instruction Tuning for Mathematical Reasoning. ICML 2024. \n\n[3] Augmenting Math Word Problems via Iterative Question Composing. ICLR Workshop 2024.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "rNUzQzrphU", "reviewer": "Reviewer_upsU", "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.", "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": "Yes", "rating": 7, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "- The paper is clearly structured and easy to follow.\n\n- 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.\n\n- 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].\n\n [1] MathScale: Scaling Instruction Tuning for Mathematical Reasoning\n\n [2] Augmenting Math Word Problems via Iterative Question Composing", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer upsU:**\n\nThank you for the valuable feedback on our paper. We appreciate the time and effort you have put into reviewing our work and we are grateful for encouraging comments such as the clear paper structure, novel method, solid experiments, and interesting findings. We have carefully read your review and addressed your concerns as follows.\n\n**[Weakness #1] Compared with other models that have comparable SFT data sizes**\n\nWe reproduce the MathScale and MMIQC based on the repositories [1] and [2] based on the Mistral base model. Note that both MathScale and MMIQC methods generate approximately 2M data to fine-tune the Mistral 7B model, while our proposed method only generates 860K data. \n\nThe results show that our proposed data generation method achieves higher performance with less volume of generated data, demonstrating the efficiency and effectiveness of our proposal. We will add these two comparison methods to our final paper. \n\n| Model | #Dataset | GSM8K | MATH |\n| --- | --- | --- | --- |\n| MathScale | ~1,999K | 74.0 | 34.5 |\n| MMIQC | ~2,294K | 60.5 | 36.0 |\n| Ours | 860K | 86.8 | 37.3 |\n\n[1] https://huggingface.co/fdqerq22ds/MathScale-Mistral\n\n[2] https://huggingface.co/datasets/Vivacem/MMIQC\n\n**[Question #1] Cost of  data synthesis**\n\nThe cost of data synthesis mainly depends on the calling of GPT-4 (autoformalization, informalization, and reasoning path generation), it requires ~1K tokens cost for each problem generation. As to the CPU cost, in our experiments, we use a 48-core CPU, and take about 770s to mutate 5000 problems from MATH dataset , i.e., 0.154s per each problem. Hence, this part of the consumption is totally acceptable.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "nz7cgz4JmS", "reviewer": "Reviewer_UMpg", "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.", "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. \n\n2. 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. \n\n3. 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": "I believe the authors have adequately addressed limitations of their work.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "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.\n\n2. 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.\n\n3. 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? \n\n2. 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.\n\n3. 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.\n\nTypos:\nLine 69: involes -> involves\nLine 157: effecitveness -> effectiveness\nTable 3 caption: illusrate -> illustrate\nLine 338: repsectively -> respectively", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer XHjb:**\n\nThank you for the valuable feedback on our paper. We appreciate the time and effort you have put into reviewing our work and we are grateful for encouraging comments such as nice idea, significant work, and clear writing. We have carefully read your review and addressed your concerns as follows.\n\n**[Weakness #1] False positive rate of autoformalization**\n\nWe apologize for the confusion about the false positive rate. The consistency check is performed by directly checking the numerical solutions. A false positive refers to that the formal problem is inconsistent with its informalized version while their derived solutions (by symbolic solver and GPT-4, respectively) are consistent. Given the rarity of such instances, a (nearly) zero false positive rate is reasonable. We will further illustrate the definition of the false positive in the revision.\n\n**[Weakness #2] More details about projected MCMC**\n\nThanks for the comments. We will include a more detailed description of projected MCMC in the revision.\n\n**[Weakness #3] Scalability of the approach**\n\nSorry for the unclear statements. 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. The detailed data sizes for purely LLM-generated and mutated problems, along with an ablation study of removing purely LLM-generated data, are presented in Appendix E (Table 4) and Appendix F (Table 5). We will further clarify this in the revision.\n\n**[Question #1] Details of generated solutions**\n\nThanks for the comment. We use the standard setting for the solution generations (CoT prompt, temperature=0.7, top_p=0.95). An example of formalized problem, symbolic solver's solution, informalized problem, and GPT-4's reasoning path is shown in the following.\n```\n# Formalized Problem\n(declare-fun a () Real)\n(declare-fun b () Real)\n(declare-fun f (Real) Real)\n\n; Define the piecewise function f(x)\n(define-fun f ((x Real)) Real\n  (ite (> x 2) (+ (* a x) 3)\n    (ite (< x (- 2)) (- (* 2 x) b)\n      (- x 5))))\n\n; Assert continuity at x = 2\n(assert (= (f 2) (f 2.0000001)))\n\n; Assert continuity at x = -2\n(assert (= (f (- 2)) (f (- 2.0000001))))\n\n; Find a + b\n(declare-fun sum_ab () Real)\n(assert (= sum_ab (+ a b)))\n\n; Solve the constraints\n(check-sat)\n(get-value (a b sum_ab))\n\n# Symbolic solver \n(-3.0, 3.0, 0.0)\n\n# Informalized problem\nLet \\\\[f(x) = \\\\left\\\\{\\n\\\\begin{array}{cl}\\nax + 3, &\\\\text{ if } x > 2, \\\\\\\\\\nx - 5, &\\\\text{ if } -2 \\\\leq x \\\\leq 2, \\\\\\\\\\n2x - b, &\\\\text{ if } x < -2.\\n\\\\end{array}\\n\\\\right.\\\\]\\n\\nDetermine the values of $a$ and $b$ for which the function $f(x)$ is continuous at $x = 2$ and $x = -2$, and then calculate the sum of $a$ and $b$.\n\n# GPT-4 reasoning paths\nFor the function $f(x)$ to be continuous at $x = 2$, the values of the function as it approaches 2 from the left and the right must be the same. Thus the value of the function for $x > 2$ must equal the value of the function for $-2 \\\\leq x \\\\leq 2$ when $x = 2$.\\n\\nSo we set $ax + 3$ equal to $x - 5$ when $x = 2$:\\n\\n$2a + 3 = 2 - 5$\\n\\n$2a = -6$\\n\\n$a = -3$.\\n\\nSimilarly, for $f(x)$ to be continuous at $x = -2$, the values of the function for $-2 \\\\leq x \\\\leq 2$ must equal the value of the function for $x < -2$ when $x = -2$.\\n\\nSo we set $x - 5$ equal to $2x - b$ when $x = -2$:\\n\\n$-2 - 5 = 2(-2) - b$\\n\\n$-7 = -4 - b$\\n\\n$b = 3$.\\n\\nNow that we have the values of $a$ and $b$, we can find their sum:\\n\\n$a + b = -3 + 3 = 0$.\\n\\nThe answer is 0.\n```\n\n**[Question #2]  Details about the choice of interpreted functions**\n\nWe apologize for the lack of details. In our implementation, we first identify which functions are used in the problem and then determine the interpreted functions accordingly. For instance, if a problem involves sine functions, the interpreted trigonometric functions will be randomly (and uniformly) selected, while other irrelevant functions (e.g., lcm, gcd) will be excluded. This step is adapted from the theory/logic selection in PySMT (see [the code piece](https://github.com/pysmt/pysmt/blob/master/pysmt/operators.py)).\n\n**[Question #3] Details about symbolic solvers**\n\nYes, SciPy and SymPy are used in our framework. In our implementation, we first serialize the SMT-LIB format into SymPy expression, and then use SymPy `solve` and SciPy `minimize` function to solve the problem. More implementation details are shown in Appendix E.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We thank all the reviewers for their in-depth comments, which urge us improving our paper. We will revise the paper accordingly. Here, we summarize our responses to the major issues raised by the reviewers.

Reviewers **BS8K**, **bEBk**, and **XHjb** request further discussion about tool-use framework. First, our  method is fundamentally different from tool-based methods as we aim to formalize the problems allowing for mutation and verification, which tool-based methods cannot do (shown in response to reviewer **bEBk**). Moreover, combining our method with tool-use framework may further improve the capability of LLMs (shown in response to reviewer **BS8K**). We will present a comprehensive analysis of these results in our revision.

Reviewer **bEBk** and **upsU** question the cost of our method. First, our method is automated, only requiring minimal human effort to define a few uninterpreted functions beforehand. Next, the cost of our method mainly depends on the calling of GPT-4 (~1K tokens cost per problem) and CPU cost of mutation (0.154s per problem on 48-core CPU). Therefore, the cost of our method is totally acceptable and similar to the comparison data generation method. 

Reviewer **BS8K**, **bEBk**, and **upsU** concern about the experiments in our paper. We first would like to clarify that specific data generation methods can determine the final performance. Therefore, we directly compare different methods with their recommended data scales. To further demonstrate the effectiveness of our method, we add two comparison models trained with millions of training samples, i.e., MathScale [1] and MMIQC [2] (shown in response to reviewer **bEBk** and **upsU**). 

Reviewer **BS8K and XHjb** question the details of validity and diversity, autoformalization, projected MCMC, and so on. We have presented the detailed explanations in the corresponding responses. All the details will be further clarified in the revision.

[1] MathScale: Scaling Instruction Tuning for Mathematical Reasoning. ICML 2024. 

[2] Augmenting Math Word Problems via Iterative Question Composing. ICLR Workshop 2024.

Meta-review: 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.
Decision: Accept (poster)