Neuro-Symbolic Data Generation for Math Reasoning

Dear Reviewer XHjb:

Thank 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.

[Weakness #1] False positive rate of autoformalization

We 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.

[Weakness #2] More details about projected MCMC

Thanks for the comments. We will include a more detailed description of projected MCMC in the revision.

[Weakness #3] Scalability of the approach

Sorry 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.

[Question #1] Details of generated solutions

Thanks 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.

# Formalized Problem
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun f (Real) Real)

; Define the piecewise function f(x)
(define-fun f ((x Real)) Real
  (ite (> x 2) (+ (* a x) 3)
    (ite (< x (- 2)) (- (* 2 x) b)
      (- x 5))))

; Assert continuity at x = 2
(assert (= (f 2) (f 2.0000001)))

; Assert continuity at x = -2
(assert (= (f (- 2)) (f (- 2.0000001))))

; Find a + b
(declare-fun sum_ab () Real)
(assert (= sum_ab (+ a b)))

; Solve the constraints
(check-sat)
(get-value (a b sum_ab))

# Symbolic solver 
(-3.0, 3.0, 0.0)

# Informalized problem
Let \
$
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$.

# GPT-4 reasoning paths
For 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.

[Question #2] Details about the choice of interpreted functions

We 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).

[Question #3] Details about symbolic solvers

Yes, 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.

Dear Reviewer upsU:

Thank 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.

[Weakness #1] Compared with other models that have comparable SFT data sizes

We 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.

The 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.

[1] https://huggingface.co/fdqerq22ds/MathScale-Mistral

[2] https://huggingface.co/datasets/Vivacem/MMIQC

[Question #1] Cost of data synthesis

The 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.

Dear Reviewer BS8K:

Thank 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.

[Weakness #1] Limitations of the user-specified structure

We 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.

[Weakness #2] Combining the method with tool-use framework

We 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.

[1] MAmmoTH: Building Math Generalist Models through Hybrid Instruction Tuning. ICLR 2024.

[2] ToRA: A Tool-Integrated Reasoning Agent for Mathematical Problem Solving. ICLR 2024.

[Weakness #3] Definitions of validity and diversity

Thanks 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.

To 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.

(\text{M}_3)\\left\\{ \\begin{array}{l} a(b+c) + z_1 = 152 \\\\ b(c+a) - z_2 = 162 \\\\ c(a+b) = 170 \\\\ a, b, c \in \mathbb{N}^+ \\end{array} \\right.

If 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.

[Question #1] Results of catastrophic forgetting

Thanks 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.

Dear Reviewer bEBk:

Thank 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.

[Weakness #1] Examples and costs of the whole pipeline

For the conversion from natural language to SMT-LIB language, we have included an example of autoformalization, mutation, and informalization in Appendix E (Example 2).

The 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.

The 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.

[Weakness #2] Compared with tool-used methods

We would like to clarify that our method is fundamentally different from tool-used methods.

Our 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.

However, 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.

[Weakness #3] Comparison on the same data amount

We 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.

For 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.

In 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.

[1] MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models. ICLR 2024.

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

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