大語言模型，果然可以用來研究數(shù)學(xué)定理！

最近，微軟亞洲研究院、北大、北航等機(jī)構(gòu)的研究人員，通過97個(gè)回合的「蘇格拉底式」嚴(yán)格推理，成功讓GPT-4得出了「P≠NP」的結(jié)論！

論文地址：https://arxiv.org/abs/2309.05689

幾個(gè)月前，數(shù)學(xué)天才陶哲軒曾在一篇博客中稱，2026年，AI將與搜索和符號(hào)數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴的合著者。

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

如今，GPT-4用出色的表現(xiàn)再次證明，LLM的確有進(jìn)行科學(xué)研究和科學(xué)發(fā)現(xiàn)的能力。

P/NP難題有多難

作為美國克雷數(shù)學(xué)研究所（CMI）在2000年公布的七個(gè)千禧年難題之一，「P/NP問題」目前依然是理論信息學(xué)中計(jì)算復(fù)雜度理論領(lǐng)域里的未解之謎。

人們喜歡把它描述為「很可能是位居理論計(jì)算機(jī)科學(xué)核心的未解決問題」，也是人類提出的最深刻的問題之一。如果解決解決P/NP難題，將徹底改變?nèi)祟愇拿鬟M(jìn)程。

1971年，數(shù)學(xué)家Stephen A. Cook和Leonid Levin相對(duì)獨(dú)立地提出這個(gè)問題：兩個(gè)復(fù)雜度類P和NP是否是恒等的？

具體來說，一些永遠(yuǎn)無法通過簡單計(jì)算得到答案的問題，就屬于P/NP問題。

一個(gè)復(fù)雜問題如果能在多項(xiàng)式時(shí)間內(nèi)解決，就被稱為P問題，意味著計(jì)算機(jī)很容易將它求解。

那NP問題就是除了P問題之外的問題嗎？未必。我們并不能證明一個(gè)問題能在多項(xiàng)式時(shí)間內(nèi)解決，也無法證明它不能在多項(xiàng)式時(shí)間內(nèi)解決。

所以，NP問題并不是非P類問題。

聽起來似乎很復(fù)雜，我們可以用集水滸英雄卡的故事來類比。二十多年前集過卡的讀者應(yīng)該都知道，無論是加大購買量，還是擴(kuò)大購買范圍，都很難集齊全套水滸英雄。

這其實(shí)就是一個(gè)P/NP問題——是否有一種方法，讓集卡的過程輕而易舉？

所以，GPT-4是怎樣得出P≠NP的？讓我們往下看。

97輪對(duì)話，給出P≠NP結(jié)論

在這項(xiàng)研究中，研究者GPT-4學(xué)會(huì)了一種「蘇格拉底式推理」。

他們引入了五個(gè)不同的角色（比如精通概率論的數(shù)學(xué)家），作為協(xié)助證明者，根據(jù)自己擅長證明不同的部分。

GPT-4用這種方法，開發(fā)了一種推理路徑，得出了和北航Ke Xu、北工商Guangyan Zhou（論文三作和四作）最近提出結(jié)果一致的結(jié)論！

論文地址：https://arxiv.org/pdf/2302.09512.pdf

在最初的14輪對(duì)話中，GPT-4被引導(dǎo)設(shè)計(jì)出了初步的證明模式。

GPT-4被問的第一個(gè)問題是：「你能從哲學(xué)角度而不是計(jì)算機(jī)理論角度找到P!=NP問題背后的根本問題嗎？」

在這個(gè)提示中，技巧在于鼓勵(lì)模型創(chuàng)造性回答，避免進(jìn)行檢索。比如，「如何證明 P!=NP」這樣的提示可能會(huì)引導(dǎo)大模型進(jìn)行檢索。

用上「蘇格拉底式推理」中的轉(zhuǎn)換模式后，就可以生成更具創(chuàng)新性的回答。

對(duì)于這個(gè)問題，GPT-4是這么回答的——

P!=NP問題背后的基本哲學(xué)問題，可以看作是創(chuàng)造力、直覺和洞察力（通常與NP問題相關(guān)）與系統(tǒng)化、算法和確定性方法（與P問題相關(guān)）之間的矛盾。

