近年來(lái)，大型語(yǔ)言模型（LLM）在數(shù)學(xué)應(yīng)用題和數(shù)學(xué)定理證明等任務(wù)中取得了長(zhǎng)足的進(jìn)步。數(shù)學(xué)推理需要嚴(yán)格的、形式化的多步推理過程，因此是 LLMs 推理能力進(jìn)步的關(guān)鍵里程碑， 但仍然面臨著重要的挑戰(zhàn)。

以往的研究工作，如思維鏈（CoT），揭示了中間步驟引導(dǎo)的有效性。然而，人工地去標(biāo)注這樣的中間步驟需要花費(fèi)大量人力和時(shí)間成本，而自動(dòng)合成的數(shù)據(jù)也容易在正確性和人類易讀性上面出現(xiàn)問題。

本文中，來(lái)自香港城市大學(xué)、中山大學(xué)、華為諾亞方舟實(shí)驗(yàn)室等機(jī)構(gòu)的研究人員提出了一個(gè)統(tǒng)一的數(shù)學(xué)推理數(shù)據(jù)合成框架 MUSTARD，能夠生成大量的、正確的且人類可讀可理解的高質(zhì)量數(shù)學(xué)推理數(shù)據(jù)。

• 論文題目：MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
• 論文鏈接：https://openreview.net/forum?id=8xliOUg9EW
• 代碼鏈接：https://github.com/Eleanor-H/MUSTARD
• 數(shù)據(jù)集鏈接：https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
• 作者主頁(yè)：https://eleanor-h.github.io/

利用形式化證明器的高質(zhì)量數(shù)據(jù)合成框架

MUSTARD 框架由三階段組成：

第一階段，概念采集：首先定義并建立了一個(gè)數(shù)學(xué)概念庫(kù)，涵蓋小學(xué)、初中、高中和高等教育四個(gè)教育階段的概念，每個(gè)教育階段有 5 至 9 個(gè)數(shù)學(xué)領(lǐng)域，涵蓋代數(shù)和幾何等不同類型的數(shù)學(xué)問題。每個(gè)領(lǐng)域都包含細(xì)分的數(shù)學(xué)概念，如多項(xiàng)式運(yùn)算或因式分解。隨后從數(shù)學(xué)概念庫(kù)當(dāng)中抽取一個(gè)或多個(gè)數(shù)學(xué)概念作為種子，規(guī)定所生成的問題類別。

第二階段，數(shù)據(jù)生成：根據(jù)數(shù)學(xué)概念提示大型語(yǔ)言模型生成數(shù)學(xué)問題和多步的求解過程。具體來(lái)說(shuō)，MUSTARD 利用大型語(yǔ)言模型生成自然語(yǔ)言和代碼的能力，提示大型語(yǔ)言模型完成三項(xiàng)任務(wù)：（T1）生成與給定概念相關(guān)的數(shù)學(xué)問題；（T2）用自然語(yǔ)言給出問題的求解；（T3）自動(dòng)形式化，將自然語(yǔ)言求解轉(zhuǎn)化為 Lean 3 的形式化求解。

第三階段，形式化驗(yàn)證：使用交互式的形式化定理證明器的驗(yàn)證篩選出準(zhǔn)確的求解過程。MUSTARD 將 Lean 3 的形式化求解輸送給 Lean 形式化驗(yàn)證器后，如果定理證明器沒有返回錯(cuò)誤信息，則相應(yīng)的數(shù)據(jù)會(huì)被收集到有效集合中。否則，MUSTARD 會(huì)從定理證明器那里收集錯(cuò)誤信息，并提示語(yǔ)言模型修改形式化求解。MUSTARD 會(huì)進(jìn)行多輪驗(yàn)證和自我糾正，直到獲得有效的形式化求解。

MUSTARD 框架由概念采集、數(shù)據(jù)生成、形式化驗(yàn)證三階段組成。

