ICLR 2024 Spotlight | 無懼中間步驟，MUSTARD可產生高品質數學推理數據

AIxiv專欄是本站發布學術、技術內容的欄位。過去數年，本站AIxiv專欄接收通報了2,000多篇內容，涵蓋全球各大專院校與企業的頂尖實驗室，有效促進了學術交流與傳播。如果您有優秀的工作想要分享，歡迎投稿或聯絡報道。投稿信箱：liyazhou@jiqizhixin.com；zhaoyunfeng@jiqizhixin.com。

近年來，大型語言模型（LLM）在數學應用題和數學定理證明等任務中取得了長足的進步。數學推理需要嚴格的、形式化的多步驟推理過程，因此是 LLMs 推理能力進步的關鍵里程碑， 但仍面臨著重要的挑戰。

以往的研究工作，如思維鏈（CoT），揭示了中間步驟引導的有效性。然而，人工地去標註這樣的中間步驟需要花費大量人力和時間成本，而自動合成的數據也容易在正確性和人類易讀性上面出現問題。

本文中，來自香港城市大學、中山大學、華為諾亞方舟實驗室等機構的研究人員提出了一個統一的數學推理數據合成框架MUSTARD，能夠生成大量的、正確的且人類可讀可理解的高品質數學推理資料。

• 論文題目：MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
• 論文連結：https://openreview.net/forum?id=8httpslig /github.com/Eleanor-H/MUSTARD
• 資料集連結：https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
  h.github.io/
• 利用形式化證明器的高品質資料合成框架

：首先定義並建立了一個數學概念庫，涵蓋小學、初中、高中和高等教育四個教育階段的概念，每個教育階段有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 條資料；形式化證明器驗證的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。

Dataset download: https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view

Automatic Formalization/Informalization Challenge

Research The team also opened an automatic formalization (autoformalization) and an automatic informalization (auto-informalization) challenge based on the dual data of natural language and Lean formal language in the MUSTARDSAUCE data set. In addition, the research team has simultaneously opened two challenge tracks: automated theorem generation and proving and code-assisted automated optimization problem-solving with code. The competition is from April 3 – May 27, 2024. The winning team will have the opportunity to participate in the ICML 2024 AI for Math workshop on July 26 in Vienna, Austria.

• Track 1-1 (automatic formalization): https://www.codabench.org/competitions/2436/
• Track 1-2 (automatic informalization): https: //www.codabench.org/competitions/2484/
• Track 2 (automatic theorem generation and proof): https://www.codabench.org/competitions/2437/
• Track 3 (code Assisted automatic solution of operations research optimization problems): https://www.codabench.org/competitions/2438/

^References:

^{[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, December 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}

以上是ICLR 2024 Spotlight | 無懼中間步驟，MUSTARD可產生高品質數學推理數據的詳細內容。更多資訊請關注PHP中文網其他相關文章！