【ITBEAR科技資訊】4月23日消息，近日，加州理工教授Anima Anandkumar宣布，其團隊已經(jīng)發(fā)布了Lean Copilot論文的擴展版本，并對代碼庫進行了更新。該論文中介紹的Copilot工具，現(xiàn)在能夠自動化完成80%以上的數(shù)學證明步驟，這一成績較之前的基線aesop提升了2.3倍。該工具在MIT許可下保持開源。
這一重大進展的背后，是一位華人小哥宋沛洋的杰出貢獻。他是UCSB的榮譽CS本科生，同時也是加州理工學院計算+數(shù)學科學(CMS)系的SURF研究員。網(wǎng)友們對此紛紛表示贊嘆，甚至有人戲言，陶哲軒現(xiàn)在的數(shù)學研究可以原地加速5倍了。
Lean Copilot工具的推出，旨在啟動人類和大型語言模型(LLM)的協(xié)作，以編寫出100%準確的形式化數(shù)學證明。該工具解決了一個核心技術挑戰(zhàn)，即在Lean中運行LLM的推理。通過這一工具，LLM可以在Lean中提出證明策略，同時允許人類以無縫的方式進行干預和修改。
形式化數(shù)學證明自動化一直是一項艱巨的挑戰(zhàn)。盡管LLM在處理數(shù)學和推理任務時表現(xiàn)出色，但它們也時常會犯錯誤，產(chǎn)生不準確的結(jié)果。因此，數(shù)學證明大多仍需要手動推導和仔細驗證。而Lean等定理證明工具，雖然可以形式化證明過程的每一步，但人類編寫Lean代碼卻相當費力。在這種背景下，Lean Copilot的誕生顯得尤為重要。
此前，陶哲軒等多位數(shù)學家已經(jīng)多次證實了LLM可以作為輔助人類證明定理的有效工具。而此次Lean Copilot的更新，無疑讓這一觀點得到了進一步的印證。該工具不僅提高了數(shù)學證明的自動化程度，還為數(shù)學家們提供了一個更為高效、靈活的研究環(huán)境。
據(jù)ITBEAR科技資訊了解，Lean Copilot的構建基于一些創(chuàng)新性的工具，如策略建議、證明搜索和前提選擇等。這些工具通過LLM生成策略建議，完成中間證明目標，并選擇相關前提，從而大大提高了數(shù)學證明的效率和準確性。此外，該工具還提供了一個通用框架，使得用戶能夠創(chuàng)建各種自動化證明工具，進一步推動了數(shù)學研究的進步。
