今天向大家介紹一個新的開源大語言模型——LLEMMA，這是一個專為數學研究而設計的前沿語言模型。

LLEMMA解數學題的一個示例

LLEMMA的誕生源于在Proof-Pile-2數據集上對Code Llama模型的深度訓練。這個數據集是一個科學論文、數學相關網頁和數學代碼的綜合體。

過去雖然有數學專用的模型，但許多模型都有各種限制。例如，有的模型是封閉訪問，這使得它們無法為更廣泛的研究所用。有的則技術上稍顯落后。

但LLEMMA的出現改變了這一局面。它不僅在MATH基準測試上創下了新高，甚至超越了某些還未對外公開的頂尖模型，如Minerva。更讓人欣喜的是，LLEMMA無需額外的調整，即可直接應用于工具和定理證明。

讓我們一起了解下這個模型背后的技術吧！

Paper:Llemma: An Open Language Model For Mathematics
Link:https://arxiv.org/pdf/2310.10631.pdf
Code:https://github.com/EleutherAI/math-lm

->輔導界的小米帶你沖刺ACL2024

數據集

LLEMMA是專為數學設計的大型語言模型，具有70億和340億參數。這一模型的訓練方法是在Proof-Pile-2.2.1數據集上繼續對Code Llama模型進行預訓練。以下是關于該數據集的簡要說明：

Proof-Pile-2：這是一個包含550億令牌的綜合數據集，融合了科學論文、數學相關的網絡內容和數學代碼，其知識截止于2023年4月（不包括特定的Lean證明步驟子集）。

代碼：為了適應數學家日益重視的計算工具，如數值模擬和計算代數系統，研究團隊創建了名為AlgebraicStack的源代碼數據集。這個數據集涉及17種編程語言，包括數值、符號和正式的數學內容，共計110億令牌。

網絡數據：研究團隊利用了OpenWebMath數據集，這是一個精選的、與數學相關的高質量網絡頁面集合，總計150億令牌。

科學論文：使用了名為RedPajama的ArXiv子集，其中包含290億令牌。

通用自然語言和代碼數據：作為訓練數據的補充，研究團隊還融合了一些通用領域的數據，并以Proof-Pile-2為主，還融合了Pile數據集和RedPajama的GitHub子集。

模型訓練

模型初始化：所有模型都從Code Llama初始化，隨后在Proof-Pile-2上接受更多的訓練。

訓練量：

LLEMMA 7B：2000億令牌的訓練。

LLEMMA 34B：500億令牌的訓練。

訓練工具和硬件：使用GPT-NeoX庫在256個A100 40GB GPU上進行訓練。使用了各種先進技術如Tensor并行、ZeRO Stage 1分片優化器狀態、Flash Attention 2等以提高效率和減少內存需求。

訓練細節：

LLEMMA 7B：經過42,000步訓練，每個全局批次有400萬令牌，上下文長度為4096令牌，占用A100大約23,000小時。學習率開始從1 × 10^(-4)漸溫，然后逐漸減少。雖然計劃是48,000步訓練，但在42,000步時由于NaN損失中斷了。

LLEMMA 34B：經過12,000步訓練，每個全局批次有400萬令牌，上下文長度為4096令牌，約占用47,000個A100小時。學習率從5 × 10^(-5)開始逐漸增加，然后逐漸減少。

RoPE調整：在訓練LLEMMA 7B前，RoPE的基本周期從θ = 1,000,000減少到θ = 10,000，目的是為了在LLEMMA 7B上進行長上下文微調。而LLEMMA 34B維持了θ = 1,000,000的原始設置。

實驗設置與評估結果

作者通過少樣本評估對LLEMMA模型進行比較，并專注于沒有進行微調的最新模型。具體來說，他們使用了使用思維鏈推理和多數投票，在MATH和GSM8k等基準上進行了評估。

評估范圍：

數學問題求解：測試模型在思維鏈推理和多數投票的數學問題上的表現。

少樣本工具使用和正式定理證明：研究模型在這些方面的表現。

記憶和數據混合的影響：分析這些因素如何影響模型的表現。

使用CoT解決數學任務

評估數據集和任務：

MATH：一個來自高中數學競賽的問題集，模型必須生成一個LATEX的解決方案，且其答案需要與參考答案匹配。

GSM8k：包含中學數學問題的數據集。

OCWCourses：從MIT的開放課程Ware提取的STEM問題。

MMLU-STEM：MMLU基準中的18個子集，涵蓋57個主題。

SAT：包含2023年5月的SAT考試中不包含圖形的數學問題的數據集。

作者與以下模型進行了比較：

Minerva：這個模型在技術內容的數據集上繼續預訓練了PaLM語言模型。

Code Llama：LLEMMA繼續預訓練的初始化模型。

Llama 2：Code Llama在代碼上繼續預訓練的初始化模型。

對于開源的模型，作者使用他們的評估套件來報告分數，該套件是Language Model Evaluation Harness的一個分支。對于Minerva模型，作者報告了Lewkowycz等人在2022年文章中的基準分數。

