MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

📄 arXiv: 2402.08957v3 📥 PDF

作者: Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, Xiaodan Liang

分类: cs.AI, cs.CL, cs.FL, cs.LG, cs.PL

发布日期: 2024-02-14 (更新: 2024-05-23)

期刊: ICLR 2024 spotlight

🔗 代码/项目: GITHUB

💡 一句话要点

提出MUSTARD框架以高效生成定理与证明数据

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 数据生成 大型语言模型 数学推理 自动化推理 机器学习 教育技术

📋 核心要点

  1. 现有方法在数学推理和定理证明任务中面临步骤标注劳动强度大、训练数据不足的问题。
  2. MUSTARD框架通过采样数学概念、生成问题及其解决方案，并利用证明助手过滤有效证明，解决了数据生成的效率和质量问题。
  3. 经过实验，微调后的Llama 2-7B模型在自动定理证明中实现了15.41%的相对性能提升，在数学应用题中提升了8.18%。

📝 摘要（中文）

近年来，大型语言模型在数学推理和定理证明等任务上取得了显著进展。这些任务需要严格的多步骤推理，然而现有方法如链式思维（CoT）在步骤标注上存在劳动强度大的问题，导致训练步骤不足。为了解决这一问题，本文提出了MUSTARD，一个高质量和多样性的定理与证明数据生成框架。MUSTARD通过三个阶段合成数据：首先，采样数学概念种子作为问题类别；其次，利用生成语言模型生成问题及其逐步的正式解决方案；最后，使用证明助手（如Lean Prover）过滤有效证明。通过MUSTARD，我们构建了包含5866个有效数据点的基准MUSTARDSAUCE，并展示了生成的高质量逐步数据的有效性。

🔬 方法详解

问题定义：本文旨在解决现有定理与证明数据生成方法在步骤标注上的劳动强度大和训练数据不足的问题。

核心思路：MUSTARD框架通过自动化的方式生成高质量的定理和证明数据，减少人工干预，提高数据生成的效率和多样性。

技术框架：MUSTARD的整体架构分为三个主要阶段：首先，采样数学概念种子；其次，利用生成语言模型生成问题及其逐步解决方案；最后，使用证明助手过滤有效证明。

关键创新：MUSTARD的创新在于其统一的合成方法，能够高效生成多样化的定理与证明数据，克服了传统方法的局限性。

关键设计：在数据生成过程中，选择合适的数学概念种子和生成模型的提示设计是关键，确保生成的数据既符合逻辑又具备多样性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，微调后的Llama 2-7B模型在自动定理证明任务中实现了15.41%的相对性能提升，而在数学应用题中提升了8.18%。这些结果表明MUSTARD框架在生成高质量数据方面的有效性和实用性。

🎯 应用场景

MUSTARD框架的潜在应用领域包括教育、自动化定理证明、数学问题求解等。通过生成高质量的定理与证明数据，可以为机器学习模型的训练提供丰富的资源，推动智能教育和自动化推理系统的发展。

📄 摘要（原文）

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.