計算機被用來驗證數學證明已經有一段時間了，但它們只有在使用專門設計的證明語言準備問題時才能做到這一點，而無法處理數學符號和數學家使用的書面文本的混合體。
如果把用自然語言寫的數學問題轉換為正式程式碼，讓電腦更容易解決它們，或許能夠幫助建構能探索數學新發現的機器。
這個過程被稱為形式化（formalisation），但僅僅一個證明就可能需要數年的工作，因此只有一小部分數學知識被形式化，然後由機器證明。
自動形式化（Autoformalization）指的是自動從自然語言數學翻譯成正式語言的任務。一個成功的自動形式化工具在實踐和哲學上的意義都是巨大的，它可以減少目前過度的形式化成本，並且從長遠來看，它可以連接各種研究領域數學推理的自動化方面。
在最近的一項研究中，Google的 Yuhuai Wu 與其合作者使用 OpenAI Codex 的神經網路進行自動形式化工作。 Codex 已經接受了大量來自網路的文字和程式資料的訓練，程式設計師可以使用它來產生可靠的程式碼。
論文連結：https://arxiv.org/pdf/2205.12615.pdf
大型語言模型的一系列最新進展展示了模型理解形式化語言的潛力。然而，現有的成功僅限於在網路上存在大量語料庫的形式化語言 (例如 Python)。相較之下，形式化的數學資料非常缺乏，最大的形式化數學語言庫之一 Archive of Formal Proofs 只有 180mb 大小，這還不到大語言模型 Codex 訓練資料的 0.18% 。
此外，與通用程式語言的情況不同，自然語言文件字串是廣泛可用的，自然語言和形式化數學語言之間幾乎沒有對齊的資料。因此，大型語言模型的成功是否能直接促進自動形式化的發展，仍是未知的。
鑑於證明語言與程式語言有相似之處，因此團隊決定看看 Codex 是否可以將包含 12500 個中學數學競賽問題的函式庫形式化。它能夠將四分之一的問題轉換為與形式證明求解程序 Isabelle 相容的格式。
Wu 表示，許多不成功的轉換是系統不理解某些數學概念的結果。 「如果你用一個解釋這個概念的例子來展示模型，那麼模型就可以快速掌握它。」
這項工作探討了大語言模型的自動形式化的前景，研究者發現大型語言模型已經在一個互動式定理證明器中具備相當好的形式化自然語言數學的能力。
下圖 1 是一個完美的自動形式化範例。該模型不僅轉換成了語法上正確的 Isabelle 程式碼，而且還能夠掌握自然語言中的重要推理點。
為了測試這種自動形式化程式的效力，團隊隨後將Codex 應用於一組已經有人類形式化版本的問題，Codex 也為這些問題生成了自己的形式化版本。團隊使用了另一個名為 MiniF2F 的 AI 來解決這兩個版本的問題。
自動形式化的問題將 MiniF2F 的成功率從 29% 提高到了 35%，這表明 Codex 在問題形式化方面取得了重要進展。
值得注意的是，許多數學競賽的陳述往往是這樣一種形式：一個人被要求找到某個問題的答案，而不是證明一個給定的命題。然而形式化的數學陳述是以命題的形式，而不是以問題的形式。
為了把一個問題轉換成一個命題，研究者在問題後面附上了「The Final Answer」:
用來進行自動形式化的prompt 格式是：
這是一個有趣的進展，但 Wu 表示團隊的工作只是概念證明。 「如果目標是訓練一台媲美最頂級人類數學家的機器，那麼自動形式化似乎是實現這個目標的關鍵道路。」
劍橋大學團隊成員Albert Jiang 表示，如果進一步提高成功率， AI 將能夠與人類數學家競爭。 「如果我們達到了100% 的水平，我們肯定會創造出贏得國際數學奧林匹克金牌的AI 智能體。」
團隊近期的目標是改進自動形式化模型和自動化證明機器，但研究成果的未來影響將會更深遠。 Wu 表示，這些模型可以揭示人類目前未知的數學領域。
這種機器的推理能力也非常適合更廣泛領域的驗證任務。 「你可以驗證一個軟體是否完全按照你的要求做，或者可以驗證硬體晶片，因此它在金融交易演算法和硬體設計中都會有所應用。」
利用機器探索數學是一個令人興奮的發展，倫敦數學科學研究所的Yang-Hui He 說，但真正的挑戰是在大部分是用LaTex 編寫的數學研究中使用該模型。 「我們只用LaTex 是因為它打字順暢，但它在某種意義上是一種自然語言，也有自己的規則。」
He 說，因為用戶可以在LaTeX 中定義自己的函數和符號，這些函數和符號可能只在一篇數學論文中使用，這對於僅在純文字上訓練過的神經網路來說可能很棘手。
以上是將數學題轉換成程式碼，Google這項研究讓機器證明的正確率大幅提高的詳細內容。更多資訊請關注PHP中文網其他相關文章！