如果P=NP，那就意味著宇宙有一種基本的簡單性，表面上看似復(fù)雜的問題都有高效、優(yōu)雅的解決方案。

看來，GPT-4對(duì)P!=NP理解得很透徹，在此基礎(chǔ)上，研究者開始提問了——

「 是否所有表面上看似復(fù)雜的問題都有高效、優(yōu)雅的解決方案？如果不是，可以用什么方法來證明？」

GPT-4回答說，并非所有表面看來復(fù)雜的問題都有高效、優(yōu)雅的解決方案，這可以歸因于多種因素，比如所涉及變量的數(shù)量、變量之間關(guān)系的性質(zhì)，或問題本身的內(nèi)在難度。

然后，它提出了六種方法，其中一種是「矛盾證明」，即要證明一個(gè)問題沒有高效、優(yōu)雅的解決方案，可以假設(shè)存在這樣的解決方案，然后證明這一假設(shè)會(huì)導(dǎo)致矛盾，這樣就可以有力地證明某些解法不可能存在。

可以看到，GPT-4在回答問題過程中，真的像人類一樣擁有思辨能力。

緊接著，研究人員趁熱打鐵，繼續(xù)問道，「我們想用矛盾證明P!=NP，請(qǐng)列出幾種可能的思路?！?/span>

這次GPT-4依然給出了六個(gè)答案，不過并不嚴(yán)謹(jǐn)。

要通過矛盾證明，必須找到一個(gè)無法在多項(xiàng)式時(shí)間內(nèi)解決的NP完全（NP-complete）問題。

不過，這個(gè)回答可以啟發(fā)GPT-4在以后的對(duì)話中思考NP完全問題。

在第四輪提問中，GPT-4的回答中出現(xiàn)了諸多亮點(diǎn)。

「該怎樣構(gòu)建這些問題呢？」

比如它回答說：我們可以從眾所周知的NP完全問題入手，例如旅行商問題 （TSP）、布爾可滿足性問題（SAT）或分團(tuán)問題（Clique）。

隨后的提問中，GPT-4被引導(dǎo)著給出了越來越多智慧的回答，也讓研究開始一步步深入問題中心。

就這樣，經(jīng)過14輪連續(xù)對(duì)話，研究人員讓GPT-4對(duì)3-13步的歷史內(nèi)容，梳理出一個(gè)證明思路。

對(duì)此，GPT-4的總結(jié)中，突出顯示的兩個(gè)部分是研究后續(xù)證明的2個(gè)關(guān)鍵點(diǎn)。

第4點(diǎn)建立了一個(gè)基本的直覺，即一旦證明了極難CSP的存在，就可以使用「矛盾證明」來證明這些問題無法在多項(xiàng)式時(shí)間內(nèi)求解。

而第6點(diǎn)恰好成為后續(xù)證明工作的通用模式。

從下一輪開始，研究人員便遵循這一初步方案，嚴(yán)格地進(jìn)行證明。

然后，研究者按照草稿，在隨后的83輪對(duì)話中進(jìn)行了嚴(yán)格的推理。

而這97輪對(duì)話，可以說構(gòu)建出了一個(gè)極難的NP完全問題，其中一些實(shí)例在時(shí)間復(fù)雜度低于（即窮舉搜索）的情況下是不可解的，也就是說，證明結(jié)論為P≠NP。

是的，如果你能嚴(yán)格證明存在一種特定類型的NP完全問題，當(dāng)變量數(shù)趨于無窮大時(shí)，無法在多項(xiàng)式時(shí)間內(nèi)求解這類問題，就可以認(rèn)為，證明了P!=NP。

在Ke Xu和Guangyan Zhou的論文中，他們構(gòu)建了CSP和SAT的極難示例，證明了這些示例在沒有窮舉法的情況下無法求解。

而GPT-4，也得出了一致的結(jié)論。

是的，如果我們能夠證明不存在一種算法能夠以低于的時(shí)間復(fù)雜度解決某些SAT實(shí)例，那么當(dāng)變量數(shù)量趨于無窮大時(shí)，它確實(shí)可以為某些無法在多項(xiàng)式時(shí)間內(nèi)解決的NP完全問題的存在提供強(qiáng)有力的證據(jù)。

