大型語言模型（LLMs）是指采用機器學習技術(shù)，利用大量文本數(shù)據(jù)進行訓(xùn)練，以能夠自然地理解和生成自然語言文本的人工智能模型。這些模型可以用于自然語言處理任務(wù)，如文本分類、文本生成、語言翻譯、問題回答和摘要生成等。最近幾年，由于深度學習技術(shù)的進步，大型語言模型已經(jīng)取得了令人矚目的成就，例如 OpenAI 的 GPT 系列模型和 Google 的 BERT 模型等。這些模型似乎具有人類的智力和創(chuàng)造力。他們對書面問題提供詳細而清晰的回答。

幾十年來，數(shù)學家一直試圖將證明轉(zhuǎn)化為計算機代碼，這一過程被稱為形式化。如果你把證明寫成代碼，計算機運行代碼時沒有錯誤，你就知道證明是正確的。但證明一個命題可能需要數(shù)百或數(shù)千個小時。

在過去的五年里，人工智能研究人員已經(jīng)開始教 LLMs 自動將數(shù)學語句形式化。LLMs 已經(jīng)可以將一種自然語言翻譯成另一種自然語言。但從數(shù)學到代碼的轉(zhuǎn)換是一個艱巨的挑戰(zhàn)。

盡管 LLMs 在自然語言處理等領(lǐng)域取得了很大的成功，但是它們也存在一些問題：

數(shù)據(jù)偏差：LLMs 的性能取決于其訓(xùn)練數(shù)據(jù)。如果訓(xùn)練數(shù)據(jù)存在偏差，模型就會學到這些偏差，從而影響其性能。

偏見：LLMs 可能會從其訓(xùn)練數(shù)據(jù)中學習到偏見，并將這些偏見反映在其生成的文本中。這可能導(dǎo)致出現(xiàn)歧視性語言或錯誤的陳述。

知識表示：LLMs 沒有真正的理解語言或世界的知識，它們只是學習出現(xiàn)在數(shù)據(jù)中的模式。這意味著它們可能會在處理新的情況時出現(xiàn)問題。

模型大?。篖LMs 需要大量的計算資源和存儲空間，以及大量的訓(xùn)練數(shù)據(jù)。這使得訓(xùn)練和部署成本非常高。

環(huán)境依賴性：LLMs 的性能取決于輸入的上下文和環(huán)境。如果輸入的數(shù)據(jù)與訓(xùn)練數(shù)據(jù)不同，它們可能會產(chǎn)生錯誤的輸出。

基于上述問題，這些模型有時會做出不合邏輯的陳述，或者自信地把謊言說成事實。谷歌 AI 的吳宇懷表示：“我們不想創(chuàng)建一個像人類一樣說話的語言模型，我們想讓它明白自己在說什么。”

吳是最近兩篇論文的合著者，這兩篇論文提出了一種實現(xiàn)這一目標的方法。它們是關(guān)于一個非常具體的應(yīng)用的：訓(xùn)練人工智能系統(tǒng)做數(shù)學。

第一篇論文描述了如何教 LLM 將普通的數(shù)學語句轉(zhuǎn)換為計算機可以運行和檢查的正式代碼。第二篇訓(xùn)練 LLM 不僅要理解自然語言數(shù)學問題，而且要使用一個名為 Minerva 的系統(tǒng)實際解決這些問題。

Minerva 指的是一個用于解決數(shù)學問題的系統(tǒng)，它是一個組合了自然語言處理和數(shù)學推理的系統(tǒng)。這個系統(tǒng)的作用是幫助計算機理解自然語言中的數(shù)學問題，從而能夠通過推理和計算得出問題的答案。具體來說，這個系統(tǒng)包括多個子系統(tǒng)，包括自然語言處理、問題建模、數(shù)學知識庫和推理引擎等。通過這些子系統(tǒng)的協(xié)作，Minerva 能夠有效地解決自然語言數(shù)學問題。

總之，這些論文提出了未來人工智能設(shè)計的藍圖，LLM 可以通過數(shù)學思維學習推理。

研究人員主要使用名為 Codex 的 LLM（基于 GPT-3）。為了讓 Codex 能夠很好地理解數(shù)學，從而實現(xiàn)自動形式化，他們只提供了兩個自然語言數(shù)學問題示例及其正式代碼翻譯。在簡短的訓(xùn)練之后，Codex 給出了來自高中比賽的近 4000 道數(shù)學題目的自然語言陳述。起初，Codex 準確率略低于 30%。當它失敗時，它創(chuàng)造了一些術(shù)語來填補翻譯詞典的空白。

