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

LLEMMA解數(shù)學題的一個示例

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

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

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

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

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

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

數(shù)據(jù)集

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

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

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

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

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

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

模型訓練

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

訓練量：

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

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

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

訓練細節(jié)：

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

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

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

實驗設置與評估結果

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

評估范圍：

數(shù)學問題求解：測試模型在思維鏈推理和多數(shù)投票的數(shù)學問題上的表現(xiàn)。

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

記憶和數(shù)據(jù)混合的影響：分析這些因素如何影響模型的表現(xiàn)。

使用CoT解決數(shù)學任務

評估數(shù)據(jù)集和任務：

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

GSM8k：包含中學數(shù)學問題的數(shù)據(jù)集。

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

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

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

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

Minerva：這個模型在技術內(nèi)容的數(shù)據(jù)集上繼續(xù)預訓練了PaLM語言模型。

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

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

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

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

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

調(diào)用計算工具解決數(shù)學任務

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

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

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

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

形式化數(shù)學（數(shù)學證明）

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

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

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

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

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

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

數(shù)據(jù)混合

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

數(shù)據(jù)重疊和記憶

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

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

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

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

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

結語

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

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

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