自動(dòng)證明數(shù)學(xué)定理是人工智能的一個(gè)初衷，也是一直以來(lái)的難題。到目前為止，人類數(shù)學(xué)家使用了兩種不同的方式來(lái)書(shū)寫(xiě)數(shù)學(xué)。

第一種是大家都熟悉的方式，即用自然語(yǔ)言來(lái)描述數(shù)學(xué)證明。大部分的數(shù)學(xué)都是以這種方式書(shū)寫(xiě)的，這包括數(shù)學(xué)課本，數(shù)學(xué)論文，等等。

第二種稱之為形式化數(shù)學(xué)（formal mathematics）。這是近半個(gè)世紀(jì)計(jì)算機(jī)科學(xué)家創(chuàng)造的，用來(lái)檢驗(yàn)數(shù)學(xué)證明的一種工具。

如今看來(lái)，計(jì)算機(jī)可以被用來(lái)驗(yàn)證數(shù)學(xué)證明，但它們只有在使用專門(mén)設(shè)計(jì)的證明語(yǔ)言時(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ò)程被稱為形式化（formalisation），自動(dòng)形式化（autoformalization）指的是自動(dòng)從自然語(yǔ)言數(shù)學(xué)翻譯成形式化語(yǔ)言的任務(wù)。

形式化證明的自動(dòng)化是一項(xiàng)具有挑戰(zhàn)性的任務(wù)，深度學(xué)習(xí)方法在該領(lǐng)域尚未大獲成功，這主要是因?yàn)樾问交瘮?shù)據(jù)的稀缺。事實(shí)上，形式化證明本身是非常困難的，且只有少數(shù)專家能做到，這使得大規(guī)模的注釋工作并不現(xiàn)實(shí)。最大的形式化證明語(yǔ)料庫(kù)是用 Isabelle 代碼 (Paulson, 1994) 編寫(xiě)的，大小不到 0.6GB，比視覺(jué)或自然語(yǔ)言處理中常用的數(shù)據(jù)集小幾個(gè)數(shù)量級(jí)。為了解決形式證明的稀缺性，以往的研究提出使用合成數(shù)據(jù)、自監(jiān)督或強(qiáng)化學(xué)習(xí)來(lái)合成額外的形式化訓(xùn)練數(shù)據(jù)。雖然這些方法在一定程度上緩解了數(shù)據(jù)的不足，但都無(wú)法將大量人工撰寫(xiě)的數(shù)學(xué)證明充分利用起來(lái)。

我們以語(yǔ)言模型 Minerva為例。當(dāng)在足夠多的數(shù)據(jù)訓(xùn)練之后，我們發(fā)現(xiàn)它的數(shù)學(xué)能力非常強(qiáng)，可以在高中數(shù)學(xué)測(cè)試中拿到高于平均分水平。然而這樣的語(yǔ)言模型也有不足，它只能模仿，而不能自主訓(xùn)練而提高數(shù)學(xué)水平。形式化證明系統(tǒng)提供了一個(gè)訓(xùn)練環(huán)境，但形式化數(shù)學(xué)的數(shù)據(jù)非常少。

與形式化的數(shù)學(xué)不同，非形式化的數(shù)學(xué)數(shù)據(jù)是豐富和廣泛可用的。最近，在非形式化數(shù)學(xué)數(shù)據(jù)上訓(xùn)練的大型語(yǔ)言模型展示了令人印象深刻的定量推理能力。然而，它們經(jīng)常產(chǎn)生錯(cuò)誤的證明，而自動(dòng)檢測(cè)這些證明中的錯(cuò)誤推理是很有挑戰(zhàn)性的。

在最近的一項(xiàng)工作中，谷歌的吳宇懷 (Yuhuai Tony Wu)等研究者設(shè)計(jì)了一種叫做 DSP（Draft, Sketch, and Prove ）的新方法，將非形式化的數(shù)學(xué)證明轉(zhuǎn)化為形式化的證明，從而同時(shí)具備形式化系統(tǒng)提供的邏輯嚴(yán)謹(jǐn)性和大量的非形式化數(shù)據(jù)。

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