數(shù)據(jù)質(zhì)量的人工評(píng)價(jià)

為了探究 MUSTARD 生成數(shù)據(jù)的質(zhì)量，研究團(tuán)隊(duì)請(qǐng)掌握數(shù)學(xué)和 Lean 3 語(yǔ)言專業(yè)人士對(duì)數(shù)據(jù)進(jìn)行了質(zhì)量檢查。他們從生成的數(shù)據(jù)中隨機(jī)抽取 200 條，其中 100 條通過 Lean 定理證明器的驗(yàn)證（有效組），100 條沒有通過驗(yàn)證（無(wú)效組）。質(zhì)量檢查涵蓋每條數(shù)據(jù)的四個(gè)部分（即自然語(yǔ)言問題描述、自然語(yǔ)言求解、形式化問題描述和形式化求解），包括了正確性和一致性的檢查。具體來(lái)說(shuō)，高質(zhì)量的數(shù)據(jù)應(yīng)該有正確的自然語(yǔ)言問題描述 (D1) 和正確的問題求解 (D4)。形式化問題描述和求解應(yīng)該與自然語(yǔ)言的問題描述和求解保持一致（D5、D6）。此外，數(shù)據(jù)應(yīng)該符合指定的數(shù)學(xué)概念 (D2) 和問題類型 (D3)。表 3 展示了這六個(gè)檢查維度及要求。如果數(shù)據(jù)符合要求，則在維度中得 1 分，否則得 0 分。

