![]()
Marijn Heule 近十年來(lái)致力于破解數(shù)學(xué)難題,倘若將他的工作寫成小說(shuō),可能更像特工代號(hào):空六邊形、舒爾數(shù) 5、凱勒猜想、七維。事實(shí)上,這些曾是幾何學(xué)和組合數(shù)學(xué)中最頑固的問(wèn)題之一,困擾了人們 90 年甚至更長(zhǎng)時(shí)間。
Heule 使用了一種名為可滿足性(SAT)的計(jì)算方式將它們一一攻克。現(xiàn)在,作為卡內(nèi)基梅隆大學(xué)計(jì)算輔助數(shù)學(xué)推理研究所的一員,他認(rèn)為 SAT 可以與大型語(yǔ)言模型(LLMs)結(jié)合,創(chuàng)造出足以解決更難純數(shù)學(xué)問(wèn)題的工具。
其實(shí),SAT 就是人工智能的一個(gè)基礎(chǔ),它屬于符號(hào)人工智能(也稱為 GOFAI,即“傳統(tǒng)的人工智能”),依賴于只有是否判斷的陳述,并依照嚴(yán)密的邏輯將其串聯(lián)起來(lái)。這一鏈條可能會(huì)很長(zhǎng),長(zhǎng)到人類自己根本無(wú)法解析。
![]()
圖示:3-SAT 實(shí)例。(來(lái)源:網(wǎng)絡(luò))
但是 AI 可以。
Heule 表示,他一直對(duì)計(jì)算機(jī)是否可以解決人類推理之外的問(wèn)題很感興趣。Quanta 雜志與 Heule 就機(jī)器與人類推理的差異,SAT 的簡(jiǎn)單性如何成為其秘密武器,以及為什么在數(shù)學(xué)中理解被高估了等問(wèn)題進(jìn)行了深入探討。
Q:首先:什么是 SAT?
大致可以將其想象為一個(gè)棋盤,每個(gè)單元格中只能放 0 或 1。現(xiàn)在已經(jīng)知道了每行每列中可以放多少 0 或 1, 只需要把這個(gè)棋盤擺出來(lái)就行了。盡管這種形式很簡(jiǎn)單,但它非常強(qiáng)大。各種重要問(wèn)題,包括硬件和軟件驗(yàn)證、調(diào)度,甚至純數(shù)學(xué)領(lǐng)域,都可以翻譯成 SAT。
Q:SAT 求解與數(shù)字計(jì)算機(jī)做其他任何事情有什么不同?
SAT 工具做的事情與普通計(jì)算從根本上不同。它不是用 0 和 1 進(jìn)行計(jì)算。相反,是在尋找一個(gè)滿足所有約束的組合。
Q:生成式人工智能可以幫助研究過(guò)程本身。SAT 在這種情況下扮演什么角色?
在這種情境下,LLM 可以生成許多聽(tīng)起來(lái)似是而非的引理,「用于證明更大定理的陳述」。自動(dòng)推理會(huì)檢驗(yàn)這些是否正確。
一旦出現(xiàn)錯(cuò)誤,SAT 求解器就可以返回反例——理想情況下,是最小的反例。畢竟,實(shí)驗(yàn)者并不希望在詢問(wèn) SAT 求解器時(shí),它返回一個(gè)巨大的、難以理解的對(duì)象。
這看上去有點(diǎn)像 AI 的「目標(biāo)計(jì)算機(jī)」。它們都將整個(gè)局面拆分為若干小段,自動(dòng)推理在此時(shí)就可以一一對(duì)其進(jìn)行檢查。同樣重要的是,它還可以檢查這些部件是否真正涵蓋了所有內(nèi)容,這樣就不會(huì)有任何遺漏。
![]()
圖注:歐幾里得的《幾何要素》深刻地影響了數(shù)學(xué)家對(duì)嚴(yán)謹(jǐn)性的看法。但在過(guò)去的 400 年里,數(shù)學(xué)變得越來(lái)越抽象。(來(lái)源:網(wǎng)絡(luò))
Q:如果本身就很難理解的 LLMs 進(jìn)入到復(fù)雜的場(chǎng)景,難道問(wèn)題不會(huì)更加嚴(yán)重嗎?
事實(shí)上,當(dāng)今世上沒(méi)有哪位數(shù)學(xué)家能完全理解所有數(shù)學(xué)。更多的是,有些信譽(yù)良好的數(shù)學(xué)家能夠針對(duì)每個(gè)拼圖的小部分說(shuō):“好的,我檢查過(guò)了。這是正確的。”然后其他人可以在此基礎(chǔ)上繼續(xù)構(gòu)建。
LLMs 可以胡說(shuō)八道,但只要自動(dòng)化推理能夠說(shuō):“好的,但這一部分實(shí)際上是正確的,這里有一個(gè)證明,”這實(shí)際上比大多數(shù)紙筆證明更加可信。
Q:假設(shè)你所描述的 LLMs 與 SAT 之間的生產(chǎn)性互動(dòng)已經(jīng)被構(gòu)建了,人類數(shù)學(xué)家還能剩下什么工作要做?
在之前,我用 SAT 解決開(kāi)放問(wèn)題時(shí),總是會(huì)與數(shù)學(xué)家共事。我吸收學(xué)習(xí)他們的看法并將其編碼,以便求解器能完成工作。未來(lái)的協(xié)作方式可能與之類似。LLMs 可以幫助更多數(shù)學(xué)家學(xué)習(xí)如何自己做到這一點(diǎn)。
在數(shù)學(xué)家、生成式 AI 和自動(dòng)化推理的共同努力下,我們有機(jī)會(huì)攻克長(zhǎng)期存在的開(kāi)放問(wèn)題。但完全剔除人工會(huì)是一個(gè)錯(cuò)誤。創(chuàng)造性直覺(jué)、概念重構(gòu),這些仍然是人類獨(dú)特擅長(zhǎng)的事情。真正的魔力仍來(lái)自于合作。
原文鏈接:https://www.quantamagazine.org/to-have-machines-make-math-proofs-turn-them-into-a-puzzle-20251110/
特別聲明:以上內(nèi)容(如有圖片或視頻亦包括在內(nèi))為自媒體平臺(tái)“網(wǎng)易號(hào)”用戶上傳并發(fā)布,本平臺(tái)僅提供信息存儲(chǔ)服務(wù)。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.