在此研究之前，Codex 從未嘗試在自然語言和形式數(shù)學代碼之間進行翻譯。但 Codex 通過在 GitHub 上的培訓(xùn)熟悉代碼，也熟悉互聯(lián)網(wǎng)上的自然語言數(shù)學。在此基礎(chǔ)上，研究人員只需向它展示幾個他們想要的例子，Codex 就可以開始連接這些點了。

研究人員不僅試圖教 LLMs 如何翻譯數(shù)學問題，而且還試圖教他們?nèi)绾谓鉀Q問題。

Minerva 數(shù)學

第二篇論文雖然獨立于早期的自動形式化工作，但也有類似的風格。谷歌的研究團隊訓(xùn)練了一種 LLM 來詳細回答高中競賽級別的數(shù)學問題，例如“平行于 y = 4x + 6 的直線經(jīng)過 (5,10)，這條直線與 y 軸交點的 y 坐標是多少?”

作者從一個名為 PaLM 的 LLM 開始，它已經(jīng)接受了一般自然語言內(nèi)容的訓(xùn)練，類似于 GPT-3。他們將這個增強模型命名為 Minerva。

研究人員向 Minerva 展示了他們想要的四個例子。然后他們在一系列定量推理問題上測試了這個模型。Minerva 的表現(xiàn)因科目而異：在某些科目如代數(shù)上，它的正確率略高于一半，而在其他科目如幾何上則略低于一半。

作者們擔心的一個問題是 Minerva 正確回答問題只是因為它已經(jīng)在訓(xùn)練數(shù)據(jù)中看到了這些問題或類似的問題。這個問題被稱為“污染（pollution）”，它使得人們很難知道一個模型是真正在解決問題，還是只是在復(fù)制別人的工作。

為了防止這種可能性，研究人員讓 Minerva 參加了波蘭的 2022 年國家數(shù)學考試，它答對了 65% 的問題。這表明訓(xùn)練有素的模型具有解決數(shù)學問題的能力。

橋

盡管 Minerva 的工作令人印象深刻，但它帶有一個嚴重的問題，作者也指出了這一點：Minerva 沒有辦法自動驗證它是否正確地回答了問題。即使它確實正確地回答了一個問題，它也不能檢查它所采取的步驟是否有效。

換句話說，Minerva 它不能檢查它的工作，這意味著它需要依靠人類的反饋來變得更好。因此，研究人員懷疑這種方法能否擴大到復(fù)雜問題上。

吳指出，一方面，如果你研究自然語言或 Minerva 類型的推理，有很多數(shù)據(jù)可以利用 —— 整個數(shù)學互聯(lián)網(wǎng)，但本質(zhì)上你不能用它進行強化學習。另一方面，像 Isabelle / HOL 這樣的證明助手提供了一個基礎(chǔ)的環(huán)境，但幾乎沒有數(shù)據(jù)可供訓(xùn)練。我們需要某種橋梁把它們連接起來。

自動形式化就是那個橋。自動形式化的改進可以幫助數(shù)學家在編寫證明和驗證工作正確性方面實現(xiàn)自動化。

通過結(jié)合這兩篇論文的進步，像 Minerva 這樣的系統(tǒng)可以首先自動形式化自然語言數(shù)學問題，然后解決它們，并使用證明助手檢查它們的工作。這種即時檢查將為強化學習提供必要的反饋，使這些程序能夠從錯誤中學習。最后，他們會得到一個可證明的正確答案，并附帶一系列邏輯步驟 —— 有效地結(jié)合了 LLM 和強化學習的力量。

人工智能研究人員還有更廣泛的目標。他們認為數(shù)學是開發(fā)人工智能推理技能的完美證明，因為它可以說是所有推理任務(wù)中最難的。按照這種想法，如果一臺機器能夠有效地進行數(shù)學推理，那么它自然應(yīng)該獲得其他技能，比如編寫計算機代碼或提供醫(yī)療診斷的能力。

但是仍然有一些工作是目前的人工智能所無法替代的的，例如：

藝術(shù)創(chuàng)作：創(chuàng)造真正的、有創(chuàng)意的藝術(shù)作品需要人類的創(chuàng)造力和情感體驗的。

心理治療：面對嚴重的心理問題，人類專業(yè)心理醫(yī)生提供的治療和支持無法被取代。

體力勞動：雖然有機器人可以執(zhí)行一些體力勞動工作，但是執(zhí)行某些復(fù)雜的任務(wù)仍然需要人類的技能。

社交關(guān)系：建立和維護人際關(guān)系需要人類的情感和社交技能。

總之，在許多領(lǐng)域中，人類的情感、判斷和創(chuàng)造力是無法被替代的。

更多信息可以來這里獲取==>>電子技術(shù)應(yīng)用-AET<<