今年早些時(shí)候，吳宇懷與幾位合作者使用了 OpenAI Codex 的神經(jīng)網(wǎng)絡(luò)進(jìn)行自動(dòng)形式化工作，證明了用大型語(yǔ)言模型將非形式化語(yǔ)句自動(dòng)翻譯成形式化語(yǔ)句的可行性。DSP 則更進(jìn)一步，利用大型語(yǔ)言模型從非形式化證明中生成形式化證明草圖。證明草圖由高層次的推理步驟組成，可以由交互式定理證明器這樣的形式化系統(tǒng)來(lái)解釋。它們與完整的形式化證明不同，因?yàn)樗鼈儼瑹o(wú)理由的中間猜想的序列。在 DSP 的最后一步，形式化證明草圖被闡述為一個(gè)完整的形式化證明，使用一個(gè)自動(dòng)驗(yàn)證器來(lái)證明所有中間猜想。

吳宇懷表示：現(xiàn)在，我們展示了 LLM 可以將其生成的非形式化證明轉(zhuǎn)化為經(jīng)過(guò)驗(yàn)證的形式化證明！

方法

方法部分描述了用于形式化證明自動(dòng)化的 DSP方法，該方法利用非形式化證明來(lái)指導(dǎo)自動(dòng)形式化定理證明器的證明草圖。這里假設(shè)每個(gè)問(wèn)題都有一個(gè)非形式化命題和一個(gè)描述該問(wèn)題的形式化命題。整體 pipeline 包括三個(gè)階段（如圖 1 所示）。

圖 1.

非形式化證明的起草

DSP 方法的初始階段，包括根據(jù)問(wèn)題的自然數(shù)學(xué)語(yǔ)言描述（可能用 LATEX）為其尋找非形式化證明。由此產(chǎn)生的非形式化證明被看作是后續(xù)階段的草稿。在數(shù)學(xué)教科書(shū)中，一般都會(huì)提供定理的證明，但有時(shí)會(huì)缺失或不完整。因此，研究者考慮了與非形式化證明的存在或不存在相對(duì)應(yīng)的兩種情況。

在第一種情況下，研究者假設(shè)有一個(gè)「真實(shí)的」非形式化證明（即由人寫(xiě)的證明），這是現(xiàn)有數(shù)學(xué)理論形式化實(shí)踐中的典型情況。在第二種情況下，研究者做了一個(gè)更普遍的假設(shè)，即沒(méi)有給出真實(shí)的非形式化證明，并且用一個(gè)經(jīng)過(guò)非形式化數(shù)學(xué)數(shù)據(jù)訓(xùn)練的大型語(yǔ)言模型來(lái)起草證明候選。該語(yǔ)言模型消除了對(duì)人類證明的依賴，并能為每個(gè)問(wèn)題產(chǎn)生多種備選解決方案。雖然沒(méi)有簡(jiǎn)單的方法來(lái)自動(dòng)驗(yàn)證這些證明的正確性，但非形式化證明只需要在下一階段對(duì)生成一個(gè)好的形式化證明草圖有用。

將非形式化證明映射為形式化草圖

形式化證明草圖對(duì)解決方案的結(jié)構(gòu)進(jìn)行編碼，并撇開(kāi)低層次的細(xì)節(jié)。直觀地說(shuō)，它是一個(gè)部分證明，概述了高層次的猜想命題。圖 2 是一個(gè)證明草圖的具體例子。盡管非形式化證明經(jīng)常撇開(kāi)低層次的細(xì)節(jié)，這些細(xì)節(jié)不能在形式化證明中排出，這使得非形式化證明到形式化證明的直接轉(zhuǎn)換變得困難。相反，本文建議將非形式化證明映射到共享相同高層結(jié)構(gòu)的形式化證明草圖上。證明草圖中缺少的低層次細(xì)節(jié)可以由自動(dòng)證明器來(lái)填補(bǔ)。由于大型非形式化 - 形式化平行語(yǔ)料庫(kù)不存在，標(biāo)準(zhǔn)的機(jī)器翻譯方法不適合這項(xiàng)任務(wù)。相反，這里使用一個(gè)大型語(yǔ)言模型的小樣本學(xué)習(xí)能力。具體來(lái)說(shuō)，用了一些包含非形式化證明及其相應(yīng)的形式化草圖的例子對(duì)來(lái) prompt 該模型，然后是一個(gè)有待轉(zhuǎn)換的非形式化證明，然后讓模型生成后續(xù)的 token，以獲得所需的形式化草圖。這個(gè)模型稱為「自動(dòng)形式化器」。

圖 2.

證明草圖中的公開(kāi)猜想

