把數學變成謎題：SAT 求解器如何讓機器自動寫出人類做不到的證明

來源：ScienceAI

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

Heule 使用了一種名為可滿足性（SAT）的計算方式將它們一一攻克。現在，作為卡內基梅隆大學計算輔助數學推理研究所的一員，他認為 SAT 可以與大型語言模型（LLMs）結合，創造出足以解決更難純數學問題的工具。

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

圖示：3-SAT 實例。（來源：網絡）

但是 AI 可以。

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

Q：首先：什么是 SAT？

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

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

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

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

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

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

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

圖注：歐幾里得的《幾何要素》深刻地影響了數學家對嚴謹性的看法。但在過去的 400 年里，數學變得越來越抽象。（來源：網絡）

Q：如果本身就很難理解的 LLMs 進入到復雜的場景，難道問題不會更加嚴重嗎？

事實上，當今世上沒有哪位數學家能完全理解所有數學。更多的是，有些信譽良好的數學家能夠針對每個拼圖的小部分說：“好的，我檢查過了。這是正確的。”然后其他人可以在此基礎上繼續構建。

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

Q：假設你所描述的 LLMs 與 SAT 之間的生產性互動已經被構建了，人類數學家還能剩下什么工作要做？

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

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

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

閱讀最新前沿科技趨勢報告，請訪問歐米伽研究所的“未來知識庫”

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

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