Transformer的技能樹是越來越厲害了。
來自麻薩諸塞大學、Google和伊利諾大學厄巴納-香檳分校（UIUC）的研究人員，最近發表了一篇論文，他們透過使用大型語言模型，成功地實現了自動產生完整定理證明的目標。
論文網址：https://arxiv.org/pdf/2303.04910.pdf
這篇工作以Baldur（北歐神話中雷神Thor的兄弟）命名，首次證明了Transformer可以產生全證明，還表明在為模型提供額外上下文時，可以改進模型先前的證明。
這篇論文在2023年12月的ESEC/FSE（ACM歐洲軟體工程聯合會議和軟體工程基礎研討會）上發表，並榮獲傑出論文獎。
眾所周知，軟體中不可避免地存在著bug，這對一般應用程式或網站來說可能不會帶來太大問題。然而，對於關鍵系統背後的軟體，如加密協議、醫療設備和太空梭，我們必須確保沒有任何錯誤。
－一般的程式碼審查和測試並不能給予這個保證，這需要形式驗證（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
指的是從數學上檢查，使用形式模型描述的系統行為，是否滿足給定屬性的過程。
簡單來說就是，利用數學分析的方法，透過演算法引擎建立模型，對待測設計的狀態空間進行窮盡分析的驗證。
形式化軟體驗證，對軟體工程師來說是最具挑戰性的任務之一。例如CompCert，使用Coq互動式定理證明器驗證的C編譯器，是無所不在的GCC和LLVM等所使用的唯一編譯器。
然而，手動形式驗證（編寫證明）的成本卻相當巨大，－C編譯器的證明是編譯器程式碼本身的三倍以上。
所以，形式驗證本身就是一項「勞力密集」的任務，研究人員也在探索自動化的方法。
例如Coq和Isabelle等證明助手，透過訓練一個模型來一次預測一個證明步驟，並使用模型搜尋可能的證明空間。
而本文的Baldur首次在這個領域引入了大語言模型的能力，在自然語言文字和程式碼上訓練，並在證明上進行微調，
Baldur可以一次就產生定理的完整證明，而不是一次一個步驟。
如上圖所示，僅使用定理語句作為證明產生模型的輸入，然後從模型中抽取證明嘗試，並使用Isabelle執行證明檢查。
如果Isabelle接受了證明嘗試而沒有錯誤，就表示證明成功；否則從證明生成模型中抽取另一個證明嘗試。
Baldur在6336個Isabelle/HOL定理及其證明的基準上進行評估，從經驗上證明了完整證明生成、修復和添加上下文的有效性。
另外，這個工具之所以叫Baldur，可能是因為目前最好的自動證明產生工具叫做Thor。
Thor的證明率更高（57%），它使用較小的語言模型結合搜尋可能證明空間的方法預測證明的下一步，而Baldur的優勢在於它能夠產生完整的證明。
不過Thor和Baldur兩兄弟也可以一起工作，這樣可能把證明率提升到接近66%。
Baldur由Google的大語言模型Minerva提供支持，Minerva在科學論文和包含數學表達式的網頁上進行訓練，並對有關證明和定理的資料進行了微調。
Baldur可以與定理證明助手Isabelle合作，Isabelle檢視證明結果。當給定一個定理陳述時，Baldur幾乎在41%的時間內能夠產生一個完整的證明。
為了進一步提高Baldur的性能，研究人員向模型提供了額外的上下文資訊（例如其他定義、或理論文件中的定理陳述），這使證明率提高到47.5%。
這意味著Baldur能夠取得上下文，並使用它來預測新的正確證明，——類似於程式設計師，當了解了相關方法和程式碼之後，他們更有可能修復程式中的錯誤。
以下舉例（fun_sum_commute定理）：
這個定理來自形式證明檔案中一個名為多項式的項目。
當手動寫證明的時候，會區分兩種情況：集合是有限的或不是有限的：
#所以，對模型來說，輸入就是定理陳述，而目標輸出就是這個人工編寫的證明。
Baldur認識到這裡需要歸納，並應用了一種特殊的歸納法則，稱為infinite_finite_induct，遵循與人類書面證明相同的總體方法，但更簡潔。
而因為需要歸納，Isabelle所使用的Sledgehammer預設無法證明這個定理。
訓練
給定一個包含單一證明步驟的資料集，這裡需要建立一個新資料集，以便訓練模型一次預測整個證明。
研究人員從資料集中提取每個定理的證明步驟，並將它們連接起來以重建原始證明。
證明修復
##########還是以上面的fun_sum_commute為例，########## ###########Baldur首次產生的證明嘗試，在證明檢查器中失敗。 ############Baldur試圖應用歸納法，但未能先將證明分解為兩種情況（有限集合與無限集合）。 Isabelle傳回以下錯誤訊息：######
為了從這些字串中衍生出一個證明修復訓練範例，這裡將定理陳述、失敗的證明嘗試和錯誤訊息連接起來作為輸入，並使用正確的人工編寫的證明作為目標。
上圖詳細介紹了訓練資料的建立過程。
使用證明產生模型，針對原始訓練集中的每個問題，對溫度為0的證明進行採樣。
使用校對助手，記錄所有失敗的校樣及其錯誤訊息，然後，繼續建立新的證明修復訓練集。
對於每個原始訓練範例，將定理語句、證明產生模型產生的（不正確的）候選證明以及對應的錯誤訊息連接起來，以獲得新訓練範例的輸入序列。
在定理陳述之前加入理論文件的行，作為額外的上下文。例如下圖這樣：
Baldur中帶有上下文的證明產生模型，可以利用這些附加資訊。出現在fun_sum_commute定理語句中的字串，在這個上下文中再次出現，因此圍繞它們的附加資訊可以幫助模型做出更好的預測。
上下文可以是陳述（定理、定義、證明），也可以是自然語言註解。
為了利用LLM的可用輸入長度，研究人員首先從同一個理論檔案中加入多達50個語句。
在訓練過程中，首先將所有這些語句標記化，然後截斷序列的左側以適應輸入長度。
上圖展示了有上下文和無上下文的生成模型的證明成功率與證明嘗試次數的關係圖。我們可以看出，具有上下文的證明生成模型始終優於普通生成模型。
上圖展示了不同尺寸和溫度模型的已驗證定理與推理成本之比。
我們可以看到生成模型的證明成功率，以及8B模型和62B模型的上下文與證明嘗試次數的關係。
具有上下文的62B證明生成模型優於具有上下文的8B模型。
不過，作者在這裡強調，由於這些實驗的成本較高，他們也無法調整超參數，62B模型如果經過最佳化可能會表現得更好。
以上是陶哲軒看了都直呼內行人！谷歌等用LLM自動證明定理拿頂會傑出論文，上下文越全證越好的詳細內容。更多資訊請關注PHP中文網其他相關文章！