這項(xiàng)研究再次證明，GPT-4有充分的潛力與人類合作，共同探索極其復(fù)雜的專家級(jí)難題。

LLM不僅能掌握基本知識(shí)，還可以在廣泛的解空間中發(fā)現(xiàn)新的見解。這也預(yù)示著科學(xué)LLM的范式下，科學(xué)發(fā)現(xiàn)的無限前景。

蘇格拉底式推理

那么，GPT-4展現(xiàn)出如此強(qiáng)大，思維推理能力，背后的極致究竟是什么呢？

古希臘哲學(xué)家蘇格拉曾說過，「我不能教會(huì)別人任何事，我只能讓他們思考」。

這次，研究人員恰巧就從中汲取了靈感，提出一種通用問題的解決框架——蘇格拉底式推理（Socratic Reasoning）。

簡單講，蘇格拉底方法就是讓我們「一步一步思考」，提出一系列問題激發(fā)批判性思維。

這對(duì)于大模型來說，如果能夠進(jìn)行批判性思考，就可以針對(duì)復(fù)雜問題提出高效的解決方案。

對(duì)此，研究團(tuán)隊(duì)指出這一框架旨在推動(dòng)LLM解決高度復(fù)雜任務(wù)，協(xié)調(diào)各種子問題，并引導(dǎo)其搭建高層次推理途徑。

「蘇格拉底式推理」是在人類與LLM之間的一系列對(duì)話回合中進(jìn)行的，是與LLM一起解決復(fù)雜挑戰(zhàn)的遞歸機(jī)制。

如下圖所示，「蘇格拉底式推理」有5種強(qiáng)大的提示模式：演繹、轉(zhuǎn)換、分解、驗(yàn)證、整合。

通過發(fā)掘新的見解和觀點(diǎn)，將復(fù)雜問題分解為子問題或步驟，并通過質(zhì)疑回答進(jìn)行自我完善。

「蘇格拉底式推理」中的問題解決模式（用和分別表示（子）問題和結(jié)論

一般來說，在處理可以直接從推理中得出結(jié)論的問題時(shí)，會(huì)采用「演繹模式」（如 「讓我們一步步思考」）來指導(dǎo)LLM直接得出結(jié)論。

對(duì)于更復(fù)雜的問題，首先要求LLM將問題轉(zhuǎn)化為新問題，或分解為若干子問題。然后，通過遞歸方法，直到找到「原子問題」。

P vs. NP問題對(duì)話轉(zhuǎn)換示例

在生成新問題或得出新結(jié)論時(shí)，通過「驗(yàn)證模式」，利用LLM自我批判能力進(jìn)行驗(yàn)證和完善。

最后，「整合模式」要求 LLM 基于子問題的結(jié)果合成結(jié)論。

整個(gè)流程，研究人員鼓勵(lì)LLM通過一系列對(duì)話，遞歸地繼續(xù)上述過程，直至解決目標(biāo)問題。

這篇論文，研究人員揭示了大模型能夠在解決科學(xué)問題中大有可為，能夠在得出復(fù)雜問題結(jié)論中細(xì)化攻堅(jiān)的策略。

通過97論文對(duì)話引導(dǎo)，GPT-4展現(xiàn)出超人能力，完成了千禧數(shù)學(xué)難題全推理過程。

作者介紹

Qingxiu Dong，北京大學(xué)計(jì)算語言學(xué)研究所博士生。

Li Dong，微軟亞洲研究院首席研究員。

此前，他曾于2010年至2015年，在北航軟件開發(fā)環(huán)境國家重點(diǎn)實(shí)驗(yàn)室跟隨Ke Xu從事研究工作。

Ke Xu，北京航空航天大學(xué)計(jì)算機(jī)科學(xué)教授。

此前，他在北京航空航天大學(xué)獲得了學(xué)士、碩士和博士學(xué)位。研究興趣包括算法與復(fù)雜性、數(shù)據(jù)挖掘和網(wǎng)絡(luò)。