“DeepSeek許多重要?jiǎng)?chuàng)新出自實(shí)習(xí)生之手?！?/span>
這是前段時(shí)間社交網(wǎng)絡(luò)上盛傳的信息，不過(guò)這條信息并不夸張，因?yàn)樾寥A劍就是在DeepSeek實(shí)習(xí)期間主導(dǎo)開(kāi)發(fā)了專注于數(shù)學(xué)證明DeepSeek-Prover系列模型，他也是DeepSeek-Prover-V1.5論文的一作。
辛華劍本科畢業(yè)于中山大學(xué)邏輯學(xué)專業(yè)，現(xiàn)在是愛(ài)丁堡大學(xué)人工智能方向的一年級(jí)博士生，專注于大模型在數(shù)學(xué)定理證明中的創(chuàng)新應(yīng)用。
去年8月發(fā)布的DeepSeek-Prover-V1.5可以被看作是DeepSeek在數(shù)學(xué)證明領(lǐng)域的早期探索和技術(shù)積累，推動(dòng)了大模型更好地解決形式化定理證明問(wèn)題，當(dāng)時(shí)被稱為是“最強(qiáng)形式化推理模型”。
在大模型中，非形式化推理是其理解和生成自然語(yǔ)言、進(jìn)行常識(shí)推理的基礎(chǔ)，就像是人類(lèi)平時(shí)聊天或思考問(wèn)題時(shí)的自然方式；而形式化推理則賦予大模型在特定領(lǐng)域（如數(shù)學(xué)、代碼）進(jìn)行精確、嚴(yán)謹(jǐn)推理的能力，它有嚴(yán)格的規(guī)則和格式，每一步推理都必須符合邏輯規(guī)則，不能隨意跳步或省略。
“DeepSeek-Prover在DeepSeek算是一個(gè)比較獨(dú)立的探索性項(xiàng)目，它的初衷是探索通過(guò)形式化系統(tǒng)更好地構(gòu)造自然語(yǔ)言的嚴(yán)格推理數(shù)據(jù)?！毙寥A劍告訴「甲子光年」。
隨著AI推理能力的提升，使用AI來(lái)證明數(shù)學(xué)問(wèn)題已經(jīng)成為一個(gè)重要的研究探索方向，形式化數(shù)學(xué)也成為了討論熱點(diǎn)。
形式化數(shù)學(xué)是指使用嚴(yán)格的數(shù)學(xué)語(yǔ)言和邏輯系統(tǒng)來(lái)描述和推理數(shù)學(xué)概念、定理和證明的過(guò)程。著名數(shù)學(xué)家陶哲軒就認(rèn)為，形式化數(shù)學(xué)和AI的結(jié)合將使數(shù)學(xué)研究更加高效、協(xié)作和規(guī)模化。他樂(lè)觀地預(yù)測(cè)，未來(lái)數(shù)學(xué)家可以在AI的輔助下，一次性證明數(shù)百或數(shù)千條定理。
英國(guó)當(dāng)?shù)貢r(shí)間2月14日下午，在UKTI.HUB（英倫科創(chuàng)）舉辦的活動(dòng)上，辛華劍發(fā)表了一場(chǎng)題為《大語(yǔ)言模型時(shí)代的形式化數(shù)學(xué)革命》的演講并回答了「甲子光年」和現(xiàn)場(chǎng)觀眾的提問(wèn)。倫敦大學(xué)學(xué)院（UCL）里的一間教室，涌入了180多名觀眾。
1.形式化數(shù)學(xué)的歷史淵源
大家好，我是辛華劍。
今天我將和大家分享一些關(guān)于形式化數(shù)學(xué)的背景知識(shí)，以及探討如何利用大語(yǔ)言模型在數(shù)學(xué)推理中應(yīng)用形式化方法，并展望其可能帶來(lái)的未來(lái)影響。
需要強(qiáng)調(diào)的是，接下來(lái)我所分享的內(nèi)容，純屬個(gè)人觀點(diǎn)，不代表任何組織機(jī)構(gòu)的立場(chǎng)。
首先，什么是形式化數(shù)學(xué)？
或許對(duì)大家來(lái)說(shuō)，這并不是一個(gè)非常熟悉的概念。簡(jiǎn)單來(lái)說(shuō)，形式化數(shù)學(xué)強(qiáng)調(diào)使用精確的符號(hào)語(yǔ)言來(lái)表達(dá)數(shù)學(xué)陳述和證明，其所有的定理及其證明都必須從一些確定的公理出發(fā)，并遵循明確的、可以被機(jī)器驗(yàn)證的邏輯規(guī)則。
事實(shí)上，形式化數(shù)學(xué)并非一個(gè)全新的概念，它有著悠久的歷史。
早在萊布尼茨時(shí)期，他就提出了“普遍語(yǔ)法”的概念，希望人類(lèi)所有的思想都可以通過(guò)計(jì)算來(lái)判斷真假。比如說(shuō)當(dāng)兩人發(fā)生爭(zhēng)執(zhí)時(shí)，只要坐下來(lái)計(jì)算一下，就能得出誰(shuí)對(duì)誰(shuí)錯(cuò)的結(jié)論。他希望用代數(shù)符號(hào)的方法來(lái)刻畫(huà)這種操作，這實(shí)際上可以看作是現(xiàn)代邏輯學(xué)的肇始。
時(shí)間來(lái)到希爾伯特時(shí)代，形式化數(shù)學(xué)作為一項(xiàng)研究計(jì)劃已經(jīng)基本成熟。在他的時(shí)代，我們?nèi)绾芜M(jìn)行形式化數(shù)學(xué)呢？首先，我們需要挑選公理系統(tǒng)，并驗(yàn)證其一致性、相互獨(dú)立性和邏輯完備性。此外，還需要考慮一個(gè)關(guān)鍵問(wèn)題：是否存在一種能行的方法，能夠在一個(gè)理論中判定一個(gè)問(wèn)題的答案？雖然哥德?tīng)?、丘奇和圖靈的工作已經(jīng)否定了這種可能性，但數(shù)學(xué)的機(jī)械化或自動(dòng)化仍在不斷發(fā)展。
從20世紀(jì)30年代開(kāi)始，布爾巴基學(xué)派強(qiáng)調(diào)使用公理化的方式來(lái)重構(gòu)整個(gè)數(shù)學(xué)體系。他們認(rèn)為，人類(lèi)數(shù)學(xué)家并非無(wú)所不能。當(dāng)他們對(duì)某些數(shù)學(xué)文本的正確性產(chǎn)生質(zhì)疑時(shí)，他們?cè)V諸于將它們進(jìn)行形式化的一種可能性，直到他們認(rèn)為這種可能性只是一種練習(xí)，不需要額外的思考，他們就會(huì)停止這樣形式化的過(guò)程。
這也就是說(shuō)，形式化是他們保證數(shù)學(xué)正確性的一個(gè)根本策略。
進(jìn)入計(jì)算機(jī)和人工智能時(shí)代，麥卡錫提出了使用計(jì)算機(jī)來(lái)書(shū)寫(xiě)和檢查證明，他認(rèn)為這樣的證明可能會(huì)比數(shù)學(xué)家給出的更短。這是因?yàn)樵S多具體細(xì)節(jié)可以由計(jì)算機(jī)來(lái)代替人類(lèi)進(jìn)行驗(yàn)證，可以被很好地封裝起來(lái)，不暴露給數(shù)學(xué)家。數(shù)學(xué)家只需要關(guān)注證明的主要內(nèi)容和數(shù)學(xué)思想，一些邊界條件之類(lèi)的檢查，就可以完全交給計(jì)算機(jī)來(lái)處理。
2.當(dāng)代數(shù)學(xué)的工程化挑戰(zhàn)
雖然形式化數(shù)學(xué)擁有好的歷史淵源，為什么它至今仍未被數(shù)學(xué)界廣泛采納？以及，為什么我們認(rèn)為它將引發(fā)一場(chǎng)革命？
我們認(rèn)為，當(dāng)代數(shù)學(xué)面臨著一種工程化的挑戰(zhàn)。
我們觀察到，現(xiàn)代數(shù)學(xué)證明的篇幅已經(jīng)變得極其龐大，動(dòng)輒數(shù)百頁(yè)甚至上千頁(yè)。要掌握如此龐大的證明篇幅規(guī)模，并通過(guò)同行評(píng)審進(jìn)行驗(yàn)證，需要耗費(fèi)巨大的人力成本。
舉個(gè)例子，即使人類(lèi)專家花費(fèi)數(shù)年時(shí)間共同驗(yàn)證一個(gè)大型證明，仍然有可能出現(xiàn)錯(cuò)誤。例如，四色定理的早期證明最初被接受，但后來(lái)卻被發(fā)現(xiàn)存在問(wèn)題。
此外，知識(shí)管理也是一個(gè)關(guān)鍵問(wèn)題。
隨著數(shù)學(xué)的不斷發(fā)展，無(wú)論是在學(xué)科分支的數(shù)量上，還是在每個(gè)學(xué)科的深度上，都已經(jīng)遠(yuǎn)遠(yuǎn)超出了一個(gè)人類(lèi)專家能夠掌握的范圍。
我們會(huì)說(shuō)亨利·龐加萊是最后一位全才數(shù)學(xué)家，現(xiàn)在已經(jīng)沒(méi)有人能夠掌握所有數(shù)學(xué)分支的最新進(jìn)展。數(shù)學(xué)家之間在工作上呈現(xiàn)相對(duì)分散的狀態(tài)，這對(duì)于數(shù)學(xué)的可持續(xù)發(fā)展來(lái)說(shuō)并不是一件好事。
一個(gè)典型的例子是，2003年，黑爾斯提出了關(guān)于開(kāi)普勒猜想的一個(gè)長(zhǎng)達(dá)300頁(yè)的證明。《數(shù)學(xué)年鑒》（Annals of Mathematics）組織的12人小組花了四年時(shí)間，也沒(méi)有對(duì)其正確性做出十足的判斷。最終，黑爾斯組織21個(gè)人的團(tuán)隊(duì)花了12年時(shí)間，將這個(gè)龐大的數(shù)學(xué)證明利用Isabelle和HOL Light（證明助手軟件，能夠保證了證明之于“數(shù)學(xué)公理”與“邏輯規(guī)則”是正確的）上進(jìn)行了形式化，才最終驗(yàn)證了其正確性。
事實(shí)上，黑爾斯在他的原文中提出要做這件事的目的，并不僅僅是為了打消這12人的疑慮。他認(rèn)為，對(duì)于數(shù)學(xué)的長(zhǎng)期發(fā)展而言，形式化方法是一個(gè)根本的解決方案。
時(shí)間來(lái)到2024年，陶哲軒也正在推進(jìn)關(guān)于形式化數(shù)學(xué)方向的研究。
有采訪者問(wèn)陶哲軒：“為什么形式化數(shù)學(xué)使得數(shù)學(xué)家互相之間對(duì)工作結(jié)果的信任有了改變？”陶哲軒說(shuō)，形式化數(shù)學(xué)最好的一個(gè)特性是，它能夠?qū)⒁粋€(gè)大的問(wèn)題分解成相互獨(dú)立的很多方面，大家只要根據(jù)自己所專長(zhǎng)的方面來(lái)提交自己的證明代碼，而證明代碼的正確性驗(yàn)證是由證明助手以計(jì)算機(jī)程序執(zhí)行的方式來(lái)徹底完成的。也就是說(shuō)，數(shù)學(xué)家不需要逐行檢查別人的證明是否真的完全正確，才愿意相信他的工作成果。
因此，他認(rèn)為這種工作方式是一種更加可以擴(kuò)展到大規(guī)模的數(shù)學(xué)工作方式。他在對(duì)PFR假設(shè)的證明進(jìn)行形式化的項(xiàng)目中，與超過(guò)20人的團(tuán)隊(duì)來(lái)協(xié)作完成，這已經(jīng)比他通常合作的規(guī)模要大一些。他認(rèn)為，隨著大家對(duì)這套計(jì)算機(jī)輔助證明系統(tǒng)的了解，以及對(duì)這種形式化數(shù)學(xué)的工作方式的了解，實(shí)際上可以推廣到更大的規(guī)模。也就是說(shuō)，我們可以像軟件工程大規(guī)模開(kāi)發(fā)一樣來(lái)做數(shù)學(xué)，他認(rèn)為這是一種非?，F(xiàn)代化的方式。
另一方面，愛(ài)丁堡大學(xué)信息學(xué)院的教授Alan Bundy總結(jié)道，隨著數(shù)學(xué)的規(guī)模越來(lái)越大，我們面臨一個(gè)二難推理：要么我們必須放棄所有這種大定理，要么我們必須訴諸于計(jì)算機(jī)的輔助來(lái)進(jìn)行證明。
3.形式化數(shù)學(xué)作為一種解決方案
那么，形式化數(shù)學(xué)作為一種解決方案，是怎樣被實(shí)現(xiàn)的？
這里舉一些具體的例子。
現(xiàn)在流行的智能助手語(yǔ)言大概有四種，例如Coq、Lean、Isabelle和Mizar。
以Isabelle為例，我們?nèi)绾卧贗sabelle中進(jìn)行形式化證明？一個(gè)非常具體的例子，也是在Wikipedia上提供的演示例子：如何證明√2不是一個(gè)有理數(shù)？
我們會(huì)發(fā)現(xiàn)，這個(gè)在Isabelle中進(jìn)行的證明在思路上與人類(lèi)的證明是一致的，它也利用反證法，也逐漸推出一些中間結(jié)論，并利用這些中間結(jié)論逐步推導(dǎo)出矛盾。
最關(guān)鍵的是，我們不僅僅要在一個(gè)定理的證明內(nèi)部進(jìn)行工作，我們實(shí)際上操作的是一個(gè)非常大的數(shù)學(xué)理論。這個(gè)龐大的理論涉及到非常多的定義、引理和定理，我們?nèi)绾喂芾硭鼈冎g的相互關(guān)系？
陶哲軒在他的PFR項(xiàng)目中已經(jīng)演示了Lean blueprints帶來(lái)的工作方式變化。其中，綠色的點(diǎn)是已經(jīng)完成證明的部分，藍(lán)色的點(diǎn)是正在嘗試進(jìn)行證明中的定理，白色的點(diǎn)表示還沒(méi)有被編寫(xiě)的部分。而圖上的點(diǎn)之間的連線描述了這些定義和定理之間的依賴關(guān)系，也可以幫助更好地理解和分析整個(gè)項(xiàng)目。
當(dāng)這個(gè)blueprint中所有的點(diǎn)都變成了綠色的時(shí)候，我們就可以確鑿無(wú)疑地判斷這個(gè)整套數(shù)學(xué)理論已經(jīng)完成證明了。
但是，為什么現(xiàn)在大家在學(xué)校里仍然使用自然語(yǔ)言來(lái)學(xué)習(xí)和研究呢？這是因?yàn)橛泻芏嗟淖璧K，使得我們還沒(méi)有采用形式化的方法。
一方面是文化上的阻礙。數(shù)學(xué)工作者仍然更習(xí)慣于使用紙筆來(lái)進(jìn)行更靈活的推導(dǎo)，而形式化數(shù)學(xué)往往只被認(rèn)為是工程化的輔助技巧，而不是在數(shù)學(xué)思想上有啟發(fā)的技術(shù)。
另一方面，形式化數(shù)學(xué)的學(xué)習(xí)曲線非常陡峭。它有非常復(fù)雜的程序語(yǔ)法和語(yǔ)義，需要使用者同時(shí)了解數(shù)學(xué)思想、以類(lèi)型論或集合論進(jìn)行形式化的邏輯方法，以及編寫(xiě)程序語(yǔ)言的技術(shù)。
結(jié)果就是，同樣一個(gè)證明，在形式化系統(tǒng)里面做和用自然語(yǔ)言做相比，很多時(shí)候要多花十倍甚至二十倍的人工成本，這其中包括要額外證明很多在直觀上非常直接的、但嚴(yán)格證明非?，嵥榈囊?。
其他的因素還包括，可能你在Mathematica里面可以順利地算出一個(gè)很復(fù)雜的積分，但要使這樣的積分結(jié)果被Lean這樣的嚴(yán)格證明系統(tǒng)接受，目前仍然缺乏自動(dòng)化的銜接機(jī)制。
4.大語(yǔ)言模型在形式化數(shù)學(xué)的應(yīng)用
接下來(lái)，我想和大家探討一下大語(yǔ)言模型（LLM）在形式化數(shù)學(xué)領(lǐng)域的發(fā)展。我將從以下幾個(gè)方面展開(kāi)：
首先，我們可以考慮GPQA Diamond，這是一個(gè)衡量PhD水平科學(xué)問(wèn)題的榜單。我們可以看到，從2023年到2025年，大語(yǔ)言模型在解決這些問(wèn)題上的能力有了顯著提升。特別是OpenAI的o1、o3和DeepSeek-R1等模型，其水平已經(jīng)略高于人類(lèi)專家的水平。
這意味著，我們距離實(shí)現(xiàn)通用人工智能（AGI）可能已經(jīng)并沒(méi)有想象中那么遙遠(yuǎn)。
另外，OpenAI 前不久發(fā)布的一份報(bào)告顯示，目前最先進(jìn)的大語(yǔ)言模型在算法競(jìng)賽上的表現(xiàn)也十分驚艷。在codeforces編程競(jìng)賽平臺(tái)上，o1模型最高能達(dá)到98%甚至更高的分位數(shù)，這意味著它已經(jīng)位于前2%的水平。在2024年國(guó)際奧林匹克數(shù)學(xué)競(jìng)賽（IOI）上，他們的模型能達(dá)到362分，這已經(jīng)達(dá)到了人類(lèi)金牌選手的水平。
在數(shù)學(xué)方面，DeepMind去年7月份發(fā)布的形式化數(shù)學(xué)定理證明模型AlphaProof也取得了重要進(jìn)展。和我們的做法一樣，該模型也不是在自然語(yǔ)言上進(jìn)行訓(xùn)練和測(cè)試，而是在形式化證明系統(tǒng)Lean中進(jìn)行的。它與專注幾何的模型AlphaGeometry2一道，在2024年的國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）中獲得了28分的成績(jī)，距離金牌水平僅差1分。
那么，這些看起來(lái)像是奇跡的模型是如何訓(xùn)練出來(lái)的呢？其背后的訓(xùn)練機(jī)制是怎樣的呢？
以AlphaProof為例，它的訓(xùn)練流程大致分為兩部分。第一部分先收集 100 萬(wàn)道人類(lèi)數(shù)學(xué)問(wèn)題，這些問(wèn)題以自然語(yǔ)言描述，再使用神經(jīng)網(wǎng)絡(luò)將其翻譯成一億道形式化數(shù)學(xué)問(wèn)題。
然后，我們?cè)诖嘶A(chǔ)上訓(xùn)練解題神經(jīng)網(wǎng)絡(luò)。該網(wǎng)絡(luò)采用了類(lèi)似于AlphaGo的強(qiáng)化學(xué)習(xí)方法，不斷地嘗試對(duì)數(shù)學(xué)題目搜索證明，成功通過(guò)形式化驗(yàn)證的證明拿來(lái)進(jìn)行訓(xùn)練，以此不斷迭代，不斷提升解題神經(jīng)網(wǎng)絡(luò)的性能。
事實(shí)上，在2024年5月，我們的DeepSeek-Prover團(tuán)隊(duì)就已經(jīng)提出了一個(gè)相似的方法：我們同樣通過(guò)大規(guī)模的自動(dòng)形式化方法來(lái)合成證明數(shù)據(jù)，進(jìn)行迭代訓(xùn)練，不斷提升定理證明模型的表現(xiàn)。
在我們的論文中，還分享了一些數(shù)據(jù)合成流程設(shè)計(jì)的細(xì)節(jié)。例如，使用模型生成的形式化數(shù)學(xué)問(wèn)題可能是錯(cuò)誤的，我們就讓模型同時(shí)嘗試證明它和證偽它。類(lèi)似于AlphaGo在圍棋中進(jìn)行“左右互搏”的方法，只要有一方面的證明成功，我們就認(rèn)為模型成功證明了該定理，并把該證明加入訓(xùn)練數(shù)據(jù)中繼續(xù)進(jìn)行迭代。
MiniF2F是一個(gè)標(biāo)準(zhǔn)的形式化定理證明Benchmark，主要衡量模型在高中數(shù)學(xué)競(jìng)賽中的表現(xiàn)。2024年5月，我們的DeepSeek-Prover V1模型打破了Meta維持了兩年的SOTA（最先進(jìn)水平）。此后，該領(lǐng)域變得越來(lái)越活躍，各種方法層出不窮，形式化定理證明模型也以更快的速度發(fā)展。
值得一提的是，在我們于2024年8月推出的DeepSeek-Prover-V1.5中，已經(jīng)訓(xùn)練得到了一些與目前流行的推理模型相似的行為模式：大模型先進(jìn)行一系列的思維步驟，然后再將這些思維步驟轉(zhuǎn)落實(shí)為正式的回答。
正如以下實(shí)例展示的那樣，模型首先在注釋塊中進(jìn)行完整的推理再開(kāi)始進(jìn)行形式化編碼，甚至在正式代碼的寫(xiě)作中，對(duì)每一行證明的寫(xiě)作前都先進(jìn)行思考和規(guī)劃。這表明，我們的模型在一定程度上已經(jīng)具備了先思考再作答的能力。盡管它在反思和回溯能力上仍然與目前最先進(jìn)的推理模型有距離，但我相信這或許將是形式化數(shù)學(xué)定理證明模型的下一個(gè)突破的方向。
通過(guò)這個(gè)例子，我希望表達(dá)的是：形式化數(shù)學(xué)作為大語(yǔ)言模型的一個(gè)應(yīng)用領(lǐng)域或一種實(shí)踐方向，為探索模型推理能力的訓(xùn)練提供了嚴(yán)格驗(yàn)證反饋的良好環(huán)境，能夠在一定程度上對(duì)其他更通用領(lǐng)域的研究起到借鑒作用。
接下來(lái)，我想談?wù)剬?duì)未來(lái)發(fā)展方向的展望。在形式化數(shù)學(xué)定理證明的領(lǐng)域，我們期望使用大語(yǔ)言模型在哪些方面取得進(jìn)一步的突破？
首先，我們希望語(yǔ)言模型能夠主動(dòng)提出一些有意義的數(shù)學(xué)猜想，證明它們可以幫助我們更好地完成目標(biāo)定理的證明，或者發(fā)現(xiàn)已有數(shù)學(xué)結(jié)論之間的深層聯(lián)系，甚至指導(dǎo)未來(lái)的數(shù)學(xué)研究方向。
更進(jìn)一步，我們希望模型能夠獨(dú)立的發(fā)現(xiàn)一些數(shù)學(xué)抽象。
事實(shí)上，數(shù)學(xué)研究中最好的工作是能夠發(fā)現(xiàn)一些獨(dú)創(chuàng)的結(jié)構(gòu)，而往往不僅僅是解決已經(jīng)提出的猜想，也就是我們所熟悉的一句話就叫“提出問(wèn)題比發(fā)現(xiàn)問(wèn)題更重要”。
比如巴拿赫就說(shuō)過(guò)，好的數(shù)學(xué)家就是發(fā)現(xiàn)定理之間、定理的證明之間的相似性，而最好的數(shù)學(xué)家能夠發(fā)現(xiàn)類(lèi)比之間的類(lèi)比，或者說(shuō)發(fā)現(xiàn)更加高階的抽象。
這方面的工作其實(shí)也已經(jīng)有探索，比如說(shuō)在2021年時(shí)候有一個(gè)叫DreamCoder的項(xiàng)目，已經(jīng)在相對(duì)簡(jiǎn)單的Lambda Calculus上取得了進(jìn)展。它從一些非常簡(jiǎn)單的概念出發(fā)，能夠成功抽象得到復(fù)雜的概念，甚至發(fā)現(xiàn)了一些物理定律。
最后， 我們希望語(yǔ)言模型能夠獨(dú)立地構(gòu)建一個(gè)完整的數(shù)學(xué)知識(shí)庫(kù)。
例如，人類(lèi)在數(shù)學(xué)工作中、甚至是模型在迭代訓(xùn)練中都會(huì)發(fā)現(xiàn)很多零散的定義和結(jié)論，它們之間存在重疊或依賴關(guān)系。我們希望語(yǔ)言模型能夠以一種結(jié)構(gòu)化的方式將它們整合起來(lái)，形成一個(gè)層次分明、結(jié)構(gòu)良好的知識(shí)體系，在其中更一般的定理可以統(tǒng)攝更具體的定理，實(shí)現(xiàn)從高層觀點(diǎn)到初等事實(shí)之間的整合。
實(shí)際上，我們?cè)?024年也已經(jīng)有一個(gè)非常相似的工作，LEGO Prover，它獲得了2024年頂級(jí)學(xué)術(shù)會(huì)議ICLR的口頭報(bào)告推薦。和以往的的模型嘗試直接生成完整證明不同，我們讓模型在嘗試證明之前先提出一些引理，利用這些引理能夠幫助我們更好地證明目標(biāo)定理。在這個(gè)過(guò)程中得到的這些引理會(huì)被收集到技能庫(kù)中以供稍后復(fù)用，以這種方式我們能夠引導(dǎo)模型積累知識(shí)、提升性能。模型手上的工具越來(lái)越多，可以更好地來(lái)適應(yīng)由弱到強(qiáng)的泛化，一步一步地學(xué)會(huì)做一些更加復(fù)雜的問(wèn)題。
5.LLM在形式化數(shù)學(xué)中的挑戰(zhàn)和局限
最后想要分享一下在形式化數(shù)學(xué)定理證明領(lǐng)域應(yīng)用大語(yǔ)言模型仍然存在的一些挑戰(zhàn)和局限。
首先，數(shù)據(jù)稀缺。大語(yǔ)言模型的訓(xùn)練是超大規(guī)模數(shù)據(jù)驅(qū)動(dòng)的，但形式化數(shù)學(xué)領(lǐng)域的數(shù)據(jù)相對(duì)稀缺。這使得直接訓(xùn)練模型變得非常困難。因此，這個(gè)領(lǐng)域的發(fā)展會(huì)更加依賴合成數(shù)據(jù)的作用。
其次，自然語(yǔ)言與形式語(yǔ)言的翻譯。正如我們之前談到，自然語(yǔ)言和形式語(yǔ)言之間的相互翻譯并非易事。
第三，形式系統(tǒng)的復(fù)雜性。形式系統(tǒng)為了保證嚴(yán)格推理，每個(gè)定理都必須在原則上能夠追溯到原始公理，這會(huì)導(dǎo)致整個(gè)系統(tǒng)變得非常臃腫龐大。例如Lean的標(biāo)準(zhǔn)數(shù)學(xué)庫(kù)中有超過(guò)2000個(gè)代碼文件、將近180萬(wàn)行代碼，進(jìn)行新的定理證明需要準(zhǔn)確調(diào)用其中已有的結(jié)論，這實(shí)際上是一個(gè)非常困難的任務(wù)。我認(rèn)為要使用大語(yǔ)言模型做好形式化數(shù)學(xué)需要擁有在大規(guī)模代碼庫(kù)上工作的Agent能力，而這目前是一個(gè)公認(rèn)的挑戰(zhàn)。
那么，如果我們?cè)跀?shù)學(xué)領(lǐng)域成功應(yīng)用了大型語(yǔ)言模型，又意味著什么呢？
我會(huì)從對(duì)數(shù)學(xué)研究、對(duì)工業(yè)規(guī)模的驗(yàn)證、對(duì)數(shù)學(xué)教育、對(duì)一般應(yīng)用這四個(gè)方面去談。從我個(gè)人的觀點(diǎn)看，DeepSeek之所以受到這么大的關(guān)注，很大程度上是因?yàn)樗故玖艘粋€(gè)道理：如果說(shuō)智能可以就像自來(lái)水一樣，價(jià)格低廉、規(guī)模可擴(kuò)展、質(zhì)量可以信賴，它是會(huì)改變整個(gè)世界的。這就像古羅馬能夠創(chuàng)造一種繁榮的文明形態(tài)，與輸水管道等可靠的基礎(chǔ)設(shè)施是密不可分的。
對(duì)于數(shù)學(xué)研究而言，我們希望能開(kāi)發(fā)一種服務(wù)或產(chǎn)品，幫助數(shù)學(xué)家快速驗(yàn)證一些簡(jiǎn)單的但勞動(dòng)密集的猜想，將他們從繁瑣的細(xì)節(jié)中解放出來(lái)。語(yǔ)言模型可以充當(dāng)人機(jī)交互的接口，將自然語(yǔ)言問(wèn)題翻譯成代碼，利用已有知識(shí)庫(kù)中進(jìn)行嚴(yán)格驗(yàn)證，并將結(jié)果以自然語(yǔ)言的形式反饋給數(shù)學(xué)家。
第二個(gè)方面就是關(guān)于工業(yè)中的大規(guī)模驗(yàn)證。事實(shí)上，除了數(shù)學(xué)之外，形式化方法也在軟硬件驗(yàn)證上有廣闊的應(yīng)用，例如英特爾在芯片驗(yàn)證上廣泛使用了大規(guī)模的SAT/SMT求解器，而定理證明器可以在更高層次的抽象上完成嚴(yán)格的規(guī)約驗(yàn)證。然而，由于需要專家花費(fèi)長(zhǎng)時(shí)間進(jìn)行證明編碼，在實(shí)踐中廣泛實(shí)施中的代價(jià)非常高昂，極大限制了形式化方法的應(yīng)用。我們希望語(yǔ)言模型能夠加速形式驗(yàn)證的普及，使其能夠以更低廉、更可擴(kuò)展的方式應(yīng)用于更廣泛的領(lǐng)域，避免軟硬件漏洞可能導(dǎo)致的巨大損失。
第三個(gè)方面就是教育。我們可以保存和傳承那些可能被遺忘的數(shù)學(xué)知識(shí)。隨著老一代數(shù)學(xué)家的退出，他們的研究成果可能會(huì)逐漸被人遺忘。但語(yǔ)言模型可以成為一種可擴(kuò)展的知識(shí)載體，保存和傳承這些長(zhǎng)尾的數(shù)學(xué)知識(shí)。
總之，大語(yǔ)言模型為數(shù)學(xué)提供了一種嚴(yán)格且可持續(xù)的知識(shí)載體和應(yīng)用手段，我們認(rèn)為它在自動(dòng)化形式化和定理證明方面具有廣闊的應(yīng)用前景。
雖然目前仍然面臨數(shù)據(jù)稀缺、自然語(yǔ)言對(duì)齊以及系統(tǒng)復(fù)雜性等挑戰(zhàn)，但我們相信，隨著技術(shù)的不斷發(fā)展，大語(yǔ)言模型將在數(shù)學(xué)領(lǐng)域發(fā)揮越來(lái)越重要的作用，同時(shí)也將推動(dòng)軟硬件驗(yàn)證以及其他科學(xué)應(yīng)用的進(jìn)步。
6.問(wèn)答環(huán)節(jié)
問(wèn)：DeepSeek有哪些創(chuàng)新之處？這些創(chuàng)新對(duì)AI開(kāi)發(fā)者有哪些啟示？在提升算力利用率方面，我們應(yīng)該關(guān)注什么呢？
辛華劍：DeepSeek震動(dòng)華爾街一個(gè)方面是它的訓(xùn)練成本非常低，這與DeepSeek在算力管控方面的工作密不可分。在實(shí)際工作中，尤其對(duì)于大模型而言，如何制定合適的算力策略至關(guān)重要。如果我們有更多的卡，肯定不會(huì)太顧及算力的使用效率，所以有些時(shí)候資源有限是能夠促進(jìn)創(chuàng)新的活躍的，但另一方面，在算力不足的情況下，也難以在scaling law上獲得正確的認(rèn)知。這其實(shí)是一個(gè)比較矛盾的問(wèn)題。
問(wèn)：DeepSeek-Prover-1.5的定理證明在邏輯上是百分之百正確的嗎？
辛華劍：我們強(qiáng)調(diào)通過(guò)驗(yàn)證的證明是正確的，但這句話的前提在于我們對(duì)數(shù)學(xué)問(wèn)題進(jìn)行的形式化建模是正確的，以及它所最終實(shí)現(xiàn)的這個(gè)程序語(yǔ)義是符合我們期望的。
問(wèn)：MCTS（蒙特卡洛樹(shù)搜索）對(duì)于模型訓(xùn)練很重要嗎？
辛華劍：我們?cè)贒eepSeek-Prover-V1.5階段確實(shí)做了MCTS，但我們發(fā)現(xiàn)MCTS和獨(dú)立的采樣相比，表現(xiàn)并沒(méi)有非常大的收益。這可能與DeepSeek-R1技術(shù)報(bào)告里說(shuō)MCTS不太成功的結(jié)論是吻合的，不過(guò)在做R1的時(shí)候我已經(jīng)離開(kāi)DeepSeek了，所以我也只是猜測(cè)。
問(wèn)：在資源有限的情況下，如何分配訓(xùn)練和推理資源才能達(dá)到最佳效果？“大模型+無(wú)推理”和“中模型+花費(fèi)更多token來(lái)做推理”哪個(gè)更好？
辛華劍：這是一個(gè)非常好的問(wèn)題，也是我們?cè)谧鯬rover項(xiàng)目中實(shí)際面臨的挑戰(zhàn)。比如，在初期探索階段，我們是用小規(guī)模模型（如幾百M(fèi)）進(jìn)行大規(guī)模的MCTS（蒙特卡洛樹(shù)搜索），還是用更大規(guī)模的模型（如幾十B）來(lái)做小規(guī)模的推理？一個(gè)可以參考的例子是，去年在AIMO（人工智能數(shù)學(xué)奧林匹克競(jìng)賽）的第二名團(tuán)隊(duì)對(duì)模型采樣方法以及規(guī)模上的平衡做了細(xì)致的研究，大家參考他們的報(bào)告《An Empirical Analysis of Compute-Optimal Inference for Problem-Solving with Language Models》。
問(wèn)：AI是否會(huì)取代人類(lèi)從事科研工作？例如，在數(shù)學(xué)、物理、化學(xué)等領(lǐng)域，哪些學(xué)科更容易被AI賦能？
辛華劍：我個(gè)人從事AI For Math的研究，我認(rèn)為數(shù)學(xué)是一個(gè)AI與人類(lèi)進(jìn)行溝通的良好橋梁。因?yàn)閿?shù)學(xué)是一個(gè)更傾向于純粹的思辨，而非實(shí)驗(yàn)的學(xué)科。這使得在AI大模型開(kāi)發(fā)階段，與環(huán)境交互的方式更加簡(jiǎn)潔，從而方便AI算法的開(kāi)發(fā)和驗(yàn)證。當(dāng)然，最近我們也看到AI在實(shí)驗(yàn)科學(xué)領(lǐng)域也有所應(yīng)用。例如，有研究機(jī)構(gòu)嘗試讓AI參與實(shí)驗(yàn)，甚至讓AI像學(xué)生一樣手動(dòng)進(jìn)行實(shí)驗(yàn)，從中獲取經(jīng)驗(yàn)和知識(shí)。我認(rèn)為，AI在各個(gè)科研領(lǐng)域都在進(jìn)行探索，而未來(lái)2到5年可能會(huì)有更顯著的進(jìn)展。
問(wèn)：LLM的幻覺(jué)問(wèn)題會(huì)對(duì)數(shù)學(xué)定理造成怎樣的影響？
辛華劍：這個(gè)問(wèn)題非常困擾我們。我們發(fā)現(xiàn)很多時(shí)候它會(huì)提出一些數(shù)學(xué)庫(kù)里面根本就沒(méi)有的定義或定理，或者說(shuō)它在訓(xùn)練過(guò)程中記住了一些名字，但這些名字在當(dāng)前的使用階段已經(jīng)不再使用了，但模型仍然會(huì)使用類(lèi)似的東西。我覺(jué)得這方面的解決歸根結(jié)底需要Agent能力，需要大語(yǔ)言模型和整個(gè)系統(tǒng)進(jìn)行充分的交互，實(shí)際判斷它現(xiàn)在工作的這個(gè)基礎(chǔ)數(shù)學(xué)庫(kù)到底已經(jīng)有什么樣的內(nèi)容。
問(wèn)：展望未來(lái)十年，人工智能領(lǐng)域最令人興奮的機(jī)會(huì)是什么？最大的挑戰(zhàn)又是什么呢？
辛華劍：事實(shí)上，在o1出現(xiàn)之前，我根本沒(méi)有想到可以把思維鏈拉得這樣長(zhǎng)，出現(xiàn)足夠自主反思能力的推理模型。我認(rèn)為這樣的技術(shù)進(jìn)展，往往非?？缭叫缘?，即使是在一線訓(xùn)練模型的同學(xué)也不一定能對(duì)未來(lái)有準(zhǔn)確的預(yù)測(cè)。我感覺(jué)很多時(shí)候AI就像一種魔法，它會(huì)有怎樣的結(jié)果，只有真正動(dòng)手試一試才知道。對(duì)于我們來(lái)說(shuō)這恰恰是做AI研究工作最大的motivation（驅(qū)動(dòng)力），它確實(shí)是一個(gè)需要充分想象力的學(xué)科。
關(guān)注公眾號(hào)「甲子光年」，后臺(tái)回復(fù)“數(shù)學(xué)”，獲得辛華劍《大語(yǔ)言模型時(shí)代的形式化數(shù)學(xué)革命》演講高清完整版PDF?；蛘唿c(diǎn)擊文末“閱讀原文”，進(jìn)入相關(guān)鏈接下載。
作者：王藝
2025-02-17
90940
0
0
0