Lean Copilot，讓陶哲軒等眾多數(shù)學(xué)家讚不絕口的這個(gè)形式化數(shù)學(xué)工具，又有超強(qiáng)進(jìn)化了？

就在剛剛，加州理工學(xué)院教授Anima Anandkumar宣布，團(tuán)隊(duì)發(fā)布了Lean Copilot論文的擴(kuò)展版本，並且更新了程式碼庫(kù)。

圖片

論文網(wǎng)址：https://arxiv.org/pdf/2404.12534.pdf

#最新實(shí)驗(yàn)表明，這個(gè)Copilot工具，可以自動(dòng)化80%以上的數(shù)學(xué)證明步驟了！這個(gè)紀(jì)錄，比以前的基線(xiàn)aesop還要好2.3倍。

並且，和以前一樣，它在MIT許可下是開(kāi)源的。

圖片

他是華人小哥宋沛洋，他是UCSB的榮譽(yù)CS本科生，加州理工學(xué)院計(jì)算數(shù)學(xué)科學(xué)（CMS）系的SURF研究員。

網(wǎng)友驚呼：所以，陶哲軒現(xiàn)在的數(shù)學(xué)研究可以原地加速5倍了？

圖片

LLM提出證明策略，人類(lèi)無(wú)縫幹預(yù)

團(tuán)隊(duì)就發(fā)布了這個(gè)Lean Copilot的工具，希望啟動(dòng)人類(lèi)和LLM的協(xié)作，寫(xiě)出100%準(zhǔn)確的形式化數(shù)學(xué)證明。

它解決了一個(gè)核心技術(shù)挑戰(zhàn)：在Lean中運(yùn)行LLM的推理。

透過(guò)這個(gè)工具，我們可以讓LLM在Lean中提出證明策略，讓人類(lèi)以無(wú)縫的方式介入和修改。

圖片

之所以開(kāi)發(fā)這個(gè)項(xiàng)目，是因?yàn)樽詣?dòng)化定理證明在如今仍是一項(xiàng)艱鉅的挑戰(zhàn)。

我們都知道，LLM在做數(shù)學(xué)和推理任務(wù)時(shí)，常常會(huì)犯錯(cuò)、產(chǎn)生幻覺(jué)，十分不可靠。

圖片

因此，到目前為止，數(shù)學(xué)證明大多是手動(dòng)推導(dǎo)的，需要仔細(xì)驗(yàn)證。

像Lean這的定理證明工具，倒是可以形式化證明過(guò)程的每一步，但人類(lèi)寫(xiě)起Lean，實(shí)在很費(fèi)力。

在這種情況下，Lean Copilot的誕生就顯得意義重大。

讓陶哲軒多次震驚的神器：數(shù)學(xué)家還不會(huì)用就完蛋了

LLM可以作為輔助人類(lèi)證明定理的工具，這論點(diǎn)已經(jīng)被陶哲軒多次證實(shí)了。

他前腳剛在部落格預(yù)測(cè)，26年AI將和搜尋、符號(hào)數(shù)學(xué)工具結(jié)合，成為數(shù)學(xué)研究中值得信賴(lài)的合著者。

緊接著，佐證他觀點(diǎn)的研究就如雨後春筍一般源源不絕地冒出來(lái)。

去年6月，加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者，就建構(gòu)了一個(gè)基於開(kāi)源LLM的定理證明器LeanDojo。

圖片

9月，微軟亞洲研究院、北大、北航等機(jī)構(gòu)的研究人員，透過(guò)97個(gè)回合的「蘇格拉底式」嚴(yán)格推理，成功讓GPT-4得出了「P≠NP」的結(jié)論，破解了這個(gè)千禧年難題 。

圖片

在第97輪對(duì)話(huà)中，GPT-4得出結(jié)論，證明範(fàn)例在沒(méi)有窮舉法的情況下無(wú)法求解，證明了結(jié)論為P≠NP

去年10月，陶哲軒在GPT-4、Copilot的幫助下，直接發(fā)現(xiàn)了自己論文中的一處隱藏bug。

在用Lean4形式化第6頁(yè)論點(diǎn)的過(guò)程中發(fā)現(xiàn)，他發(fā)現(xiàn)表達(dá)式

