MUSTARD：掌握定理与证明数据的统一合成
人工智能
2024-05-24 v3 计算与语言
形式语言与自动机理论
机器学习
编程语言
摘要
近期，大型语言模型 (LLMs) 在包括数学推理和定理证明在内的各种任务中取得了显著进展。由于这两项任务需要严格且形式化的多步推理，它们是探索 LLMs 推理能力的理想领域，但仍面临重要挑战。先前的研究，如思维链 (CoT)，揭示了中间步骤引导的有效性。然而，这种逐步标注需要大量人力，导致当前基准测试的训练步骤不足。为填补这一空白，本工作引入了 MUSTARD，一个掌握高质量、多样性定理与证明数据统一合成的数据生成框架。MUSTARD 分三个阶段合成数据：(1) 它采样少量数学概念种子作为问题类别。(2) 然后，它提示一个生成式语言模型，利用采样的概念来获取问题及其逐步形式化解法。(3) 最后，该框架利用证明助手（例如 Lean Prover）来筛选有效的证明。通过提出的 MUSTARD，我们呈现了一个包含 5,866 个有效数据点的定理与证明基准 MUSTARDSAUCE。每个数据点包含一个非形式化陈述、一个非形式化证明以及一个通过证明器验证的转换后的形式化证明。我们进行了广泛的分析，并证明 MUSTARD 生成了经过验证的高质量逐步数据。我们进一步应用 MUSTARDSAUCE 来微调较小的语言模型。微调后的 Llama 2-7B 在自动定理证明中实现了 15.41% 的平均相对性能增益，在数学应用题中实现了 8.18% 的增益。代码和数据可在 https://github.com/Eleanor-H/MUSTARD 获取。
引用
@article{arxiv.2402.08957,
title = {MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data},
author = {Yinya Huang and Xiaohan Lin and Zhengying Liu and Qingxing Cao and Huajian Xin and Haiming Wang and Zhenguo Li and Linqi Song and Xiaodan Liang},
journal= {arXiv preprint arXiv:2402.08957},
year = {2024}
}