Transformer的技能樹是越來越厲害了。

來自馬薩諸塞大學、谷歌和伊利諾伊大學厄巴納-香檳分校（UIUC）的研究人員發(fā)表了一篇論文，利用大語言模型自動生成定理的完整證明。

論文地址：https://arxiv.org/pdf/2303.04910.pdf

這篇工作以Baldur（北歐神話中雷神Thor的兄弟）命名，首次證明了使用Transformer生成全證明是可能的，并且當為模型提供額外的上下文時，還可以改進模型先前的證明。

文章發(fā)表于2023年12月在舊金山舉行的ESEC/FSE（ACM歐洲軟件工程聯(lián)合會議和軟件工程基礎研討會）上，并獲得了杰出論文獎（Distinguished Paper award）。

眾所周知，軟件存在bug（廢話），這在一般應用程序或者網(wǎng)站上問題不大，但對于比如加密協(xié)議、醫(yī)療設備和航天飛機等關鍵系統(tǒng)背后的軟件而言，必須確保沒有錯誤。

——一般的代碼審查和測試并不能給出這個保證，這需要形式驗證（formal verification）。

對于formal verification，ScienceDirect給出的解釋為：

the process of mathematically checking that the behavior of a system, described using a formal model, satisfies a given property, also described using a formal model

指的是從數(shù)學上檢查，使用形式模型描述的系統(tǒng)行為，是否滿足給定屬性的過程。

簡單來說就是，利用數(shù)學分析的方法，通過算法引擎建立模型，對待測設計的狀態(tài)空間進行窮盡分析的驗證。

形式化軟件驗證，對于軟件工程師來說是最具挑戰(zhàn)性的任務之一。例如CompCert，使用Coq交互式定理證明器驗證的C編譯器，是無處不在的GCC和LLVM等使用的唯一編譯器。

然而，手動形式驗證（編寫證明）的成本卻相當巨大，——C編譯器的證明是編譯器代碼本身的三倍以上。

所以，形式驗證本身是一項“勞動密集型”的任務，研究人員也在探索自動化的方法。

比如Coq和Isabelle等證明助手，通過訓練一個模型來一次預測一個證明步驟，并使用模型搜索可能的證明空間。

而本文的Baldur首次在這個領域引入了大語言模型的能力，在自然語言文本和代碼上訓練，并在證明上進行微調(diào)，

Baldur可以一次就生成定理的完整證明，而不是一次一個步驟。

如上圖所示，僅使用定理語句作為證明生成模型的輸入，然后從模型中抽取證明嘗試，并使用Isabelle執(zhí)行證明檢查。

如果Isabelle接受了證明嘗試而沒有錯誤，就說明證明成功；否則從證明生成模型中抽取另一個證明嘗試。

Baldur在6336個Isabelle/HOL定理及其證明的基準上進行評估，從經(jīng)驗上證明了完整證明生成、修復和添加上下文的有效性。

另外，這個工具之所以叫Baldur，可能是因為當前最好的自動證明生成工具叫做Thor。

Thor的證明率更高（57%），它使用較小的語言模型結合搜索可能證明空間的方法預測證明的下一步，而Baldur的優(yōu)勢在于它能夠生成完整的證明。

不過Thor和Baldur兩兄弟也可以一起工作，這樣可能把證明率提升到接近66%。

自動生成完整證明

Baldur由Google的大語言模型Minerva提供支持，Minerva在科學論文和包含數(shù)學表達式的網(wǎng)頁上進行訓練，并對有關證明和定理的數(shù)據(jù)進行了微調(diào)。

Baldur可以與定理證明助手Isabelle合作，Isabelle對證明結果進行檢查。當給定一個定理陳述時，Baldur幾乎在41%的時間內(nèi)能夠生成一個完整的證明。

為了進一步提高Baldur的性能，研究人員向模型提供了額外的上下文信息（比如其他定義、或理論文件中的定理陳述），這使證明率提高到47.5%。

這意味著Baldur能夠獲取上下文，并使用它來預測新的正確證明，——類似于程序員，當了解了相關方法和代碼之后，他們更有可能修復程序中的錯誤。

下面舉個例子（fun_sum_commute定理）：

這個定理來自形式證明檔案中一個名為多項式的項目。

當人工編寫證明的時候，會區(qū)分兩種情況：集合是有限的或者不是有限的：

所以，對于模型來說，輸入是定理陳述，而目標輸出是這個人工編寫的證明。

Baldur認識到這里需要歸納，并應用了一種特殊的歸納法則，稱為infinite_finite_induct，遵循與人類書面證明相同的總體方法，但更簡潔。

而因為需要歸納，Isabelle使用的Sledgehammer默認無法證明這個定理。

訓練

為了訓練證明生成模型，研究人員構建了一個新的證明生成數(shù)據(jù)集。

現(xiàn)有數(shù)據(jù)集包含單個證明步驟的示例，每個訓練示例包括證明狀態(tài)（輸入）和要應用的下一個證明步驟（目標）。

給定一個包含單個證明步驟的數(shù)據(jù)集，這里需要創(chuàng)建一個新數(shù)據(jù)集，以便訓練模型一次預測整個證明。

研究人員從數(shù)據(jù)集中提取每個定理的證明步驟，并將它們連接起來以重建原始證明。

證明修復

還是以上面的fun_sum_commute為例，

Baldur首次生成的證明嘗試，在證明檢查器中失敗。

Baldur試圖應用歸納法，但未能首先將證明分解為兩種情況（有限集與無限集）。Isabelle返回以下錯誤消息：

為了從這些字符串中派生出一個證明修復訓練示例，這里將定理陳述、失敗的證明嘗試和錯誤消息連接起來作為輸入，并使用正確的人工編寫的證明作為目標。

上圖詳細介紹了訓練數(shù)據(jù)的創(chuàng)建過程。

使用證明生成模型，針對原始訓練集中的每個問題，對溫度為0的證明進行采樣。

使用校對助手，記錄所有失敗的校樣及其錯誤消息，然后，繼續(xù)構建新的證明修復訓練集。

對于每個原始訓練示例，將定理語句、證明生成模型生成的（不正確的）候選證明以及相應的錯誤消息連接起來，以獲得新訓練示例的輸入序列。

添加上下文

在定理陳述之前添加理論文件的行，作為額外的上下文。比如下圖這樣：

Baldur中帶有上下文的證明生成模型，可以利用這些附加信息。出現(xiàn)在fun_sum_commute定理語句中的字符串，在這個上下文中再次出現(xiàn)，因此圍繞它們的附加信息可以幫助模型做出更好的預測。

上下文可以是陳述（定理、定義、證明），還可以是自然語言注釋。

為了利用LLM的可用輸入長度，研究人員首先從同一個理論文件中添加多達50個語句。

在訓練過程中，首先對所有這些語句進行標記化，然后截斷序列的左側(cè)以適應輸入長度。

上圖展示了有上下文和無上下文的生成模型的證明成功率與證明嘗試次數(shù)的關系圖。我們可以看出，具有上下文的證明生成模型始終優(yōu)于普通生成模型。

上圖展示了不同尺寸和溫度模型的已驗證定理與推理成本之比。

我們可以看到生成模型的證明成功率，以及8B模型和62B模型的上下文與證明嘗試次數(shù)的關系。

具有上下文的62B證明生成模型優(yōu)于具有上下文的8B模型。

不過，作者在這里強調(diào)，由于這些實驗的成本較高，他們也無法調(diào)整超參數(shù)，62B模型如果經(jīng)過優(yōu)化可能會表現(xiàn)得更好。