圖片

在n=3,k=2時(shí)，其實(shí)是發(fā)散的。

這個(gè)不太容易看出的bug能被及時(shí)抓住，多虧了Lean4。原因是，Lean要求他建構(gòu)02。由此，Lean無(wú)法基於負(fù)的0

圖片

這個(gè)發(fā)現(xiàn)直接讓陶哲軒瞳孔震驚。

圖片

而在去年年底，#陶哲軒直接成功地用AI工具，完成了形式化多項(xiàng)式Freiman-Ruzsa猜想證明過(guò)程的工作。

圖片

最後，依賴(lài)關(guān)係圖已經(jīng)完全被綠色所覆蓋，Lean編譯器也報(bào)告說(shuō)，這個(gè)猜想完全遵循標(biāo)準(zhǔn)公理。

圖片

在這個(gè)過(guò)程中，所有最前線(xiàn)的數(shù)學(xué)研究者，都在第一時(shí)間感受到了AI對(duì)於數(shù)學(xué)研究顛覆力量的直接衝擊。

Lean Coilot，讓Lean更好用

而今天，Lean Copilot的這項(xiàng)研究，讓Lean直接變得更強(qiáng)大了。

在這篇論文中，團(tuán)隊(duì)基於Lean Copilot建立了一些工具，用於建議證明步驟（策略建議）、完成中間證明目標(biāo)（證明搜尋）和使用LLM選擇相關(guān)前提（前提選擇）。

實(shí)驗(yàn)結(jié)果也充分證明了，跟Lean中現(xiàn)有的基於規(guī)則的證明自動(dòng)化相比，Lean Copilot在輔助人類(lèi)自動(dòng)化定理證明上，是有效的。

Lean Copilot提供了一個(gè)通用框架，可以透過(guò)CTranslate 2在本地，或在伺服器上執(zhí)行LLM的推理。

透過(guò)這個(gè)框架，使用者就能創(chuàng)造各種自動(dòng)化證明工具。

圖片

Lean是數(shù)學(xué)家中很受歡迎的證明助手。如下圖所示，Lean中的一個(gè)證明，是由一系列被稱(chēng)為策略（tactics）的證明步驟組成。

圖片

從整個(gè)定理開(kāi)始作為初始目標(biāo)，策略反覆地將目前的目標(biāo)轉(zhuǎn)換為更簡(jiǎn)單的子目標(biāo)，直到所有目標(biāo)都解決。

使用者在由VSCode驅(qū)動(dòng)的IDE中互動(dòng)編寫(xiě)策略，在右邊的infoview面板中顯示目標(biāo)。

產(chǎn)生策略建議

利用Lean Copilot，團(tuán)隊(duì)建立了suggest_tropics，一種用LLM產(chǎn)生策略建議的工具。

而它本身，也是一種策略。

應(yīng)用程式時(shí)，它會(huì)將目前目標(biāo)輸入LLM，並且從LLM取得產(chǎn)生的策略候列表。

它會(huì)查看每個(gè)選項(xiàng)，看它們是否會(huì) 1）導(dǎo)致錯(cuò)誤；2）結(jié)果沒(méi)有錯(cuò)，但不能完成證明；3）順利完成證明。

如果是1），這個(gè)策略就會(huì)被刪除。

圖片

只有無(wú)錯(cuò)誤的策略，才會(huì)顯示在右邊的視圖面板中。

其中，成功完成證明的策略，使用綠色標(biāo)記（類(lèi)別3）；沒(méi)有錯(cuò)誤改變證明目標(biāo)，但未完成證明的策略，使用藍(lán)色標(biāo)記（類(lèi)別2）。

注意！當(dāng)所有列出的策略都屬於類(lèi)別2時(shí)，這個(gè)資訊對(duì)於使用者來(lái)說(shuō)，可能極有價(jià)值。

在這種情況下，剩餘目標(biāo)的訊息，可以直接幫助使用者選擇策略，作為下一個(gè)中間證明步驟。

看到建議後，使用者可以選擇是否接受，或使用它們作為靈感來(lái)源，制定新策略。

例如，我們?cè)贚ean程式碼中定義了一個(gè)定理add_abc，它的初始目標(biāo)如圖3右所示。

