MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

R3Q1. The risk of data contamination.

Thank you for the valuable question. We check cross-contamination between MUSTARDSAUCE and the evaluation datasets inspired by the GPT-4 Technical Report [1]. However, instead of using a substring match that may result in false negatives and false positives, we compute cosine similarities based on text-embedding-ada-002 [3] and then inspect the nearest data points in the paired datasets. The automated theorem proving (ATP) dataset miniF2F only contains formal statements and proofs, while the math word problem (MWP) dataset GSM8K only contains informal statements and proofs. For a more detailed inspection, we check the corresponding fractions in MUSTARDSAUCE. We demonstrate the inspected cases as follows. The nearest data points are dissimilar. Therefore, we exclude data contamination of the generated MUSTARDSAUCE according to these observations.

[1] OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023.

[3] Greene, R., Sanders, T., Weng, L., & Neelakantan, A. (2022). New and improved embedding model. https://openai.com/blog/new-and-improved-embedding-model

MUSTARDSAUCE v.s. miniF2F (cosine similarity = 0.6439)

MUSTARDSAUCE Case

Informal Statement: Alex has 5 ten-dollar bills and 3 one-dollar bills. How much money does Alex have in total?

Informal Proof: To find out how much money Alex has in total, we need to multiply the number of each type of bill by its value. So, Alex has 5 ten-dollar bills, which equals 5 * 10 = 50 dollars. He also has 3 one-dollar bills, which equals 3 * 1 = 3 dollars. Adding these two amounts together gives 50 + 3 = 53 dollars. Therefore, Alex has 53 dollars in total.

Formal Statement and Proof:

def calculate_money (tens : ℕ) (ones : ℕ) : ℕ := tens * 10 + ones * 1

example : calculate_money 5 3 = 53 :=
begin
  rw calculate_money,
  refl,
end

miniF2F Case

theorem algebra_sqineq_unitcircatbpamblt1
  (a b: ℝ)
  (h₀ : a^2 + b^2 = 1) :
  a * b + (a - b) ≤ 1 :=
begin
  nlinarith [sq_nonneg (a - b)],
end

MUSTARDSAUCE v.s. GSM8K (cosine similarity = 0.5975)

MUSTARDSAUCE Case

Informal Statement: Given two vectors u = (u1,u2) and v = (v1,v2) in R^2, prove that the operation of vector addition, defined as u + v = (u1+v1, u2+v2), is commutative. That is, prove that for all u and v in R^2, u + v = v + u.

Informal Proof: We can prove this by direct computation. Given the vectors u = (u1, u2) and v = (v1, v2), we have: u + v = (u1 + v1, u2 + v2) and v + u = (v1 + u1, v2 + u2). Since addition is commutative in R (the set of all real numbers), we have u1 + v1 = v1 + u1 and u2 + v2 = v2 + u2. Thus, we conclude that (u1 + v1, u2 + v2) = (v1 + u1, v2 + u2), which means that u + v = v + u.

Formal Statement and Proof:

import data.real.basic 

variables (u1 u2 v1 v2 : ℝ)

-- defining vectors as pair of real numbers
def vector := ℝ × ℝ
-- defining vector addition
def vadd (u v : vector) : vector := (u.1 + v.1, u.2 + v.2)

-- defining vectors u and v
def u : vector := (u1, u2)
def v : vector := (v1, v2)

-- commutativity of vector addition
theorem vadd_comm : vadd (u u1 u2) (v v1 v2) = vadd (v v1 v2) (u u1 u2) :=
begin
  unfold vadd,
  unfold u,
  unfold v,
  rw add_comm u1 v1,
  rw add_comm u2 v2,
end

GSM8K Case

Question: The local firefighters are doing a "fill the boot" fundraiser. Their goal is to raise \$6300. After the first 3 hours, they have raised \\$2100. For how many hours do they have to fundraise in total to reach their goal, assuming an equal amount raised in every hour?

Answer: The fireman raise 2100 / 3 = \$<<2100/3=700>>700 per hour. They have to fundraise for 6300 / 700 = <<6300/700=9>>9 hours.

#### 9

R3Q2. What is the "valid" rate of the generated formal statements and proofs?

Thank you for the question. The "valid" rate, or the "pass rate", is the proportion of generated data (obtained from the 2nd stage of MUSTARD: Proof Generation) that are validated by the Lean Prover (obtained from the 3rd stage of MUSTARD: Proof Filtering).

R2Q7. The inconsistency between the #reduce statements and various theorem proofs.

