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

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

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

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

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

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

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

->輔導(dǎo)界的小米帶你沖刺ACL2024

數(shù)據(jù)集

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

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

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

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

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

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

模型訓(xùn)練

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

訓(xùn)練量：

LLEMMA 7B：2000億令牌的訓(xùn)練。

LLEMMA 34B：500億令牌的訓(xùn)練。

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

訓(xùn)練細(xì)節(jié)：

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

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

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

實驗設(shè)置與評估結(jié)果

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

評估范圍：

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

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

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

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

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

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

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

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

MMLU-STEM：MMLU基準(zhǔn)中的18個子集，涵蓋57個主題。

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

作者與以下模型進(jìn)行了比較：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

結(jié)語

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

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

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