  Recent large language models (LLMs) have witnessed significant advancement in
various tasks, including mathematical reasoning and theorem proving. As these
two tasks require strict and formal multi-step inference, they are appealing
domains for exploring the reasoning ability of LLMs but still face important
challenges. Previous studies such as Chain-of-Thought (CoT) have revealed the
effectiveness of intermediate steps guidance. However, such step-wise
annotation requires heavy labor, leading to insufficient training steps for
current benchmarks. To fill this gap, this work introduces MUSTARD, a data
generation framework that masters uniform synthesis of theorem and proof data
of high quality and diversity. MUSTARD synthesizes data in three stages: (1) It
samples a few mathematical concept seeds as the problem category. (2) Then, it
prompts a generative language model with the sampled concepts to obtain both
the problems and their step-wise formal solutions. (3) Lastly, the framework
utilizes a proof assistant (e.g., Lean Prover) to filter the valid proofs. With
the proposed MUSTARD, we present a theorem-and-proof benchmark MUSTARDSAUCE
with 5,866 valid data points. Each data point contains an informal statement,
an informal proof, and a translated formal proof that passes the prover
validation. We perform extensive analysis and demonstrate that MUSTARD
generates validated high-quality step-by-step data. We further apply the
MUSTARDSAUCE for fine-tuning smaller language models. The fine-tuned Llama 2-7B
achieves a 15.41% average relative performance gain in automated theorem
proving, and 8.18% in math word problems. Codes and data are available at
https://github.com/Eleanor-H/MUSTARD.