作為這個(gè)過(guò)程的最后一部分，研究者執(zhí)行現(xiàn)成的自動(dòng)證明器來(lái)填補(bǔ)證明草圖中缺失的細(xì)節(jié)，這里的「自動(dòng)證明器」是指能夠產(chǎn)生形式上可驗(yàn)證的證明的系統(tǒng)。該框架對(duì)自動(dòng)證明器的具體選擇是不可知的：它可以是符號(hào)證明器（如啟發(fā)式證明自動(dòng)化工具）、基于神經(jīng)網(wǎng)絡(luò)的證明器或者混合方法。如果自動(dòng)證明器成功地填補(bǔ)了證明草圖中的所有空白，它就會(huì)返回最終的形式化證明，可以對(duì)照問(wèn)題的規(guī)格進(jìn)行檢查。如果自動(dòng)證明器失敗（例如，它超過(guò)了分配的時(shí)間限制），則認(rèn)為評(píng)估是不成功的。

實(shí)驗(yàn)

研究者進(jìn)行了一系列實(shí)驗(yàn)，包括從 miniF2F 數(shù)據(jù)集中生成問(wèn)題的形式化證明，并表明很大一部分定理可以用這種方法自動(dòng)證明。此處研究了兩種環(huán)境，其中非形式化證明是由人類寫(xiě)的，或者是由一個(gè)在數(shù)學(xué)文本上訓(xùn)練的大型語(yǔ)言模型起草的。這兩種設(shè)置對(duì)應(yīng)于現(xiàn)有理論形式化過(guò)程中經(jīng)常出現(xiàn)的情況，即通常有非形式化證明，但有時(shí)作為練習(xí)留給讀者，或者由于空白處的限制而缺失。

表 1 展示了在 miniF2F 數(shù)據(jù)集上發(fā)現(xiàn)的成功形式化證明的比例。結(jié)果包括本文實(shí)驗(yàn)的四條 baseline，以及帶有人類編寫(xiě)的證明和模型生成的證明的 DSP 方法。

可以看出，附加了 11 種啟發(fā)式策略的自動(dòng)證明器大大增加了 Sledgehammer 的性能，在 miniF2F 的驗(yàn)證集上將其成功率從 9.9% 提高到 18.0%，在測(cè)試集上從 10.4% 提高到 20.9%。兩個(gè)使用語(yǔ)言模型和證明搜索的 baseline 在 miniF2F 的測(cè)試集上分別達(dá)到 29.9% 和 35.2% 的成功率。

基于人類編寫(xiě)的非形式化證明，DSP 方法在 miniF2F 的驗(yàn)證和測(cè)試集上取得了 42.6% 和 39.3% 的成功率。488 個(gè)問(wèn)題中共有 200 個(gè)可以通過(guò)這種方式進(jìn)行證明。Codex 模型和 Minerva（8B）模型在解決 miniF2F 上的問(wèn)題時(shí)給出了非常相似的結(jié)果：它們都指導(dǎo)自動(dòng)驗(yàn)證器分別解決了驗(yàn)證集和測(cè)試集上 40.6% 和 35.3% 的問(wèn)題。

當(dāng)切換到 Minerva（62B）模型時(shí)，成功率分別上升到 43.9% 和 37.7%。與人編寫(xiě)的非形式化證明相比，其在驗(yàn)證集上的成功率要高 1.3%，在測(cè)試集上要低 1.6%。總的來(lái)說(shuō)，Minerva（62B）模型能夠解決 miniF2F 上的 199 個(gè)問(wèn)題，比用人編寫(xiě)的證明少一個(gè)。Minerva（540B）模型在 miniF2F 的驗(yàn)證集和測(cè)試集中分別解決了 42.6% 和 38.9% 的問(wèn)題，也生成了 199 個(gè)成功的證明。

在兩種情況下，DSP 方法都能有效地指導(dǎo)自動(dòng)證明器：使用人類的非形式化證明或語(yǔ)言模型生成的非形式化證明。DSP 幾乎將證明器的成功率提高了一倍，并在使用 Isabelle 的 miniF2F 上產(chǎn)生了 SOTA 性能。此外，更大的 Minerva 模型在指導(dǎo)自動(dòng)形式化證明器方面幾乎和人類一樣有幫助。

如下圖所示，DSP 方法顯著提高了 Sledgehammer + 啟發(fā)式證明器的性能（~20% -> ~40%），在 miniF2F 上實(shí)現(xiàn)了新的 SOTA。

Minerva 的 62B 和 540B 版本生成的證明與人類的證明非常相似。