AIxiv专栏是机器之心发布学术、技术内容的栏目。过去数年，机器之心AIxiv专栏接收报道了2000多篇内容，覆盖全球各大高校与企业的顶级实验室，有效促进了学术交流与传播。如果您有优秀的工作想要分享，欢迎投稿或者联系报道。投稿邮箱：[email protected]；[email protected]。
近年来，大型谈话模型（LLM）在数学应用题和数学定理证实等任务中取得了长足的进步。数学推理需要严格的、形式化的多步推理过程，因此是 LLMs 推理能力进步的关键里程碑， 但仍然面临着重要的挑战。
以往的研究工作，如思维链（CoT），揭示了中间步骤引导的有效性。然而，人工地去标注这样的中间步骤需要花费大量人力和时间成本，而主动合成的数据也容易在正确性和人类易读性上面出现题目。
本文中，来自香港城市大学、中山大学、华为诺亚方舟实验室等机构的研究人员提出了一个统一的数学推理数据合成框架 MUSTARD，能够生成大量的、正确的且人类可读可理解的高质量数学推理数据。
论文题目：MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
论文链接：https://openreview.net/forum?id=8xliOUg9EW
代码链接：https://github.com/Eleanor-H/MUSTARD
数据集链接：https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
作者主页：https://eleanor-h.github.io/
利用形式化证实器的高质量数据合成框架
MUSTARD 框架由三阶段组成：
第一阶段，观点采集：首先定义并建立了一个数学观点库，涵盖小学、初中、高中和高等教育四个教育阶段的观点，每个教育阶段有 5 至 9 个数学领域，涵盖代数和几何等不同类型的数学题目。每个领域都包含细分的数学观点，如多项式运算或因式分解。随后从数学观点库当中抽取一个或多个数学观点作为种子，规定所生成的题目类别。
第二阶段，数据生成：根据数学观点提示大型谈话模型生成数学题目和多步的求解过程。具体来说，MUSTARD 利用大型谈话模型生成自然谈话和代码的能力，提示大型谈话模型完成三项任务：（T1）生成与给定观点相关的数学题目；（T2）用自然谈话给出题目的求解；（T3）主动形式化，将自然谈话求解转化为 Lean 3 的形式化求解。
第三阶段，形式化考证：使用交互式的形式化定理证实器的考证筛选出准确的求解过程。MUSTARD 将 Lean 3 的形式化求解输送给 Lean 形式化考证器后，如果定理证实器没有返回错误信息，则相应的数据会被收集到有效集合中。否则，MUSTARD 会从定理证实器那里收集错误信息，并提示谈话模型修改形式化求解。MUSTARD 会进行多轮考证和自我纠正，直到获得有效的形式化求解。
MUSTARD 框架由观点采集、数据生成、形式化考证三阶段组成。
数据质量的人工评价
为了探究 MUSTARD 生成数据的质量，研究团队请掌握数学和 Lean 3 谈话专业人士对数据进行了质量检查。他们从生成的数据中随机抽取 200 条，其中 100 条通过 Lean 定理证实器的考证（有效组），100 条没有通过考证（无效组）。质量检查涵盖每条数据的四个部分（即自然谈话题目形容、自然谈话求解、形式化题目形容和形式化求解），包括了正确性和一致性的检查。具体来说，高质量的数据应该有正确的自然谈话题目形容 (D1) 和正确的题目求解 (D4)。形式化题目形容和求解应该与自然谈话的题目形容和求解保持一致（D5、D6）。此外，数据应该符合指定的数学观点 (D2) 和题目类型 (D3)。表 3 展示了这六个检查维度及要求。如果数据符合要求，则在维度中得 1 分，否则得 0 分。
表 3 显示了有效组和无效组在每个维度上的准确率和相应的 p 值。(D1）和（D4）的显著差异性说明了 MUSTARD 生成的题目和答案的正确性。（D6）的显著差异性表明了所生成的数据的自然谈话形容和形式化形容的高度一致性。
数据对模型数学推理能力的有效性
为了评估 MUSTARDSAUCE 对提高数学推理能力的影响，研究团队利用这些数据对较小规模的谈话模型进行了微调，并在数学应用题（MWP）和主动定理证实（ATP）上对其进行了评估。本文对比了 MUSTARDSAUCE 数据集的以下组合数据的有效性：
MUSTARDSAUCE-valid：经过了 Lean 形式化证实器考证的 5866 条数据；
MUSTARDSAUCE-invalid：未能通过 Lean 形式化证实器考证的 5866 条数据；
MUSTARDSAUCE-random：随机的 5866 条数据；
MUSTARDSAUCE-tt：MUSTARD 生成的所有 28316 条数据。
研究团队采用 LoRA [1] 在每个组合数据上微调开源 GPT2-large [2]、Llama 2-7B 和 Llama 2-70B [3]。对于数学应用题任务，他们使用 GSM8K [4] 和 MATH [5][6] 数据集进行评估。在评估主动定理证实时，研究团队使用了 Mathlib [8]和 miniF2F [7] 基准。此外，他们也在 MUSTARDSAUCE-test 上进行了评估。
总的来说，在 MUSTARDSAUCE 上对模型进行微调提高了模型的数学推理能力。在主动定理证实（下表 5）和数学应用题求解（下表 4），使用 MUSTARDSAUCE-valid 进行微调与使用 MUSTARDSAUCE-random 进行微调相比，平均相对功能提高了 18.15%（下表 5）和 11.01%（下表 4）。
对于主动定理证实，经过微调的 Llama 2-7B 平均功能提升 15.41%，经过微调的 GPT 2-large 平均功能提升 20.89%。
对于数学应用题求解，经过微调的 Llama 2-7B 平均功能提升 8.18%，经过微调的 GPT 2-large 平均功能提升 15.41%。此外，经过 MUSTARDSAUCE-tt 微调的模型虽在微调数据量上有绝对优势，但其功能不及经过 MUSTARDSAUCE-valid 微调的模型功能。
Llama 2-70B 的更多结果。在微调更大的谈话模型时，MUSTARDSAUCE 数据仍然有效。
MUSTARDSAUCE 数据集
本文开源了 MUSTARDSAUCE 数据集。其中每一个数据都包含了自然谈话的题目形容和多步求解，以及对偶的形式化谈话 Lean 3 的题目形容和多步求解。MUSTARDSAUCE 的数据包括了数学应用题和定理证实题，涵盖了从小学到高等教育阶段的难度分级。题目的推理步数随着题目难度的增长而增长。最难的题目需要 30 步左右的求解步骤，约 20 个 Lean 3 tactics。
数据集下载：https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
主动形式化 / 非形式化挑战赛
研究团队还基于 MUSTARDSAUCE 数据集的自然谈话和 Lean 形式谈话的对偶数据，开放了一个主动形式化（autoformalization）和一个主动非形式化（auto-informalization）的挑战赛。此外，研究团队还同步开放了主动定理生成和证实（automated theorem generation and proving）和代码辅助的运筹优化题目主动求解（automated optimization problem-solving with code）等两个挑战赛赛道。比赛时间为 2024 年 4 月 3 日 – 5 月 27 日。优胜队伍将有机会参加 7 月 26 日于奥地利维也纳举办的 ICML 2024 AI for Math 研讨会。
赛道 1-1 （主动形式化）：https://www.codabench.org/competitions/2436/
赛道 1-2 （主动非形式化）：https://www.codabench.org/competitions/2484/
赛道 2 （主动定理生成和证实）：https://www.codabench.org/competitions/2437/
赛道 3 （代码辅助的运筹优化题目主动求解）：https://www.codabench.org/competitions/2438/
参考文献：
[1] Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. arXiv preprint arXiv:2106.09685, 2021.
[2] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1 (8):9, 2019.
[3] Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Niko- lay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami, Naman Goyal, Anthony Hartshorn, Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Marie-Anne Lachaux, Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog, Yixin Nie, Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiaoqing Ellen Tan, Binh Tang, Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, Iliyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aure ́lien Rodriguez, Robert Stojnic, Sergey Edunov, and Thomas Scialom. Llama 2: Open foundation and fine- tuned chat models. CoRR, abs/2307.09288, 2023. doi: 10.48550/arXiv.2307.09288. URL https://doi.org/10.48550/arXiv.2307.09288.
[4] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. CoRR, abs/2110.14168, 2021.
[5] 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, Decem- ber 2021, virtual, 2021.
[6] Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. arXiv preprint arXiv:2305.20050, 2023.
[7] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Repre- sentations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
[8] https://github.com/leanprover-community/mathlib