圖片

當(dāng)我們輸入suggest_tropics時(shí)，會(huì)在右邊看到策略建議。

第一個(gè)策略顯示為綠色，表示證明已成功完成。

接下來(lái)三個(gè)建議都是藍(lán)色，這表示無(wú)法直接完成證明，但不會(huì)導(dǎo)致錯(cuò)誤。

因而，它們很有可能是有效的中間證明步驟！

同時(shí)，剩餘子目標(biāo)也顯示了出來(lái)。

而Tactic state欄位顯示No goal，是因?yàn)橹辽儆幸粋€(gè)策略建議可以被證明。

圖片

搜尋完整證明

此外，因?yàn)槿祟?lèi)和機(jī)器都不能始終如一地產(chǎn)生正確的策略，因此在這個(gè)過(guò)程中必須回溯、探索不同的替代方案，這個(gè)過(guò)程就是證明搜尋。

當(dāng)是上面所說(shuō)的Suggest_tropics，僅能產(chǎn)生目前步驟的策略，不具備搜尋多策略證明的能力。

為此，團(tuán)隊(duì)將其與基於規(guī)則的證明搜尋工具aesop結(jié)合起來(lái)，建立了一個(gè)基於LLM的證明搜尋工具。

Aesop會(huì)將最佳優(yōu)先搜尋作為L(zhǎng)ean的策略實(shí)施，並且允許使用者配置搜尋樹(shù)的擴(kuò)展方式。

圖片

搜尋樹(shù)是由作為節(jié)點(diǎn)的目標(biāo)組成。

起初，它只有原始目標(biāo)作為根節(jié)點(diǎn)。在每一步中，aesop都會(huì)選擇最有希望的未擴(kuò)展節(jié)點(diǎn)，透過(guò)應(yīng)用程式策略對(duì)其擴(kuò)展，將產(chǎn)生的節(jié)點(diǎn)新增為子節(jié)點(diǎn)。

圖片

而當(dāng)aesop找到一條從根源到可輕鬆解決的目標(biāo)的路徑，就證明搜尋成功了！

因此，aesop的效能關(guān)鍵取決於使用者是否配置了有效的規(guī)則集。

這就可以看出，aesop缺乏彈性。因此，Search_proof透過(guò)在每個(gè)步驟中由suggest_tropics產(chǎn)生的目標(biāo)相關(guān)策略，來(lái)增強(qiáng)aesop的規(guī)則集，讓它變得更加靈活。

對(duì)於圖3中的原始目標(biāo)，使用者只需輸入search_prrof，找到可以解決目標(biāo)的完整證明，就顯示在了資訊視圖中（圖5右）。

可以看到，由於發(fā)現(xiàn)了成功的證據(jù)，所以剩餘的Tactic state是No goals。

圖片

選擇註解好的前提

此外，定理證明中另一個(gè)具有挑戰(zhàn)性的重要任務(wù)是，找到減少或完成證明的相關(guān)前提。

除了原始碼庫(kù)和標(biāo)準(zhǔn)函式庫(kù)中有大量前提，Lean還有一個(gè)大型數(shù)學(xué)函式庫(kù)（Mathlib）。

然而，從所有函式庫(kù)中搜尋候選前提，極為困難且耗時(shí)耗力。

所以許多人試圖，能在Lean，或其他的證明助手中得到輔助，或自動(dòng)完成這一過(guò)程。

圖片

在Lean中，最先進(jìn)的前提選擇方法是，直接在Lean中實(shí)現(xiàn)的基於隨機(jī)森林（ random forest）的框架。

然而，前提選擇任務(wù)非常適合檢索增強(qiáng)型LLM，即在大模型訓(xùn)練期間訓(xùn)練檢索矩陣（前提嵌入），以估計(jì)證明目標(biāo)與候選前提之間的相關(guān)性。

給定推理時(shí)的證明目標(biāo)，首先將目標(biāo)編碼成一個(gè)向量，然後在前提嵌入和目標(biāo)向量之間執(zhí)行矩陣向量乘法。

然後，為了選擇前k個(gè)前提（其中k可以是超參數(shù)，決定使用者想要回傳多少前提），此時(shí)只要回傳得分最高的k個(gè)前提。

