把数学变成谜题：SAT 求解器如何让机器自动写出人类做不到的证明

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/