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

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

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

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

但是 AI 可以。

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

Q：首先：什么是 SAT？

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

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

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

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

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

一旦出現(xiàn)錯誤，SAT 求解器就可以返回反例——理想情況下，是最小的反例。畢竟，實驗者并不希望在詢問 SAT 求解器時，它返回一個巨大的、難以理解的對象。

這看上去有點像 AI 的「目標(biāo)計算機」。它們都將整個局面拆分為若干小段，自動推理在此時就可以一一對其進(jìn)行檢查。同樣重要的是，它還可以檢查這些部件是否真正涵蓋了所有內(nèi)容，這樣就不會有任何遺漏。

圖注：歐幾里得的《幾何要素》深刻地影響了數(shù)學(xué)家對嚴(yán)謹(jǐn)性的看法。但在過去的 400 年里，數(shù)學(xué)變得越來越抽象。（來源：網(wǎng)絡(luò)）

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

事實上，當(dāng)今世上沒有哪位數(shù)學(xué)家能完全理解所有數(shù)學(xué)。更多的是，有些信譽良好的數(shù)學(xué)家能夠針對每個拼圖的小部分說：“好的，我檢查過了。這是正確的?！比缓笃渌丝梢栽诖嘶A(chǔ)上繼續(xù)構(gòu)建。

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

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

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

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

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