Thank you for the question. The proportion of proofs with #reduce statements in the current MUSTARDSAUCE-valid set is 19.3%. MUSTARD aims to provide a uniform synthesis of theorem and proof data. Therefore, we have further filtered out the data points with the #reduce statements, which results in 5,922 data points.

R2Q8. The test set GSM8K only covers elementary school-level problems.

Thank you for the valuable question. We have added experiments on the MATH dataset [2] that contain more challenging math word problems, and the results are demonstrated in Table 4 as shown above. Both GPT2-large and Llama 2-7B show significant improvements after fine-tuning with MUSTARDSAUCE-valid. For example, "GPT2-large > va" performs 40% higher than "GPT2-large > ra" in the zero-shot manner. And "Llama 2-7B > va" has an 11.76% increase compared to "Llama 2-7B > ra". The observations further demonstrate the effectiveness of generated and validated MUSTARDSAUCE on math word problems.

[2] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sai-Kit Yeung (eds.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual, 2021.

R2Q4. The effectiveness of this framework for larger LLM models (e.g., 34B or 70B models or GPT3 models) remains to be investigated.

Thank you for the instructive comment. We further conduct experiments on Llama 2-70B. Since the Llama 2-34B and the GPT-3 parameters are not released, we are unable to experiment with these two models. The compared performances between Llama 2-7B and Llama 2-70B are demonstrated in Table 8 below. The results are also updated in Table 28 in Appendix F in the main paper. Due to time limitations, we demonstrate results on GSM8K first. Llama 2-70B fine-tuned with MUSTARDSAUCE-valid performs 9.42% higher than fine-tuned with MUSTARDSAUCE-random in the zero-shot manner, and 6.68% higher in the few-shot manner. The performance gains are more significant compared to the results of Llama 2-7B. Therefore, the proposed framework remains effective with larger fine-tuned language models.

Table 8: Compared performances on GSM8K between Llama 2-7B and Llama 2-70B.

R2Q5. Would the method potentially be more effective if more data points were generated and a larger model was employed for fine-tuning?

Thank you for the constructive comment. Since generating and filtering new data with GPT-4 is costly, we instead use 75%, 50%, 25%, and 0% of current MUSTARDSAUCE-valid for fine-tuning Llama 2-7b to observe the effect of data scalability. We evaluate the model on all datasets. The results are demonstrated in Table 9 as follows. We have also uploaded the results in Figure 3 in the main paper. In general, the results on all datasets increase as the fine-tuning data scales up. Specifically, performances on the MUSTARD-test and mathlib show the most significant growth, and there is no decreasing trend in the growth rate. Therefore we expect further performance improvements when more high-quality data are included.

Table 9: Llama 2-7b performances with different data scales for fine-tuning.

R2Q6. Does the method remain more effective when compared to fine-tuning the model using the entire generated dataset?

Thank you for the valuable comment. We have fine-tuned GPT2-large and Llama 2-7B with the entire generation dataset (contains 28,320 data points in total), and the results are demonstrated in Table 4 and Table 5 in the lines "GPT2-large > tt" and "Llama 2-7B > tt". We have also updated the results and marked them with blue in Tables 4 and 5 in the main paper. We find that the models fine-tuned with the entire generated dataset perform better than those fine-tuned with MUSTARDSAUCE-random and MUSTARDSAUCE-invalid but are still inferior to those fine-tuned with MUSTARDSAUCE-valid. Therefore, more fine-tuning data improves the model performances as usual, but the smaller MUSTARDSAUCE-valid turns out to be more helpful. This finding again demonstrates our motivation that the validated theorem and proof data are of higher quality and are beneficial for reasoning.

R2Q1. The improvement of involving the theorem prover is relatively minor (e.g., see in, ra, and va in Table 4), and it raises the question of whether the best result should be derived from direct fine-tuning without any filtering and sampling.

Thank you for the question. We have further conducted experiments with fine-tuning in the entire generated dataset (28,320 data points, denoted as “total”, tt for short). The results are demonstrated in the revised Tables 4 and 5. We also mark and color code the performance gaps between models fine-tuned with MUSTARDSAUCE-random and MUSTARDSAUCE-valid in the tables. We find that models fine-tuned with the entire generated data are inferior to models fine-tuned with MUSTARDSAUCE-valid. Although the increase in the amount of fine-tuned data makes the model perform better compared to fine-tuning on MUSTARDSAUCE-invalid and MUSTARDSAUCE-random, the model's performance still lags behind that of fine-tuning on smaller amounts but higher quality data. Therefore, our proposed framework that introduces the theorem prover is effective and beneficial.

R2Q2. The subset sampled for manual verification is small.

Thank you for the valuable comments. We expand the manual verification subset by randomly selecting and manually checking another 112 data points. The results of the 200 data points in total are demonstrated in Table 3 as follows. It is shown that the results are consistent with more inspected data. (D4) and (D6) show significant differences in accuracy between the two groups. Moreover, (D1) also shows significance with the inspected data scaled up. The results demonstrate that the validated data have a higher quality than those without a formal validation process.

Table 3: Inspection dimensions and requirements in human evaluation. IS: Informal Statement. IP: Informal Proof. FS: Formal Statement. FP: Formal Proof. RT: Reasoning Type. Significant $p<0.005$ are marked with bold.

R2Q3. The model used for generating the MUSTARD dataset.

We use GPT-4 [1] for generating the MUSTARD dataset. We have added the details to our revised version.

[1] OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023.

Table 4: Maj1@1 results on GSM8K (G) and MATH (M). Zero: Zero-shot. Few: Few-shot. > denotes a fine-tuning step. in: MUSTARDSAUCE-invalid. ra: MUSTARDSAUCE-random. va: MUSTARDSAUCE-valid. tt: The entire generated data. gt: GSM8K training split. The updated results are bold and italic. The values in parentheses are performance gaps between fine-tuning with MUSTARDSAUCE-valid and MUSTARDSAUCE-random.

We sincerely thank the reviewer for all the instructive comments and valuable suggestions. We have added the following experiments to address the corresponding questions.

1. We have further conducted experiments with (1) fine-tuning in the entire generated dataset (denoted as "total", <tt>tt</tt> for short), (2) fine-tuning larger Llama 2-70B, (3) evaluation on another challenging dataset MATH [2], (4) ablation study of data scalability by fine-tuning models with different ratios of data, to further study the benefits of the proposed framework. We have the following findings:

   1. In general, fine-tuning with MUSTARDSAUCE-valid is superior to fine-tuning with MUSTARDSAUCE-invalid, MUSTARDSAUCE-random, and also the entire generated dataset. This indicates the benefits of involving formal validation in our framework.

   2. The performance gaps between MUSTARDSAUCE-valid and MUSTARDSAUCE-random are generally significant. The average performance gain in automated theorem proving (Table 5) is 18.15%, and in math word problems (Table 4) is 6.78%. The results on the MATH dataset indicate that fine-tuning with MUSTARDSAUCE-valid is considerably beneficial. For example, GPT2-large fine-tuned with MUSTARDSAUCE-valid set has a 40% performance gain in a zero-shot manner, and the performance of Llama 2-7B in a few-shot manner increases by 11.76%.

   3. Fine-tuning the larger Llama 2-70B shows greater performance improvements, which demonstrates the scalability of this framework.

   4. The model performances increase as the generated data scales up. Therefore we expect further performance improvements when more high-quality data are included.

   In summary, the extended experiments demonstrate that the proposed method generates high-quality data that are beneficial to improving language models' mathematical reasoning performance. The method is scalable to larger fine-tuned LMs and more generated data points and maintains its effectiveness.

2. We have expanded the sampled subset for manual verification from 88 data points to 200 data points.

3. The LLM we used for generating the MUSTARDSAUCE dataset is GPT-4 [1] and we have added the details in our revised manuscript.

[1] OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023.

[2] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sai-Kit Yeung (eds.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual, 2021.

Please check our detailed results and response in the following.

Dear Reviewer 9Wae,

We sincerely thank you again for your time and effort in reviewing this paper! We also thank you for your positive recognition of our extensive experiments and our contributions, as we quote as follows: "The topic of this paper is of great significance to the mathematical reasoning of large language models, ... This paper offers certain reference value for this field." "Technically, the paper presents several innovations." "The experimental data in this paper effectively demonstrate the value of the data generated by this framework."

Our paper proposes a novel framework MUSTARD that synthesizes high-quality theorem and proof data and further extensively facilitates language models' mathematical reasoning capabilities.

• The human evaluation results on 200 randomly selected data points indicate that the formal validation in MUSTARD makes a remarkable contribution to the data quality (Table 3).
• The extensive experimental results with GPT2-large, Llama 2-7B, and Llama 2-70B on the two word math problem benchmarks (GSM8K and MATH, demonstrated in Table 4) and two automated theorem proving benchmarks (mathlib and miniF2F, shown in Table 5) demonstrate that the generated data significantly facilitates the smaller language models to perform more accurate mathematical reasoning.
• Moreover, the ablation study on data scalability shows consistent performance increases when more data from MUSTARD are introduced, suggesting a great potential for scalability (Table 9 in the previous response and Figure 3 in the revised main paper). Fortunately, MUSTARD reduces the cost of acquiring such high-quality step-by-step complex reasoning data and obtains correct, scalable, and reusable data. Therefore, in future work, we would love to build a community in which all members can join the data synthesis process, and acquire and share more high-quality data with the whole community.

R1Q1. The LLM we used for the informal data generation.

We use GPT-4 [1] for generating both the informal and formal data.

[1] OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023.

R1Q2. How this approach could be scaled to the best performing models.

Thank you for the question. The proposed MUSTARD contains two language models: (1) The large language model (hereinafter the LLM) that is prompt for generating the theorem and proof data, and specifically we use GPT-4 [1] in our experiments; (2) The fine-tuned language model using the generated MUSTARDSAUCE dataset (hereinafter as the fine-tuned LM) for miniF2F, mathlib, and GSM8K, and in our experiments we use GPT-2 and Llama 2. For LLM, we have used the best-performing GPT-4. For fine-tuned LMs, we fine-tune a larger and better-performing model Llama 2-70B with MUSTARDSAUCE. The results are demonstrated in Table 8 as follows. In general, larger fine-tuned LMs achieve more significant performance gains. For example, Llama 2-70B fine-tuned with MUSTARDSAUCE-valid performs 9.42% higher than fine-tuned with MUSTARDSAUCE-invalid in the zero-shot manner, and 6.68% higher in the few-shot manner. The performance gains are higher compared to the results of Llama 2-7B. Therefore, the proposed framework remains effective when scaled to better-performing fine-tuned LMs.

Table 8: Compared performances on GSM8K between Llama 2-7B and Llama 2-70B.

R1Q3. The low value of D3 in Table 3.

As introduced in Section 3.2, MUSTARD generates both theorem-proving problems and math word problems. D3 in Table 3 inspects whether MUSTARD accurately classifies the question types during generation. Specifically, we investigate instances where theorem-proving problems might be misclassified as math word problems, and vice versa, and assess if validation using Lean Prover reduces such misclassifications. We find that the $p$-value of D3 is greater than 0.005, showing that Lean Prover validation does not significantly influence the classification. Furthermore, the proportions in both Group Valid and Group Invalid in D3 are relatively lower than other inspection dimensions. One of the reasons is that MUSTARD generates a diverse range of problems from the elementary to higher educational levels, and generating theorem-proving problems at the elementary school level is specifically challenging.

We thank Reviewer LURb again for your time and effort of reviewing this paper!

We have updated the results of the fine-tuned Llama 2-70B on the MATH dataset, which are demonstrated in Table 8 as follows and also updated to Table 28 in the main paper. Llama 2-70B fine-tuned with MUSTARDSAUCE-valid consistently outperforms the model fine-tuned with MUSTARDSAUCE-random by 8.33% in the zero-shot manner and 5.30% in the few-shot manner. It also surpasses the model fine-tuned with the invalid subset and the entire generated dataset. The results also suggest the effectiveness of the framework when scaled to better-performing fine-tuned LMs.

Table 8: Compared performances on GSM8K and MATH between Llama 2-7B and Llama 2-70B.

Dear Reviewer LURb,

We have expanded the manual verification subset by randomly selecting and manually checking another 112 data points, resulting in 200 verified data points in total, 100 of which pass the Lean Prover (Group Valid) and 100 of which do not (Group Invalid). The results of the 200 data points are demonstrated in Table 3 as follows. With the larger verified subset, we observe that the D3 value of the Valid group becomes on par with the Invalid group. Moreover, the $p$-value of D3 is greater than 0.005, which is in line with our intuition that the Lean Prover does not help the question type classification, as we explained in the previous response that MUSTARD generates a diverse range of problems from the elementary to higher educational levels, and generating theorem-proving problems at the elementary school level is specifically challenging.

More importantly, (D4) and (D6) show significant differences in accuracy between the two groups, which is consistent with our previous observations. Moreover, (D1) also shows significance with the inspected data scaled up. The results demonstrate that the validated data have a higher quality than those without a formal validation process. Therefore, our proposed MUSTARD framework is beneficial for providing such higher-quality data and being helpful for LLM mathematical reasoning.

Table 3: Inspection dimensions and requirements in human evaluation. IS: Informal Statement. IP: Informal Proof. FS: Formal Statement. FP: Formal Proof. RT: Reasoning Type. Significant $p<0.005$ are marked with bold.