表 3 顯示了有效組和無(wú)效組在每個(gè)維度上的準(zhǔn)確率和相應(yīng)的 p 值。(D1）和（D4）的顯著差異性說(shuō)明了 MUSTARD 生成的問題和答案的正確性。（D6）的顯著差異性表明了所生成的數(shù)據(jù)的自然語(yǔ)言描述和形式化描述的高度一致性。

數(shù)據(jù)對(duì)模型數(shù)學(xué)推理能力的有效性

為了評(píng)估 MUSTARDSAUCE 對(duì)提高數(shù)學(xué)推理能力的影響，研究團(tuán)隊(duì)利用這些數(shù)據(jù)對(duì)較小規(guī)模的語(yǔ)言模型進(jìn)行了微調(diào)，并在數(shù)學(xué)應(yīng)用題（MWP）和自動(dòng)定理證明（ATP）上對(duì)其進(jìn)行了評(píng)估。本文對(duì)比了 MUSTARDSAUCE 數(shù)據(jù)集的以下組合數(shù)據(jù)的有效性：

• MUSTARDSAUCE-valid：經(jīng)過了 Lean 形式化證明器驗(yàn)證的 5866 條數(shù)據(jù)；
• MUSTARDSAUCE-invalid：未能通過 Lean 形式化證明器驗(yàn)證的 5866 條數(shù)據(jù)；
• MUSTARDSAUCE-random：隨機(jī)的 5866 條數(shù)據(jù)；
• MUSTARDSAUCE-tt：MUSTARD 生成的所有 28316 條數(shù)據(jù)。

研究團(tuán)隊(duì)采用 LoRA [1] 在每個(gè)組合數(shù)據(jù)上微調(diào)開源 GPT2-large [2]、Llama 2-7B 和 Llama 2-70B [3]。對(duì)于數(shù)學(xué)應(yīng)用題任務(wù)，他們使用 GSM8K [4] 和 MATH [5][6] 數(shù)據(jù)集進(jìn)行評(píng)估。在評(píng)估自動(dòng)定理證明時(shí)，研究團(tuán)隊(duì)使用了 Mathlib [8]和 miniF2F [7] 基準(zhǔn)。此外，他們也在 MUSTARDSAUCE-test 上進(jìn)行了評(píng)估。

總的來(lái)說(shuō)，在 MUSTARDSAUCE 上對(duì)模型進(jìn)行微調(diào)提高了模型的數(shù)學(xué)推理能力。在自動(dòng)定理證明（下表 5）和數(shù)學(xué)應(yīng)用題求解（下表 4），使用 MUSTARDSAUCE-valid 進(jìn)行微調(diào)與使用 MUSTARDSAUCE-random 進(jìn)行微調(diào)相比，平均相對(duì)性能提高了 18.15%（下表 5）和 11.01%（下表 4）。

對(duì)于自動(dòng)定理證明，經(jīng)過微調(diào)的 Llama 2-7B 平均性能提升 15.41%，經(jīng)過微調(diào)的 GPT 2-large 平均性能提升 20.89%。

對(duì)于數(shù)學(xué)應(yīng)用題求解，經(jīng)過微調(diào)的 Llama 2-7B 平均性能提升 8.18%，經(jīng)過微調(diào)的 GPT 2-large 平均性能提升 15.41%。此外，經(jīng)過 MUSTARDSAUCE-tt 微調(diào)的模型雖在微調(diào)數(shù)據(jù)量上有絕對(duì)優(yōu)勢(shì)，但其性能不及經(jīng)過 MUSTARDSAUCE-valid 微調(diào)的模型性能。

Llama 2-70B 的更多結(jié)果。在微調(diào)更大的語(yǔ)言模型時(shí)，MUSTARDSAUCE 數(shù)據(jù)仍然有效。

MUSTARDSAUCE 數(shù)據(jù)集

本文開源了 MUSTARDSAUCE 數(shù)據(jù)集。其中每一個(gè)數(shù)據(jù)都包含了自然語(yǔ)言的問題描述和多步求解，以及對(duì)偶的形式化語(yǔ)言 Lean 3 的問題描述和多步求解。MUSTARDSAUCE 的數(shù)據(jù)包括了數(shù)學(xué)應(yīng)用題和定理證明題，涵蓋了從小學(xué)到高等教育階段的難度分級(jí)。題目的推理步數(shù)隨著題目難度的增長(zhǎng)而增長(zhǎng)。最難的題目需要 30 步左右的求解步驟，約 20 個(gè) Lean 3 tactics。

數(shù)據(jù)集下載：https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view

自動(dòng)形式化 / 非形式化挑戰(zhàn)賽

研究團(tuán)隊(duì)還基于 MUSTARDSAUCE 數(shù)據(jù)集的自然語(yǔ)言和 Lean 形式語(yǔ)言的對(duì)偶數(shù)據(jù)，開放了一個(gè)自動(dòng)形式化（autoformalization）和一個(gè)自動(dòng)非形式化（auto-informalization）的挑戰(zhàn)賽。此外，研究團(tuán)隊(duì)還同步開放了自動(dòng)定理生成和證明（automated theorem generation and proving）和代碼輔助的運(yùn)籌優(yōu)化問題自動(dòng)求解（automated optimization problem-solving with code）等兩個(gè)挑戰(zhàn)賽賽道。比賽時(shí)間為 2024 年 4 月 3 日 – 5 月 27 日。優(yōu)勝隊(duì)伍將有機(jī)會(huì)參加 7 月 26 日于奧地利維也納舉辦的 ICML 2024 AI for Math 研討會(huì)。

• 賽道 1-1 （自動(dòng)形式化）：https://www.codabench.org/competitions/2436/
• 賽道 1-2 （自動(dòng)非形式化）：https://www.codabench.org/competitions/2484/
• 賽道 2 （自動(dòng)定理生成和證明）：https://www.codabench.org/competitions/2437/
• 賽道 3 （代碼輔助的運(yùn)籌優(yōu)化問題自動(dòng)求解）：https://www.codabench.org/competitions/2438/

本文轉(zhuǎn)自 機(jī)器之心 ，作者：機(jī)器之心

原文鏈接:??https://mp.weixin.qq.com/s/-mVe7ztpAmT71Gf8iDAYhA??