計(jì)算機(jī)被用來(lái)驗(yàn)證數(shù)學(xué)證明已經(jīng)有一段時(shí)間了，但它們只有在使用專(zhuān)門(mén)設(shè)計(jì)的證明語(yǔ)言準(zhǔn)備問(wèn)題時(shí)才能做到這一點(diǎn)，而無(wú)法處理數(shù)學(xué)符號(hào)和數(shù)學(xué)家使用的書(shū)面文本的混合體。

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

這個(gè)過(guò)程被稱(chēng)為形式化（formalisation），但僅僅一個(gè)證明就可能需要數(shù)年的工作，因此只有一小部分?jǐn)?shù)學(xué)知識(shí)被形式化，然后由機(jī)器證明。

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

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

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

將 12500 個(gè)中學(xué)數(shù)學(xué)競(jìng)賽問(wèn)題形式化

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

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

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

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

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

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

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

自動(dòng)形式化的問(wèn)題將 MiniF2F 的成功率從 29% 提高到了 35%，這表明 Codex 在問(wèn)題形式化方面取得了重要進(jìn)展。

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

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

用來(lái)進(jìn)行自動(dòng)形式化的 prompt 格式是：

AI 將與人類(lèi)數(shù)學(xué)家競(jìng)爭(zhēng)？

這是一項(xiàng)有趣的進(jìn)展，但 Wu 表示團(tuán)隊(duì)的工作只是一個(gè)概念證明?！溉绻繕?biāo)是訓(xùn)練一臺(tái)媲美最頂級(jí)人類(lèi)數(shù)學(xué)家的機(jī)器，那么自動(dòng)形式化似乎是實(shí)現(xiàn)這個(gè)目標(biāo)的關(guān)鍵道路。」

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

團(tuán)隊(duì)近期的目標(biāo)是改進(jìn)自動(dòng)形式化模型和自動(dòng)化證明機(jī)器，但研究成果的未來(lái)影響將會(huì)更深遠(yuǎn)。Wu 表示，這些模型可以揭示人類(lèi)目前未知的數(shù)學(xué)領(lǐng)域。

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

利用機(jī)器探索數(shù)學(xué)是一個(gè)令人興奮的發(fā)展，倫敦?cái)?shù)學(xué)科學(xué)研究所的 Yang-Hui He 說(shuō)，但真正的挑戰(zhàn)是在大部分是用 LaTex 編寫(xiě)的數(shù)學(xué)研究中使用該模型?！肝覀冎挥?LaTex 是因?yàn)樗蜃猪槙常谀撤N意義上是一種自然語(yǔ)言，也有自己的規(guī)則?！?/p>

He 說(shuō)，因?yàn)橛脩艨梢栽?LaTeX 中定義自己的函數(shù)和符號(hào)，這些函數(shù)和符號(hào)可能只在一篇數(shù)學(xué)論文中使用，這對(duì)于僅在純文本上訓(xùn)練過(guò)的神經(jīng)網(wǎng)絡(luò)來(lái)說(shuō)可能很棘手。