數(shù)學(xué)，作為科學(xué)的基石，一直以來都是研究和創(chuàng)新的關(guān)鍵領(lǐng)域。

最近，普林斯頓大學(xué)等七家機(jī)構(gòu)聯(lián)合發(fā)布了一個專門用于數(shù)學(xué)的大語言模型LLEMMA，性能媲美谷歌Minerva 62B，并公開了其模型、數(shù)據(jù)集和代碼，為數(shù)學(xué)研究帶來了前所未有的機(jī)會和資源。

論文地址：https://arxiv.org/abs/2310.10631

數(shù)據(jù)集地址：https://huggingface.co/datasets/EleutherAI/proof-pile-2

項目地址：https://github.com/EleutherAI/math-lm

LLEMMA承襲了Code Llama的基礎(chǔ)，在Proof-Pile-2上進(jìn)行了預(yù)訓(xùn)練。

Proof-Pile-2，一個龐大的混合數(shù)據(jù)集，包含著550億token的信息，其中包括科學(xué)論文、富含數(shù)學(xué)內(nèi)容的網(wǎng)頁數(shù)據(jù)以及數(shù)學(xué)代碼。

這個數(shù)據(jù)集的一部分，Algebraic Stack，更是匯集了來自17種語言的11B數(shù)據(jù)集，覆蓋了數(shù)值、符號和數(shù)學(xué)證明。

擁有7億和34億個參數(shù)，在MATH基準(zhǔn)測試中表現(xiàn)卓越，超越了所有已知的開源基礎(chǔ)模型。

在與Google Research開發(fā)的專門用于數(shù)學(xué)的封閉模型相比，參數(shù)量只有Minerva 62B一半的條件下，Llemma 34B獲得了幾乎相同的性能。

Llemma在等參數(shù)基礎(chǔ)上超越了Minerva的問題解決性能，通過應(yīng)用計算工具和進(jìn)行形式定理證明，為數(shù)學(xué)問題的解決提供了無限可能。

它能輕松使用Python解釋器和形式定理證明器，進(jìn)一步展示了其解決數(shù)學(xué)問題的能力。

由于Algebraic Stack中對形式證明數(shù)據(jù)的特別重視，Llemma是第一個展示出少樣本定理證明能力的開放基礎(chǔ)模型。

圖

研究人員還開放共享了LLEMMA的所有訓(xùn)練數(shù)據(jù)和代碼。與以往的數(shù)學(xué)模型不同，LLEMMA是一個開源的、開放共享的模型，為整個科研社區(qū)敞開大門。

研究人員試圖量化模型記憶的效果。令人驚訝的是，他們發(fā)現(xiàn)Llemma對于訓(xùn)練集中出現(xiàn)的問題并沒有變得更加準(zhǔn)確。由于代碼和數(shù)據(jù)是開源的，研究人員鼓勵其他人復(fù)制和擴(kuò)展他們的分析。

訓(xùn)練數(shù)據(jù)和實驗配置

LLEMMA是一個專門用于數(shù)學(xué)的大型語言模型，它在Code Llama的基礎(chǔ)上繼續(xù)在Proof-Pile-2上進(jìn)行預(yù)訓(xùn)練，Proof-Pile-2是一個包含科學(xué)論文、含有數(shù)學(xué)內(nèi)容的網(wǎng)頁數(shù)據(jù)和數(shù)學(xué)代碼的包含了550億token的混合數(shù)據(jù)集。

其中的代碼部分AlgebraicStack包含了17種語言源代碼的11B數(shù)據(jù)集，涵蓋數(shù)值、符號和形式數(shù)學(xué)，并已開源。

LLEMMA的每個模型均從Code Llama初始化。Code Llama模型是從Llama 2初始化的decoder-only的語言模型。

作者使用標(biāo)準(zhǔn)的自回歸語言建模目標(biāo)在Proof-Pile-2上繼續(xù)訓(xùn)練Code Llama模型，對7B模型進(jìn)行了200B token的訓(xùn)練，對34B模型進(jìn)行了50B token的訓(xùn)練。

評估方法和實驗結(jié)果

作者使用Proof-Pile-2對Code Llama進(jìn)行繼續(xù)預(yù)訓(xùn)練，并且在MATH和GSM8k等多個數(shù)學(xué)問題解決任務(wù)上對LLEMMA進(jìn)行few-shot評估。

研究人員發(fā)現(xiàn)LLEMMA在這些任務(wù)上都有顯著的提升，并且能夠適應(yīng)不同的問題類型和難度。

即便是在極高難度的數(shù)學(xué)題中，LLEMMA 34B也能夠展示出與其他開放式基礎(chǔ)模型相比更強(qiáng)大的數(shù)學(xué)能力。

在數(shù)學(xué)基準(zhǔn)測試上，LLEMMA在Proof-Pile-2上的持續(xù)預(yù)訓(xùn)練改善了五個數(shù)學(xué)基準(zhǔn)測試的few-shot性能。

LLEMMA 34B在GSM8k上的改進(jìn)比Code Llama高出20個百分點，在MATH上高出13個百分點。LLEMMA 7B也優(yōu)于相似大小的專有的Minerva模型，這證明了在Proof-Pile-2上進(jìn)行預(yù)訓(xùn)練能有效提高大模型的數(shù)學(xué)解題能力。

在利用計算工具，如Python等解決數(shù)學(xué)問題方面，在MATH+Python和GSM8k+Python任務(wù)上，LLEMMA都比Code Llama更勝一籌。

在使用工具的 MATH 和 GSM8k 數(shù)據(jù)集上，LLEMMA 的性能也高于不使用工具時的性能。

在數(shù)學(xué)證明任務(wù)上，LLEMMA也表現(xiàn)優(yōu)異。

非正式到正式證明的任務(wù)目標(biāo)是在給定一個正式陳述、一個非正式的LATEX陳述和一個非正式的LATEX證明的情況下，生成一個正式證明，然后通過證明助手進(jìn)行驗證。

正式到正式證明則是通過生成一系列證明步驟（策略）來證明一個正式陳述。結(jié)果表明，LLEMMA在Proof-Pile-2上的持續(xù)預(yù)訓(xùn)練改善了這兩個正式定理證明任務(wù)的few-shot性能。

LLEMMA不僅擁有令人矚目的性能、還開放了革命性的數(shù)據(jù)集、展現(xiàn)了驚人的問題解決能力。

開源共享的精神，標(biāo)志著數(shù)學(xué)界進(jìn)入了一個新的時代。數(shù)學(xué)的未來在這里，而我們每一個數(shù)學(xué)愛好者、研究者和教育者都將從中受益。

LLEMMA的出現(xiàn)為我們提供了前所未有的工具，讓數(shù)學(xué)問題的解決變得更加高效和創(chuàng)新。

此外，開放共享的理念也將促進(jìn)全球科研社區(qū)更加深入的合作，共同推動科學(xué)的進(jìn)步。