大型語言模型（LLMs）是指采用機器學習技術，利用大量文本數據進行訓練，以能夠自然地理解和生成自然語言文本的人工智能模型。這些模型可以用于自然語言處理任務，如文本分類、文本生成、語言翻譯、問題回答和摘要生成等。最近幾年，由于深度學習技術的進步，大型語言模型已經取得了令人矚目的成就，例如 OpenAI 的 GPT 系列模型和 Google 的 BERT 模型等。這些模型似乎具有人類的智力和創造力。他們對書面問題提供詳細而清晰的回答。
幾十年來，數學家一直試圖將證明轉化為計算機代碼，這一過程被稱為形式化。如果你把證明寫成代碼，計算機運行代碼時沒有錯誤，你就知道證明是正確的。但證明一個命題可能需要數百或數千個小時。
在過去的五年里，人工智能研究人員已經開始教 LLMs 自動將數學語句形式化。LLMs 已經可以將一種自然語言翻譯成另一種自然語言。但從數學到代碼的轉換是一個艱巨的挑戰。
盡管 LLMs 在自然語言處理等領域取得了很大的成功，但是它們也存在一些問題：
數據偏差：LLMs 的性能取決于其訓練數據。如果訓練數據存在偏差，模型就會學到這些偏差，從而影響其性能。
偏見：LLMs 可能會從其訓練數據中學習到偏見，并將這些偏見反映在其生成的文本中。這可能導致出現歧視性語言或錯誤的陳述。
知識表示：LLMs 沒有真正的理解語言或世界的知識，它們只是學習出現在數據中的模式。這意味著它們可能會在處理新的情況時出現問題。
模型大小：LLMs 需要大量的計算資源和存儲空間，以及大量的訓練數據。這使得訓練和部署成本非常高。
環境依賴性：LLMs 的性能取決于輸入的上下文和環境。如果輸入的數據與訓練數據不同，它們可能會產生錯誤的輸出。
基于上述問題，這些模型有時會做出不合邏輯的陳述，或者自信地把謊言說成事實。谷歌 AI 的吳宇懷表示：“我們不想創建一個像人類一樣說話的語言模型，我們想讓它明白自己在說什么。”
吳是最近兩篇論文的合著者，這兩篇論文提出了一種實現這一目標的方法。它們是關于一個非常具體的應用的：訓練人工智能系統做數學。
第一篇論文描述了如何教 LLM 將普通的數學語句轉換為計算機可以運行和檢查的正式代碼。第二篇訓練 LLM 不僅要理解自然語言數學問題，而且要使用一個名為 Minerva 的系統實際解決這些問題。
Minerva 指的是一個用于解決數學問題的系統，它是一個組合了自然語言處理和數學推理的系統。這個系統的作用是幫助計算機理解自然語言中的數學問題，從而能夠通過推理和計算得出問題的答案。具體來說，這個系統包括多個子系統，包括自然語言處理、問題建模、數學知識庫和推理引擎等。通過這些子系統的協作，Minerva 能夠有效地解決自然語言數學問題。
總之，這些論文提出了未來人工智能設計的藍圖，LLM 可以通過數學思維學習推理。
研究人員主要使用名為 Codex 的 LLM（基于 GPT-3）。為了讓 Codex 能夠很好地理解數學，從而實現自動形式化，他們只提供了兩個自然語言數學問題示例及其正式代碼翻譯。在簡短的訓練之后，Codex 給出了來自高中比賽的近 4000 道數學題目的自然語言陳述。起初，Codex 準確率略低于 30%。當它失敗時，它創造了一些術語來填補翻譯詞典的空白。
在此研究之前，Codex 從未嘗試在自然語言和形式數學代碼之間進行翻譯。但 Codex 通過在 GitHub 上的培訓熟悉代碼，也熟悉互聯網上的自然語言數學。在此基礎上，研究人員只需向它展示幾個他們想要的例子，Codex 就可以開始連接這些點了。
研究人員不僅試圖教 LLMs 如何翻譯數學問題，而且還試圖教他們如何解決問題。
Minerva 數學
第二篇論文雖然獨立于早期的自動形式化工作，但也有類似的風格。谷歌的研究團隊訓練了一種 LLM 來詳細回答高中競賽級別的數學問題，例如“平行于 y = 4x + 6 的直線經過 (5,10)，這條直線與 y 軸交點的 y 坐標是多少?”
作者從一個名為 PaLM 的 LLM 開始，它已經接受了一般自然語言內容的訓練，類似于 GPT-3。他們將這個增強模型命名為 Minerva。
研究人員向 Minerva 展示了他們想要的四個例子。然后他們在一系列定量推理問題上測試了這個模型。Minerva 的表現因科目而異：在某些科目如代數上，它的正確率略高于一半，而在其他科目如幾何上則略低于一半。
作者們擔心的一個問題是 Minerva 正確回答問題只是因為它已經在訓練數據中看到了這些問題或類似的問題。這個問題被稱為“污染（pollution）”，它使得人們很難知道一個模型是真正在解決問題，還是只是在復制別人的工作。
為了防止這種可能性，研究人員讓 Minerva 參加了波蘭的 2022 年國家數學考試，它答對了 65% 的問題。這表明訓練有素的模型具有解決數學問題的能力。
橋
盡管 Minerva 的工作令人印象深刻，但它帶有一個嚴重的問題，作者也指出了這一點：Minerva 沒有辦法自動驗證它是否正確地回答了問題。即使它確實正確地回答了一個問題，它也不能檢查它所采取的步驟是否有效。
換句話說，Minerva 它不能檢查它的工作，這意味著它需要依靠人類的反饋來變得更好。因此，研究人員懷疑這種方法能否擴大到復雜問題上。
吳指出，一方面，如果你研究自然語言或 Minerva 類型的推理，有很多數據可以利用 —— 整個數學互聯網，但本質上你不能用它進行強化學習。另一方面，像 Isabelle / HOL 這樣的證明助手提供了一個基礎的環境，但幾乎沒有數據可供訓練。我們需要某種橋梁把它們連接起來。
自動形式化就是那個橋。自動形式化的改進可以幫助數學家在編寫證明和驗證工作正確性方面實現自動化。
通過結合這兩篇論文的進步，像 Minerva 這樣的系統可以首先自動形式化自然語言數學問題，然后解決它們，并使用證明助手檢查它們的工作。這種即時檢查將為強化學習提供必要的反饋，使這些程序能夠從錯誤中學習。最后，他們會得到一個可證明的正確答案，并附帶一系列邏輯步驟 —— 有效地結合了 LLM 和強化學習的力量。
人工智能研究人員還有更廣泛的目標。他們認為數學是開發人工智能推理技能的完美證明，因為它可以說是所有推理任務中最難的。按照這種想法，如果一臺機器能夠有效地進行數學推理，那么它自然應該獲得其他技能，比如編寫計算機代碼或提供醫療診斷的能力。
但是仍然有一些工作是目前的人工智能所無法替代的的，例如：
藝術創作：創造真正的、有創意的藝術作品需要人類的創造力和情感體驗的。
心理治療：面對嚴重的心理問題，人類專業心理醫生提供的治療和支持無法被取代。
體力勞動：雖然有機器人可以執行一些體力勞動工作，但是執行某些復雜的任務仍然需要人類的技能。
社交關系：建立和維護人際關系需要人類的情感和社交技能。
總之，在許多領域中，人類的情感、判斷和創造力是無法被替代的。
更多信息可以來這里獲取==>>電子技術應用-AET<<