LLEMMA在Proof-Pile-2上的繼續預訓練提高了五個數學基準測試的少樣本性能。LLEMMA 34B在GSM8k上比Code Llama提高了20個百分點，在MATH上提高了13個百分點；LLEMMA 7B的表現超過了專有的Minerva模型。到目前為止，LLEMMA在所有開放權重語言模型上均表現最佳。因此，可以得出結論，Proof-Pile-2上的繼續預訓練對于提高預訓練模型的數學問題解決能力是有效的。

此外，LLEMMA是在與數學相關的多樣化數據上預訓練的，而不是為特定任務進行調優。因此，預期LLEMMA可以通過任務特定的微調和少樣本提示適應許多其他任務。

調用計算工具解決數學任務

這些任務涉及在有計算工具的情況下解決問題，主要評估了以下內容：

MATH+Python：模型被提示以自然語言交替描述解決方案的步驟，然后使用代碼執行該步驟。最后的答案是一個可以執行為數字類型或SymPy對象的程序。我們的少樣本提示包括使用內置數字操作、math模塊和SymPy的示例。

GSM8k+Python：通過編寫一個執行為整數答案的Python程序來解決GSM8k單詞問題。我們使用了Gao等人（2023）的提示。

如下表所示，LLEMMA在兩個任務上都優于Code Llama。它在MATH和GSM8k上使用工具的性能也高于它在沒有工具的這些數據集上的性能。

形式化數學（數學證明）

交互式證明助手，例如Lean和Isabelle，使用特殊的編程語言來幫助驗證數學證明。但是，與常見的編程語言相比，這些特殊語言的數據非常少。

LLEMMA模型經過進一步的預訓練，以處理與這些證明相關的任務。在給定問題、非正式證明和正式聲明后，LLEMMA可以生成Isabelle代碼的正式證明。此外，模型還可以根據證明助手給出的狀態，生成證明的下一個步驟。

LLEMMA在Proof-Pile-2的預訓練包括從Lean和Isabelle提取的正式數學數據，總計超過15億個標記。作者對LLEMMA在兩個任務上的少樣本性能進行了評估：

非正式到正式的證明：根據非正式的說明，為數學問題生成正式的證明。

正式到正式的證明：在已知的證明步驟中，為下一個步驟生成代碼。

結果顯示，LLEMMA在Proof-Pile-2上的繼續預訓練提高了兩個正式定理證明任務的少樣本性能。

數據混合

在訓練語言模型時，經常會根據混合權重提高訓練數據中高質量子集的樣本頻率。作者通過在多個手動選擇的混合權重上進行短期訓練，然后選擇在高質量保留文本上（使用MATH訓練集）最小化困惑度的權重。通過這種方法，確定了訓練LLEMMA的最佳數據混合比例為21。

數據重疊和記憶

作者檢查了測試問題或解決方案是否出現在語料庫中。通過查找與測試序列中任何30-gram相匹配的文檔確定匹配程度。作者發現大約7%的MATH測試問題陳述和0.6%的解決方案在語料庫中有匹配。

在隨機抽取的100個匹配中，作者詳細檢查了測試問題與OpenWebMath文檔之間的關系。其中，41個案例沒有解決方案，49個提供了與MATH基準解決方案不同但答案相同的解決方案，9個答案錯誤或缺失，而只有1個與基準解決方案相同。

作者進一步探索了語料庫中的問題如何影響模型的性能。當將LLEMMA-34b應用于具有30-gram匹配的測試示例和沒有30-gram匹配的測試示例時，模型在難題上的準確率仍然較低，例如在具有匹配的Level 5問題上的準確率為6.08%，而在沒有匹配的問題上的準確率為6.39%。

作者發現，30-gram匹配與各個難度級別的準確性之間沒有明確的關系。這意味著測試示例和訓練文檔之間的重要匹配，并不意味著模型生成了一個記憶中的正確答案。

此外，作者還檢查了LLEMMA在MATH生成中與OpenWebMath之間的30-gram匹配，發現了13個匹配，這些匹配發生在模型生成了一系列常見的數字序列時，例如斐波那契數列，以及一次多項式因式分解的情況。這些觀察結果值得進一步研究。

結語

在這篇研究中，研究團隊成功地推出了LLEMMA和Proof-Pile-2，這是專為數學語言建模設計的大語言模型和語料庫。他們公開了模型、數據集和相關代碼。

研究揭示，LLEMMA在開放權重模型的數學問題解決標準測試上的表現尤為出眾，它不僅能通過Python代碼嫻熟地調用外部工具，還在定理證明中展示了少樣本策略預測的高效實用性。此外，該團隊深入探討了模型在解決數學問題時的卓越性能。

LLEMMA的出現，為我們展現了數學與人工智能融合的新前景。隨著LLEMMA和Proof-Pile-2的應用，期望在未來更能深化對語言模型的泛化能力、數據集結構的認知，探索將語言模型作為數學助手的可能性，并不斷提升其處理數學問題的能力。