來源：ScienceAI

Marijn Heule 近十年來致力于破解數(shù)學(xué)難題，倘若將他的工作寫成小說，可能更像特工代號(hào)：空六邊形、舒爾數(shù) 5、凱勒猜想、七維。事實(shí)上，這些曾是幾何學(xué)和組合數(shù)學(xué)中最頑固的問題之一，困擾了人們 90 年甚至更長時(shí)間。

Heule 使用了一種名為可滿足性（SAT）的計(jì)算方式將它們一一攻克?，F(xiàn)在，作為卡內(nèi)基梅隆大學(xué)計(jì)算輔助數(shù)學(xué)推理研究所的一員，他認(rèn)為 SAT 可以與大型語言模型（LLMs）結(jié)合，創(chuàng)造出足以解決更難純數(shù)學(xué)問題的工具。

其實(shí)，SAT 就是人工智能的一個(gè)基礎(chǔ)，它屬于符號(hào)人工智能（也稱為 GOFAI，即“傳統(tǒng)的人工智能”），依賴于只有是否判斷的陳述，并依照嚴(yán)密的邏輯將其串聯(lián)起來。這一鏈條可能會(huì)很長，長到人類自己根本無法解析。

圖示：3-SAT 實(shí)例。（來源：網(wǎng)絡(luò)）

但是 AI 可以。

Heule 表示，他一直對(duì)計(jì)算機(jī)是否可以解決人類推理之外的問題很感興趣。Quanta 雜志與 Heule 就機(jī)器與人類推理的差異，SAT 的簡(jiǎn)單性如何成為其秘密武器，以及為什么在數(shù)學(xué)中理解被高估了等問題進(jìn)行了深入探討。

Q：首先：什么是 SAT？

大致可以將其想象為一個(gè)棋盤，每個(gè)單元格中只能放 0 或 1?，F(xiàn)在已經(jīng)知道了每行每列中可以放多少 0 或 1， 只需要把這個(gè)棋盤擺出來就行了。盡管這種形式很簡(jiǎn)單，但它非常強(qiáng)大。各種重要問題，包括硬件和軟件驗(yàn)證、調(diào)度，甚至純數(shù)學(xué)領(lǐng)域，都可以翻譯成 SAT。

Q：SAT 求解與數(shù)字計(jì)算機(jī)做其他任何事情有什么不同？

SAT 工具做的事情與普通計(jì)算從根本上不同。它不是用 0 和 1 進(jìn)行計(jì)算。相反，是在尋找一個(gè)滿足所有約束的組合。

Q：生成式人工智能可以幫助研究過程本身。SAT 在這種情況下扮演什么角色？

在這種情境下，LLM 可以生成許多聽起來似是而非的引理，「用于證明更大定理的陳述」。自動(dòng)推理會(huì)檢驗(yàn)這些是否正確。

一旦出現(xiàn)錯(cuò)誤，SAT 求解器就可以返回反例——理想情況下，是最小的反例。畢竟，實(shí)驗(yà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)性的看法。但在過去的 400 年里，數(shù)學(xué)變得越來越抽象。（來源：網(wǎng)絡(luò)）

Q：如果本身就很難理解的 LLMs 進(jìn)入到復(fù)雜的場(chǎng)景，難道問題不會(huì)更加嚴(yán)重嗎？

事實(shí)上，當(dāng)今世上沒有哪位數(shù)學(xué)家能完全理解所有數(shù)學(xué)。更多的是，有些信譽(yù)良好的數(shù)學(xué)家能夠針對(duì)每個(gè)拼圖的小部分說：“好的，我檢查過了。這是正確的。”然后其他人可以在此基礎(chǔ)上繼續(xù)構(gòu)建。

LLMs 可以胡說八道，但只要自動(dòng)化推理能夠說：“好的，但這一部分實(shí)際上是正確的，這里有一個(gè)證明，”這實(shí)際上比大多數(shù)紙筆證明更加可信。

Q：假設(shè)你所描述的 LLMs 與 SAT 之間的生產(chǎn)性互動(dòng)已經(jīng)被構(gòu)建了，人類數(shù)學(xué)家還能剩下什么工作要做？

在之前，我用 SAT 解決開放問題時(shí)，總是會(huì)與數(shù)學(xué)家共事。我吸收學(xué)習(xí)他們的看法并將其編碼，以便求解器能完成工作。未來的協(xié)作方式可能與之類似。LLMs 可以幫助更多數(shù)學(xué)家學(xué)習(xí)如何自己做到這一點(diǎn)。

在數(shù)學(xué)家、生成式 AI 和自動(dòng)化推理的共同努力下，我們有機(jī)會(huì)攻克長期存在的開放問題。但完全剔除人工會(huì)是一個(gè)錯(cuò)誤。創(chuàng)造性直覺、概念重構(gòu)，這些仍然是人類獨(dú)特擅長的事情。真正的魔力仍來自于合作。

原文鏈接：https://www.quantamagazine.org/to-have-machines-make-math-proofs-turn-them-into-a-puzzle-20251110/

閱讀最新前沿科技趨勢(shì)報(bào)告，請(qǐng)?jiān)L問歐米伽研究所的“未來知識(shí)庫”

https://wx.zsxq.com/group/454854145828

未來知識(shí)庫是“ 歐米伽 未來研究所”建立的在線知識(shí)庫平臺(tái)，收藏的資料范圍包括人工智能、腦科學(xué)、互聯(lián)網(wǎng)、超級(jí)智能，數(shù)智大腦、能源、軍事、經(jīng)濟(jì)、人類風(fēng)險(xiǎn)等等領(lǐng)域的前沿進(jìn)展與未來趨勢(shì)。目前擁有超過8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問https://wx.zsxq.com/group/454854145828進(jìn)入。