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

如果把用自然語言編寫的數(shù)學(xué)問題轉(zhuǎn)換為正式代碼，讓計算機更容易解決它們，或許能夠幫助構(gòu)建能探索數(shù)學(xué)新發(fā)現(xiàn)的機器。

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

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

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

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

將 12500 個中學(xué)數(shù)學(xué)競賽問題形式化

大型語言模型的一系列最新進展展示了模型理解形式化語言的潛力。然而，現(xiàn)有的成功僅限于在網(wǎng)絡(luò)上存在大量語料庫的形式化語言 (例如 Python)。相比之下，形式化的數(shù)學(xué)數(shù)據(jù)非常缺乏，最大的形式化數(shù)學(xué)語言庫之一 Archive of Formal Proofs 只有 180mb 大小，這還不到大語言模型 Codex 訓(xùn)練數(shù)據(jù)的 0.18% 。

此外，與通用編程語言的情況不同，自然語言文檔字符串是廣泛可用的，自然語言和形式化數(shù)學(xué)語言之間幾乎沒有對齊的數(shù)據(jù)。因此，大型語言模型的成功是否能直接促進自動形式化的發(fā)展，仍是未知的。

鑒于證明語言與編程語言有相似之處，因此該團隊決定看看 Codex 是否可以將包含 12500 個中學(xué)數(shù)學(xué)競賽問題的庫形式化。它能夠?qū)⑺姆种坏膯栴}轉(zhuǎn)換為與形式證明求解程序 Isabelle 兼容的格式。

Wu 表示，許多不成功的轉(zhuǎn)換是系統(tǒng)不理解某些數(shù)學(xué)概念的結(jié)果?！溉绻阌靡粋€解釋這個概念的例子來展示模型，那么模型就可以快速掌握它?！?/p>

這項工作探討了大語言模型的自動形式化的前景，研究者發(fā)現(xiàn)大型語言模型已經(jīng)在一個交互式定理證明器中具備相當好的形式化自然語言數(shù)學(xué)的能力。

下圖 1 是一個完美的自動形式化示例。該模型不僅轉(zhuǎn)換成了語法上正確的 Isabelle 代碼，而且還能夠掌握自然語言中的重要推理點。

為了測試這種自動形式化程序的效力，團隊隨后又將 Codex 應(yīng)用于一組已經(jīng)有人類形式化版本的問題，Codex 也為這些問題生成了自己的形式化版本。團隊使用了另一個名為 MiniF2F 的 AI 來解決這兩個版本的問題。

自動形式化的問題將 MiniF2F 的成功率從 29% 提高到了 35%，這表明 Codex 在問題形式化方面取得了重要進展。

值得注意的是，許多數(shù)學(xué)競賽的陳述往往是這樣一種形式：一個人被要求找到某個問題的答案，而不是證明一個給定的命題。然而形式化的數(shù)學(xué)陳述是以命題的形式，而不是以問題的形式。

為了把一個問題轉(zhuǎn)換成一個命題，研究者在問題后面附上了「The Final Answer」:

用來進行自動形式化的 prompt 格式是：

AI 將與人類數(shù)學(xué)家競爭？

這是一項有趣的進展，但 Wu 表示團隊的工作只是一個概念證明。「如果目標是訓(xùn)練一臺媲美最頂級人類數(shù)學(xué)家的機器，那么自動形式化似乎是實現(xiàn)這個目標的關(guān)鍵道路?！?/p>

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

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

這種機器的推理能力也非常適合更廣泛領(lǐng)域的驗證任務(wù)?！改憧梢则炞C一個軟件是否完全按照你的要求做，或者可以驗證硬件芯片，因此它在金融交易算法和硬件設(shè)計中都會有所應(yīng)用。」

利用機器探索數(shù)學(xué)是一個令人興奮的發(fā)展，倫敦數(shù)學(xué)科學(xué)研究所的 Yang-Hui He 說，但真正的挑戰(zhàn)是在大部分是用 LaTex 編寫的數(shù)學(xué)研究中使用該模型?！肝覀冎挥?LaTex 是因為它打字順暢，但它在某種意義上是一種自然語言，也有自己的規(guī)則?！?/p>

He 說，因為用戶可以在 LaTeX 中定義自己的函數(shù)和符號，這些函數(shù)和符號可能只在一篇數(shù)學(xué)論文中使用，這對于僅在純文本上訓(xùn)練過的神經(jīng)網(wǎng)絡(luò)來說可能很棘手。