而要在Lean中執(zhí)行推理任務(wù)，除了Lean Copilot提供的快速推理外，還需要一個(gè)高效的矩陣乘法庫(kù)和一個(gè)C 的numpy矩陣閱讀器。

研究人員採(cǎi)用了來(lái)自CTranslate2的矩陣乘法函數(shù)，和來(lái)自L(fǎng)ibnpy的C 快速numpy檔案讀取器。

他們又透過(guò)FFI機(jī)制，將這些數(shù)字連結(jié)到Lean。

因此，前提選擇的策略可以非常有效率地運(yùn)行，因?yàn)榍疤崆度肟梢灶A(yù)先計(jì)算，所有後續(xù)操作都可以使用上文介紹的函式庫(kù)在C 中快速完成。

在獲得回傳的前提後，研究者進(jìn)一步以有用的信息對(duì)其進(jìn)行註解。

這裡將所有前提分為兩類(lèi)：可直接在當(dāng)前環(huán)境中使用的前提（範(fàn)圍內(nèi)前提）和不可直接在當(dāng)前環(huán)境中使用的前提（範(fàn)圍外前提）。

這取決於是否導(dǎo)入了所需的軟體包。

如果已經(jīng)導(dǎo)入了前提所需的套件，則可以輕鬆使用該前提。如下圖6顯示了附註解的範(fàn)圍內(nèi)前提。

圖7所示是註解的範(fàn)圍外前提。

下面舉個(gè)使用「前提選擇」的例子，對(duì)於圖3中的定理add_abc，可以直接在證明中輸入select_premises（圖8左）。

然後，相關(guān)前提的列表，就會(huì)出現(xiàn)在資訊視圖中（圖8右）。

對(duì)於這個(gè)簡(jiǎn)單的定理，可以清楚地看到所選的前提確實(shí)相關(guān)，因?yàn)樗鼈兌寂c自然數(shù)和加法規(guī)則有關(guān)。

在這種情況下，所選的4個(gè)前提都在目前範(fàn)圍內(nèi)，這表示它們的模組已經(jīng)導(dǎo)入。

如上，便是研究人員透過(guò)Lean Copilot建構(gòu)的三個(gè)實(shí)用的證明自動(dòng)化工具，用於策略建議、搜尋證明和前提選擇。

81.2%的證明步驟，全都自動(dòng)化了

透過(guò)Lean Copilot框架，研究人員憑經(jīng)驗(yàn)提出了假設(shè)－在Lean互動(dòng)定理證明（ITP）中進(jìn)行人機(jī)協(xié)作是有益的。

由於Lean中的定理證明過(guò)程，主要以策略證明為主。

因此，在具體實(shí)驗(yàn)中，作者主要評(píng)估了用於「策略建議」，以及「證明搜尋」的證明自動(dòng)化工具。

總而言之，aesop是當(dāng)前是一種用於證明搜索，最先進(jìn)的基於規(guī)則的證明自動(dòng)化工具。

研究人員在兩種情況下，驗(yàn)證了基於LLM的搜尋證明與aesop相比的有效性：

（1）自主證明定理（LLM獨(dú)立完成）

（2）協(xié)助人類(lèi)進(jìn)行定理證明（人類(lèi)與AI協(xié)作）

此外，研究者還將搜尋證明與策略建議進(jìn)行了比較，以證明除了單一策略建議之外，搜尋證明體現(xiàn)的優(yōu)勢(shì)。

研究Lean Copilot如何有效地幫助人類(lèi)進(jìn)行ITP的過(guò)程，類(lèi)似於人類(lèi)在軟體程式設(shè)計(jì)中使用Copilot的範(fàn)式。

也就是說(shuō)，當(dāng)我們面對(duì)一個(gè)目標(biāo)時(shí)，首先會(huì)呼叫Copilot，看其是否可以直接解決問(wèn)題。

如果不能，我們會(huì)進(jìn)一步簡(jiǎn)化目標(biāo)，然後再?lài)L試Copilot。然後，一直重複上述過(guò)程，直至Copilot成功解決剩餘目標(biāo)。

而研究人員是透過(guò)這樣的迭代協(xié)作範(fàn)例中，去查看每個(gè)證明自動(dòng)化工具可以自動(dòng)化多少人力。

