計算機被用來驗證數學證明已經有一段時間了，但它們只有在使用專門設計的證明語言準備問題時才能做到這一點，而無法處理數學符號和數學家使用的書面文本的混合體。

如果把用自然語言編寫的數學問題轉換為正式代碼，讓計算機更容易解決它們，或許能夠幫助構建能探索數學新發現的機器。

這個過程被稱為形式化（formalisation），但僅僅一個證明就可能需要數年的工作，因此只有一小部分數學知識被形式化，然后由機器證明。

自動形式化（Autoformalization）指的是自動從自然語言數學翻譯成正式語言的任務。一個成功的自動形式化工具在實踐和哲學上的意義都是巨大的，它可以減少目前過度的形式化成本，并且從長遠來看，它可以連接各種研究領域數學推理的自動化方面。

在最近的一項研究中，谷歌的 Yuhuai Wu 與其合作者使用 OpenAI Codex 的神經網絡進行自動形式化工作。Codex 已經接受了來自網絡的大量文本和編程數據的訓練，程序員可以使用它來生成可靠的代碼。

論文鏈接：https://arxiv.org/pdf/2205.12615.pdf

將 12500 個中學數學競賽問題形式化

大型語言模型的一系列最新進展展示了模型理解形式化語言的潛力。然而，現有的成功僅限于在網絡上存在大量語料庫的形式化語言 (例如 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 格式是：

AI 將與人類數學家競爭？

這是一項有趣的進展，但 Wu 表示團隊的工作只是一個概念證明。「如果目標是訓練一臺媲美最頂級人類數學家的機器，那么自動形式化似乎是實現這個目標的關鍵道路。」

劍橋大學團隊成員 Albert Jiang 表示，如果進一步提高成功率，AI 將能夠與人類數學家競爭。「如果我們達到了 100% 的水平，我們肯定會創造出贏得國際數學奧林匹克金牌的 AI 智能體。」

團隊近期的目標是改進自動形式化模型和自動化證明機器，但研究成果的未來影響將會更深遠。Wu 表示，這些模型可以揭示人類目前未知的數學領域。

這種機器的推理能力也非常適合更廣泛領域的驗證任務。「你可以驗證一個軟件是否完全按照你的要求做，或者可以驗證硬件芯片，因此它在金融交易算法和硬件設計中都會有所應用。」

利用機器探索數學是一個令人興奮的發展，倫敦數學科學研究所的 Yang-Hui He 說，但真正的挑戰是在大部分是用 LaTex 編寫的數學研究中使用該模型。「我們只用 LaTex 是因為它打字順暢，但它在某種意義上是一種自然語言，也有自己的規則。」

He 說，因為用戶可以在 LaTeX 中定義自己的函數和符號，這些函數和符號可能只在一篇數學論文中使用，這對于僅在純文本上訓練過的神經網絡來說可能很棘手。