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

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

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

如今看來，計算機(jī)可以被用來驗證數(shù)學(xué)證明，但它們只有在使用專門設(shè)計的證明語言時才能做到這一點，而無法處理數(shù)學(xué)符號和數(shù)學(xué)家使用的書面文本的混合體。如果把用自然語言編寫的數(shù)學(xué)問題轉(zhuǎn)換為形式化代碼，讓計算機(jī)更容易解決它們，或許能夠幫助構(gòu)建能探索數(shù)學(xué)新發(fā)現(xiàn)的機(jī)器。這個過程被稱為形式化（formalisation），自動形式化（autoformalization）指的是自動從自然語言數(shù)學(xué)翻譯成形式化語言的任務(wù)。

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

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

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

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

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

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

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

方法

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

圖 1.

非形式化證明的起草

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

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

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

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

圖 2.

證明草圖中的公開猜想

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

實驗

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

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

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

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

當(dāng)切換到 Minerva（62B）模型時，成功率分別上升到 43.9% 和 37.7%。與人編寫的非形式化證明相比，其在驗證集上的成功率要高 1.3%，在測試集上要低 1.6%?？偟膩碚f，Minerva（62B）模型能夠解決 miniF2F 上的 199 個問題，比用人編寫的證明少一個。Minerva（540B）模型在 miniF2F 的驗證集和測試集中分別解決了 42.6% 和 38.9% 的問題，也生成了 199 個成功的證明。

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

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

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

更多內(nèi)容，請參考原論文。