具體結(jié)果，如下表1顯示。

證明搜尋（search_proof）可以自動(dòng)證明64%的定理（50個(gè)中的32個(gè)），明顯高於aesop和策略建議（suggest_tropics）。

當(dāng)用於輔助人類(lèi)時(shí)，證明搜尋只需要平均1.02個(gè)手動(dòng)輸入策略，這也比aesop（3.62）和策略建議（2.72）更好。

圖片

最後，對(duì)於每個(gè)測(cè)試的定理，作者計(jì)算了三個(gè)工具中每一個(gè)可以自動(dòng)化的證明步驟的百分比。

結(jié)果發(fā)現(xiàn)，證明搜尋可以自動(dòng)完成定理中約81.2%的證明步驟，明顯高於策略建議（48.6%）和aesop（35.2%）。

總之，證明搜尋的效能比策略建議，高出1.67倍，比基於規(guī)則的基線(xiàn)aesop高2.31倍。

透過(guò)Copilot在Lean中進(jìn)行本地LLM推理

Lean Copilot中的tactic建議、證明搜尋和前提選擇，這三個(gè)任務(wù)本質(zhì)上可能看起來(lái)不同，但對(duì)於使用者體驗(yàn)的要求是相似的。

它們都需要足夠快速地產(chǎn)生回應(yīng)，具有適中的運(yùn)算需求，同時(shí)在Lean中運(yùn)行。

使用者之所以有這些要求，是因?yàn)長(zhǎng)ean本身在大多數(shù)情況下都能非常快速地提供環(huán)境回饋（例如剩餘目標(biāo)，錯(cuò)誤訊息，類(lèi)型資訊等）。

這種快速，跟證明定理的本質(zhì)是一致的－它需要連貫的推理。

如果Lean Copilot需要使用者等待很長(zhǎng)一段時(shí)間，那麼人類(lèi)和AI之間的協(xié)作就很難發(fā)揮作用。

同樣，我們也非常希望滿(mǎn)足低運(yùn)算的需求。因?yàn)長(zhǎng)ean中的定理證明本身不需要GPU，可以在使用者本地的筆記型電腦上運(yùn)作。

因此，能夠在大多數(shù)硬體（包括沒(méi)有GPU的筆記型電腦）上高效運(yùn)行，對(duì)於Lean的用戶(hù)就非常重要。

因?yàn)槭褂谜咴诰帉?xiě)證明時(shí)，可能無(wú)法存取支援CUDA的GPU。

因?yàn)樾枰獫M(mǎn)足快速推理和低運(yùn)算需求，而且所有流行的高效深度學(xué)習(xí)框架都是在Python中，團(tuán)隊(duì)想到的一個(gè)自然的解決方案，就是在Python中託管模型(本地或遠(yuǎn)端)，然後從Lean向模型發(fā)出請(qǐng)求。

然而，這種方法會(huì)受到進(jìn)程間通訊的開(kāi)銷(xiāo)的影響，並且它需要使用者執(zhí)行額外的設(shè)定步驟，並不適合Lean的傳統(tǒng)工作流程。

為了克服這些問(wèn)題，Lean Copilot透過(guò)外部功能介面(FFI)在Lean中本地運(yùn)行LLM。

FFI是一種機(jī)制，可以用一種語(yǔ)言寫(xiě)的程式呼叫另一種語(yǔ)言的子程式。

Lean部分用c 實(shí)現(xiàn)，可以與c 高效互通。

程式設(shè)計(jì)師可以在Lean中宣告一個(gè)函數(shù)，但在c 中實(shí)作函數(shù)體。實(shí)作會(huì)被編譯到一個(gè)共享庫(kù)中，並動(dòng)態(tài)連結(jié)到Lean。

預(yù)設(shè)情況下，我們採(cǎi)用的是LeanDojo預(yù)訓(xùn)練的repver模型。它基於一個(gè)編碼器-解碼器轉(zhuǎn)換器，BVT5，它將輸入字串映射到輸出字串。

Lean Copilot透過(guò)將模型包裝成一個(gè)對(duì)字串操作的c 函數(shù)，使其在Lean中可運(yùn)行，該函數(shù)可以透過(guò)FFI在精益中呼叫。

