編輯:編輯部
【新智元導讀】讓陶哲軒大神贊不絕口的形式化研究神器Lean,運行LLM的推理卻有個bug。最近,加州理工團隊解決了這個bug,把80%以上的數(shù)學證明步驟,都自動化了!
Lean Copilot,讓陶哲軒等眾多數(shù)學家贊不絕口的這個形式化數(shù)學工具,又有超強進化了?
就在剛剛,加州理工教授Anima Anandkumar宣布,團隊發(fā)布了Lean Copilot論文的擴展版本,并且更新了代碼庫。
論文地址:https://arxiv.org/pdf/2404.12534.pdf
最新實驗表明,這個Copilot工具,可以自動化80%以上的數(shù)學證明步驟了!這個紀錄,比以前的基線aesop還要好2.3倍。
并且,和以前一樣,它在MIT許可下是開源的。
而對此做出巨大貢獻的,是一位華人小哥宋沛洋,他是UCSB的榮譽CS本科生,加州理工學院計算 數(shù)學科學(CMS)系的SURF研究員。
網(wǎng)友驚呼:所以,陶哲軒現(xiàn)在的數(shù)學研究可以原地加速5倍了?
LLM提出證明策略,人類無縫干預
團隊就發(fā)布了這個Lean Copilot的工具,希望啟動人類和LLM的協(xié)作,編寫出100%準確的形式化數(shù)學證明。
它解決了一個核心技術(shù)挑戰(zhàn):在Lean中運行LLM的推理。
通過這個工具,我們就可以讓LLM在Lean中提出證明策略,允許人類以無縫的方式干預和修改。
之所以開發(fā)這個項目,是因為自動化定理證明在如今仍是一項艱巨的挑戰(zhàn)。
我們都知道,LLM在做數(shù)學和推理任務時,時常會犯錯誤、產(chǎn)生幻覺,十分不可靠。
因此,到目前為止,數(shù)學證明大多是手動推導的,需要仔細驗證。
像Lean這的定理證明工具,倒是可以形式化證明過程的每一步,但人類編寫起Lean,著實很費力。
在這種情況下,Lean Copilot的誕生就顯得意義重大。
讓陶哲軒多次震驚的神器:數(shù)學家還不會用就完蛋了
LLM可以作為輔助人類證明定理的工具,這一論點已經(jīng)被陶哲軒多次證實了。
他前腳剛在博客里預測,26年AI將和搜索、符號數(shù)學工具結(jié)合,成為數(shù)學研究中值得信賴的合著者。
緊接著,佐證他觀點的研究就如雨后春筍一般源源不斷地冒出來。
去年6月,加州理工、英偉達、MIT等機構(gòu)的學者,就構(gòu)建了一個基于開源LLM的定理證明器LeanDojo。
9月,微軟亞洲研究院、北大、北航等機構(gòu)的研究人員,通過97個回合的「蘇格拉底式」嚴格推理,成功讓GPT-4得出了「P≠NP」的結(jié)論,破解了這個千禧年難題。
在第97輪對話中,GPT-4得出結(jié)論,證明示例在沒有窮舉法的情況下無法求解,證明了結(jié)論為P≠NP
去年10月,陶哲軒在GPT-4、Copilot的幫助下,直接發(fā)現(xiàn)了自己論文中的一處隱藏bug。
在用Lean4形式化第6頁論點的過程中發(fā)現(xiàn),他發(fā)現(xiàn)表達式
在n=3,k=2時,實際上是發(fā)散的。
這個不太容易看出的bug能被及時捉住,多虧了Lean4。原因是,Lean要求他構(gòu)建0<n?3,但陶哲軒只假設了n>2。由此,Lean無法基于負的0<n?3得到反證。
這一發(fā)現(xiàn)直接讓陶哲軒瞳孔震驚。
而在去年年底,陶哲軒直接成功地用AI工具,完成了形式化多項式Freiman-Ruzsa猜想證明過程的工作。
最后,依賴關(guān)系圖已經(jīng)完全被綠色所覆蓋,Lean編譯器也報告說,這個猜想完全遵循標準公理。
在這個過程中,所有最前線的數(shù)學研究者,都在第一時間感受到了AI對于數(shù)學研究顛覆力量的直接沖擊。
Lean Coilot,讓Lean更好用
而今天,Lean Copilot的這項研究,讓Lean直接變得更強大了。
在這篇論文中,團隊基于Lean Copilot構(gòu)建了一些工具,用于建議證明步驟(策略建議)、完成中間證明目標(證明搜索)和使用LLM選擇相關(guān)前提(前提選擇)。
實驗結(jié)果也充分表明了,跟Lean中現(xiàn)有的基于規(guī)則的證明自動化相比,Lean Copilot在輔助人類自動化定理證明上,是有效的。
Lean Copilot提供了一個通用框架,可以通過CTranslate 2在本地,或者在服務器上運行LLM的推理。
通過這個框架,用戶就能創(chuàng)建各種自動化證明工具。
Lean是一個在數(shù)學家中很受歡迎的證明助手。如下圖所示,Lean中的一個證明,是由一系列被稱為策略(Tactics)的證明步驟組成。
從整個定理開始作為初始目標,策略反復地將當前的目標轉(zhuǎn)化為更簡單的子目標,直到所有目標都被解決。
用戶在由VSCode驅(qū)動的IDE中交互編寫策略,在右邊的infoview面板中顯示目標。
生成策略建議
利用Lean Copilot,團隊構(gòu)建出了suggest_tropics,一種用LLM生成策略建議的工具。
而它本身,也是一種策略。
應用時,它將當前目標輸入LLM,并且從LLM獲取生成的策略候列表。
它會查看每個選項,看它們是否會 1)導致錯誤;2)結(jié)果沒有錯,但不能完成證明;3)順利完成證明。
如果是1),這個策略就會被刪除。
只有無錯誤的策略,才會顯示在右邊的視圖面板中。
其中,成功完成證明的策略,使用綠色標記(類別3);沒有錯誤改變證明目標,但未完成證明的策略,使用藍色標記(類別2)。
注意!當所有列出的策略都屬于類別2時,這個信息對于用戶來說,可能極有價值。
在這種情況下,剩余目標的信息,可以直接幫助用戶選擇策略,作為下一個中間證明步驟。
看到建議后,用戶可以選擇是否接受,或使用它們作為靈感來源,制定新策略。
比如,我們在Lean代碼中定義了一個定理add_abc,它的初始目標如圖3右所示。
當我們輸入suggest_tropics時,會在右邊看到策略建議。
第一個策略顯示為綠色,表示證明已成功完成。
接下來三個建議均為藍色,這就表明無法直接完成證明,但不會導致錯誤。
因而,它們很有可能是有效的中間證明步驟!
同時,剩余子目標也顯示了出來。
而Tactic state字段顯示No goal,是因為至少有一個策略建議可以被證明。
搜索完整證明
此外,因為人類和機器都不能始終如一地產(chǎn)生正確的策略,因此在這個過程中必須回溯、探索不同的替代方案,這個過程就是證明搜索。
當是上面所說的Suggest_tropics,僅能生成當前步驟的策略,不具備搜索多策略證明的能力。
為此,團隊將其與基于規(guī)則的證明搜索工具aesop結(jié)合起來,構(gòu)建了一個基于LLM的證明搜索工具。
Aesop會將最佳優(yōu)先搜索作為Lean的策略實施,并且允許用戶配置搜索樹的擴展方式。
搜索樹是由作為節(jié)點的目標組成。
起初,它只有原始目標作為根節(jié)點。在每一步中,aesop都會選擇最有希望的未擴展節(jié)點,通過應用策略對其擴展,將生成的節(jié)點添加為子節(jié)點。
而當aesop找到一條從根源到可輕松解決的目標的路徑,就證明搜索成功了!
因此,aesop的性能關(guān)鍵取決于用戶是否配置了有效的規(guī)則集。
這就可以看出,aesop缺乏靈活性。因此,Search_proof通過在每一步中由suggest_tropics生成的目標相關(guān)策略,來增強aesop的規(guī)則集,讓它變得更加靈活。
對于圖3中的原始目標,用戶只需輸入search_prrof,找到可以解決目標的完整證明,就顯示在了信息視圖中(圖5右)。
可以看到,由于發(fā)現(xiàn)了成功的證據(jù),所以剩余的Tactic state是No goals。
選擇注釋好的前提
此外,定理證明中另一項具有挑戰(zhàn)性的重要任務是,找到減少或完成證明的相關(guān)前提。
除了源碼庫和標準庫中有大量前提,Lean還有一個大型數(shù)學庫(MathLib)。
然而,從所有庫中搜索候選前提,極其困難且耗時耗力。
所以許多人都試圖,能在Lean,或其他的證明助手中得到輔助,或自動完成這一過程。
在Lean中,最先進的前提選擇方法是,直接在Lean中實現(xiàn)的基于隨機森林(random forest)的框架。
然而,前提選擇任務非常適合檢索增強型LLM,即在大模型訓練期間訓練檢索矩陣(前提嵌入),以估計證明目標與候選前提之間的相關(guān)性。
給定推理時的證明目標,首先將目標編碼成一個向量,然后在前提嵌入和目標向量之間執(zhí)行矩陣向量乘法。
然后,為了選擇前k個前提(其中k可以是一個超參數(shù),決定用戶想要返回多少個前提),這時只需返回得分最高的k個前提。
而要在Lean中執(zhí)行推理任務,除了Lean Copilot提供的快速推理外,還需要一個高效的矩陣乘法庫和一個C 的numpy矩陣閱讀器。
研究人員采用了來自CTranslate2的矩陣乘法函數(shù),和來自Libnpy的C 快速numpy文件閱讀器。
他們再次通過FFI機制,將這些數(shù)鏈接到Lean。
因此,前提選擇的策略可以非常高效地運行,因為前提嵌入可以預先計算,所有后續(xù)操作都可以使用上文介紹的庫在C 中快速完成。
在獲得返回的前提后,研究者進一步用有用的信息對其進行注釋。
這里將所有前提所分為兩類:可直接在當前環(huán)境中使用的前提(范圍內(nèi)前提)和不可直接在當前環(huán)境中使用的前提(范圍外前提)。
這取決于是否導入了所需的軟件包。
如果已經(jīng)導入了前提所需的包,則可以輕松使用該前提。如下圖6顯示了帶注釋的范圍內(nèi)前提。
圖7所示是帶注釋的范圍外前提。
下面舉個使用「前提選擇」的例子,對于圖3中的定理add_abc,可以直接在證明中輸入select_premises(圖8左)。
然后,相關(guān)前提的列表,就會出現(xiàn)在信息視圖中(圖8右)。
對于這個簡單的定理,可以清晰看到所選的前提確實相關(guān),因為它們都與自然數(shù)和加法規(guī)則有關(guān)。
在這種情況下,所選的4個前提都在當前范圍內(nèi),這意味著它們的模塊已經(jīng)導入。
如上,便是研究人員通過Lean Copilot構(gòu)建的三個實用的證明自動化工具,用于策略建議、搜索證明和前提選擇。
81.2%的證明步驟,全都自動化了
通過Lean Copilot框架,研究人員憑經(jīng)驗提出了假設——在Lean交互式定理證明(ITP)中進行人機協(xié)作是有益的。
由于Lean中的定理證明過程,主要以策略證明為主。
因此,在具體實驗中,作者主要評估了用于「策略建議」,以及「證明搜索」的證明自動化工具。
總而言之,aesop是當前是一種用于證明搜索,最先進的基于規(guī)則的證明自動化工具。
研究人員在兩種情況下,驗證了基于LLM的搜索證明與aesop相比的有效性:
(1)自主證明定理(LLM獨立完成)
(2)協(xié)助人類進行定理證明(人類與AI協(xié)作)
此外,研究者還將搜索證明與策略建議進行了比較,以證明除了單一策略建議之外,搜索證明體現(xiàn)的優(yōu)勢。
研究Lean Copilot如何有效地幫助人類進行ITP的過程,類似于人類在軟件編程中使用Copilot的范式。
也就是說,當我們面對一個目標時,首先會調(diào)用Copilot,看其是否可以直接解決問題。
如果不能,我們會進一步簡化目標,然后再次嘗試Copilot。然后,一直重復上述過程,直至Copilot成功解決剩余目標。
而研究人員便是通過這樣的迭代協(xié)作范例中,去查看每個證明自動化工具可以自動化多少人力。
具體結(jié)果,如下表1顯示。
證明搜索(search_proof)可以自動證明64%的定理(50個中的32個),明顯高于aesop和策略建議(suggest_tropics)。
當用于輔助人類時, 證明搜索僅需要平均1.02個手動輸入策略,這也比aesop(3.62)和策略建議(2.72)更好。
最后,對于每個測試的定理,作者計算了三個工具中每一個可以自動化的證明步驟的百分比。
結(jié)果發(fā)現(xiàn),證明搜索可以自動完成定理中約81.2%的證明步驟,明顯高于策略建議(48.6%)和aesop(35.2%)。
總之,證明搜索的性能比策略建議,要高出1.67倍,比基于規(guī)則的基線aesop高2.31倍。
通過Copilot在Lean中進行本地LLM推理
Lean Copilot中的tactic建議、證明搜索和前提選擇,這三個任務在本質(zhì)上可能看起來不同,但對于用戶體驗的要求是相似的。
它們都需要足夠快速地生成響應,具有適中的計算需求,同時在Lean中運行。
用戶之所以有這些要求,是因為Lean本身在大多數(shù)情況下都能非??焖俚靥峁┉h(huán)境反饋(比如剩余目標,錯誤信息,類型信息等)。
這種快速,跟證明定理的本質(zhì)是一致的——它需要連貫的推理。
如果Lean Copilot需要用戶等待很長一段時間,那么人類和AI之間的協(xié)作就很難發(fā)揮作用。
同樣,我們也非常希望滿足低計算的需求。因為Lean中的定理證明本身不需要GPU,可以在用戶本地的筆記本電腦上運行。
因此,能夠在大多數(shù)硬件(包括沒有GPU的筆記本電腦)上高效運行,對于Lean的用戶就非常重要。
因為用戶在編寫證明時,可能無法訪問支持CUDA的GPU。
因為需要滿足快速推理和低計算需求,而且所有流行的高效深度學習框架都是在Python中,團隊想到的一個自然的解決方案,就是在Python中托管模型(本地或遠程),然后從Lean向模型發(fā)出請求。
然而,這種方法會受到進程間通信的開銷的影響,并且它需要用戶執(zhí)行額外的設置步驟,并不適合Lean的傳統(tǒng)工作流程。
為了克服這些問題,Lean Copilot通過外部功能接口(FFI)在Lean中本地運行LLM。
FFI是一種機制,可以用一種語言編寫的程序調(diào)用另一種語言的子程序。
Lean部分用c 實現(xiàn),可以與c 高效互操作。
程序員可以在Lean中聲明一個函數(shù),但在c 中實現(xiàn)函數(shù)體。實現(xiàn)會被編譯到一個共享庫中,并動態(tài)鏈接到Lean。
默認情況下,我們采用的是LeanDojo預訓練的repver模型。它基于一個編碼器-解碼器轉(zhuǎn)換器,BVT5,它將輸入字符串映射到輸出字符串。
Lean Copilot通過將模型包裝成一個對字符串操作的c 函數(shù),使其在Lean中可運行,該函數(shù)可以通過FFI在精益中調(diào)用。
華人作者立大功
最新論文中的三人團隊,也是23年6月開源平臺LeanDojo其中的作者。
論文地址:https://arxiv.org/pdf/2306.15626.pdf
Peiyang Song(宋沛洋)
宋沛洋是加州大學圣巴巴拉分校創(chuàng)意研究學院(CCS)的計算機科學榮譽本科生,導師是Richert Wang和Phill Conrad 。
與此同時,他還是加州理工學院計算與數(shù)學科學系(CMS)的SURF研究員,由Anima Anandkumar教授和Kaiyu Yang博士共同指導。
另外,他還是UC伯克利建筑實驗室的研究員,與Tim Sherwood和Dr. Jeremy Lau(谷歌)一起合作。
他的研究興趣是機器學習(ML),涉及自然語言處理(NLP)和計算機視覺(CV)等應用領域,以及系統(tǒng)和編程語言(PL)等基礎理論。
宋沛洋最近的研究主要有兩個方向。
一是神經(jīng)符號推理和人工智能數(shù)學(AI4Math),將大模型與交互式定理證明器(ITPs)相結(jié)。
另一個是基于時序邏輯的高能效機器學習。
Kaiyu Yang(楊凱峪)
楊凱峪是加州理工學院計算 數(shù)學科學(CMS)系的博士后研究員,導師是Anima Anandkumar。
他曾在普林斯頓大學獲得了博士學位,導師是Jia Deng,還曾與Olga Russakovsky、陳丹琦一起工作。
他的研究重點是神經(jīng)符號人工智能,旨在使機器學習能夠進行符號推理,希望通過兩個方向?qū)崿F(xiàn):
(1)將機器學習應用于符號推理任務,如形式邏輯或自然語言中的數(shù)學推理和定理證明;
(2)將符號組件引入機器學習模型,使其更具可解釋性、可驗證性和數(shù)據(jù)高效。
目前,他正在研究能夠理解和推理數(shù)學的人工智能。數(shù)學推理是人類智能的一個重要里程碑,它有可能改變科學和工程中的許多重要問題,比如解決偏微分方程和公式驗證。
Anima Anandkumar
Anima Anandkumar現(xiàn)在是加州理工學院計算和數(shù)學科學教授。
她的研究興趣主要集中在大規(guī)模機器學習、非凸優(yōu)化和高維統(tǒng)計等領域。
特別是,她一直在帶頭開發(fā)和分析機器學習的張量算法。
張量分解方法具有極高的并行性和可擴展性,可應用于海量數(shù)據(jù)。它可以保證收斂到最優(yōu)解,并對許多概率模型(比如Markov模型)輸出一致的估計結(jié)果。
更廣泛地說,Anandkumar教授一直在研究加速非凸優(yōu)化的高效技術(shù)。
參考資料:
https://arxiv.org/abs/2404.12534
https://github.com/lean-dojo/LeanCopilot
https://twitter.com/AnimaAnandkumar/status/1782518528098353535
版權(quán)聲明:本文內(nèi)容由互聯(lián)網(wǎng)用戶自發(fā)貢獻,該文觀點僅代表作者本人。本站僅提供信息存儲空間服務,不擁有所有權(quán),不承擔相關(guān)法律責任。如發(fā)現(xiàn)本站有涉嫌抄襲侵權(quán)/違法違規(guī)的內(nèi)容, 請發(fā)送郵件至 舉報,一經(jīng)查實,本站將立刻刪除。