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

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

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

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

項(xiàng)目地址：https://github.com/EleutherAI/math-lm

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

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

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

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

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

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

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

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

圖

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

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

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

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

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

LLEMMA的每個(gè)模型均從Code Llama初始化。Code Llama模型是從Llama 2初始化的decoder-only的語(yǔ)言模型。

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

評(píng)估方法和實(shí)驗(yàn)結(jié)果

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

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

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

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

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

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

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

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

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

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

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

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

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

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