圖片

華人作者立大功

最新論文中的三人團(tuán)隊(duì)，也是23年6月開(kāi)源平臺(tái)LeanDojo其中的作者。

圖片

論文網(wǎng)址：https://arxiv.org/pdf/2306.15626.pdf

#Peiyang Song（宋沛洋）

圖片

宋沛洋是加州大學(xué)聖塔芭芭拉分校創(chuàng)意研究學(xué)院（CCS）的電腦科學(xué)榮譽(yù)本科生，導(dǎo)師是Richert Wang和Phill Conrad 。

同時(shí)，他也是加州理工學(xué)院計(jì)算與數(shù)學(xué)科學(xué)系（CMS）的SURF研究員，由Anima Anandkumar教授和Kaiyu Yang博士共同指導(dǎo)。

圖片

另外，他也是UC伯克利建築實(shí)驗(yàn)室的研究員，與Tim Sherwood和Dr. Jeremy Lau（Google ）一起合作。

他的研究興趣是機(jī)器學(xué)習(xí)（ML），涉及自然語(yǔ)言處理（NLP）和電腦視覺(jué)（CV）等應(yīng)用領(lǐng)域，以及系統(tǒng)和程式語(yǔ)言（PL）等基礎(chǔ)理論。

宋沛洋最近的研究主要有兩個(gè)方向。

一是神經(jīng)符號(hào)推理和人工智慧數(shù)學(xué)（AI4Math），將大模型與互動(dòng)式定理證明器（ITPs）相結(jié)。

另一個(gè)是基於時(shí)序邏輯的高能效機(jī)器學(xué)習(xí)。

Kaiyu Yang（楊凱峪）

圖片

楊凱峪是加州理工學(xué)院計(jì)算數(shù)學(xué)科學(xué)（CMS）系的博士後研究員，指導(dǎo)教授是Anima Anandkumar。

他曾在普林斯頓大學(xué)獲得了博士學(xué)位，導(dǎo)師是Jia Deng，也曾與Olga Russakovsky、陳丹琦一起工作。

他的研究重點(diǎn)是神經(jīng)符號(hào)人工智慧，旨在使機(jī)器學(xué)習(xí)能夠進(jìn)行符號(hào)推理，希望透過(guò)兩個(gè)方向?qū)崿F(xiàn)：

（1）將機(jī)器學(xué)習(xí)應(yīng)用於符號(hào)推理任務(wù)，如形式邏輯或自然語(yǔ)言中的數(shù)學(xué)推理和定理證明；

（2）將符號(hào)組件引入機(jī)器學(xué)習(xí)模型，使其更具可解釋性、可驗(yàn)證性和數(shù)據(jù)高效。

目前，他正在研究能夠理解和推理數(shù)學(xué)的人工智慧。數(shù)學(xué)推理是人類(lèi)智慧的一個(gè)重要里程碑，它有可能改變科學(xué)和工程中的許多重要問(wèn)題，例如解決偏微分方程和公式驗(yàn)證。

Anima Anandkumar

Anima Anandkumar現(xiàn)在是加州理工學(xué)院計(jì)算和數(shù)學(xué)科學(xué)教授。

圖片

她的研究興趣主要集中在大規(guī)模機(jī)器學(xué)習(xí)、非凸優(yōu)化和高維度統(tǒng)計(jì)等領(lǐng)域。

特別是，她一直在帶頭開(kāi)發(fā)和分析機(jī)器學(xué)習(xí)的張量演算法。

張量分解方法具有極高的平行性和可擴(kuò)展性，可應(yīng)用於大量資料。它可以保證收斂到最優(yōu)解，並對(duì)許多機(jī)率模型（例如Markov模型）輸出一致的估計(jì)結(jié)果。

更廣泛地說(shuō)，Anandkumar教授一直在研究加速非凸優(yōu)化的高效技術(shù)。

參考資料：

http://ipnx.cn/link/1dd5a4016c624ef51f0542d4ae60e281

#http://ipnx.cn/link/ed798eec75807df6e79b0be391f720e4

#http://ipnx.cn/link /a652e914c736dfaf8a6667ae6936f0d6