把數(shù)學(xué)變成謎題：SAT 求解器如何讓機(jī)器自動(dòng)寫出人類做不到的證明

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/