在新的数学证明中，人工智能取胜

来源：ScienceAI
本文约2000字，建议阅读9分钟
一个以 AlphaGo 等人工智能系统为原型的新计算机程序解决了组合学和图论中的几个未解决问题。

去年 3 月，爱荷华州立大学（Iowa State University）的数学家 Leslie Hogben 和 Carolyn Reinhart 收到了一个惊喜。特拉维夫大学的博士后研究员 Adam Wagner 通过电子邮件告诉他们，他已经回答了他们一周前发表的一个问题——尽管不是通过任何通常的数学或蛮力计算技术。相反，他使用了游戏机。

论文链接：https://arxiv.org/pdf/2103.00647.pdf

「我很高兴这个问题得到了回答。很高兴 Adam 用 AI 做到了这一点。」Hogben 说。

Hogben 和 Reinhart 的问题是 Wagner  使用人工智能解决的四个问题之一。虽然 AI 以前对数学做出了贡献，但 Wagner 对它的使用却不同寻常：他将寻找 Hogben 和 Reinhart 问题的解决方案变成了一种竞赛，使用了其他研究人员在国际象棋等流行策略游戏中成功应用过的方法。

「我看到了很多关于 DeepMind 这样的公司的文章，他们创建了这些程序，可以在真正超人的水平下玩国际象棋、围棋和 Atari 游戏，」Wagner 说。「我想，如果你能以某种方式使用这些自学习算法，这些强化学习算法，并找到一种在数学中使用它们的方法，那该多好？」

Wagner 开始尝试使用类似的策略来提出反例——与数学假设相矛盾（或「反」）的例子，从而证明它是错误的。他将寻找反例重新想象成一场猜谜游戏，然后在数十个开放的数学问题上尝试了他的程序。

「我真的认为这是一项非常漂亮的工作。」悉尼大学教授 Geordie Williamson 说，他也将机器学习与数学研究相结合。

机器学习程序「教」计算机特定的能力。强化学习模型——Wagner 和 DeepMind 都使用的类型——对指令采取不干涉的方法，让计算机反复练习一项任务（如游戏）。该模型只是为了评估计算机的工作而进行干预。作为回应，计算机会在了解哪些方法会导致更好的分数时调整其策略。

强化学习已被证明是在复杂策略游戏中训练模型的有效方法。Wagner 将其应用于数学研究的愿景非常简单。

要了解如何使用强化学习来发现反例，考虑一下这个场景。假设有一个数学猜想，预测表达式 2x – x^2 对于 x 的任何实数值都是负的。这个猜想是不正确的——你可以通过产生一个 x 的值（一个反例）来证明它是错误的。（0 到 2 之间的任何数字都是反例，2x – x^2 的值在 x = 1 处达到峰值。）

为了使用强化学习做到这一点，Wagner 可能会让他的模型在一个由猜测实数 x 组成的游戏中自由发挥。玩完游戏之后，模型会收到它的分数：2x – x^2 的值。最初，由于不知道什么数字可以使分数最大化，该模型会疯狂地猜测。但是一旦模型玩了足够多的时间，一个模式就会变得明显：x 越接近 1，得分越高。通过遵循这种模式，模型一旦猜到 0 到 2 之间的数字，就不可避免地会遇到反例。

Wagner 将相同的基本方案应用于数十个问题，只是改变了计算机允许进行的分数和移动类型。所有的问题都来自离散数学，它处理分离和不同的对象——想想整数，而不是连续的数轴。

问题的离散性使 Wagner 更容易建立模型。例如，Richard Brualdi 和 Lei Cao 在 2020 年提出了一个关于矩阵的问题，其数值为 0 。计算机可以通过循环遍历每个可用点并选择 0 或 1。

「所有这些游戏都只是有限决策的有限序列，」Wagner 说。（允许无限多步骤的游戏会引入新的复杂性。）

Brualdi 和 Cao 的问题涉及一组特定的 0-1 矩阵，他们称之为 312 模式避免（312-pattern avoiding），参考 3 x 3，「312 矩阵」，它表示混合三维向量的元素，使（a ,b,c) 变为 (c,a,b)。0-1 矩阵是 312 模式，如果无法删除它的一些行和列并最终得到 312 矩阵，则可以避免。

更具体地说，Brualdi 和 Cao 的问题是关于矩阵的一个属性，称为「permanent」（积和式），这是一个通过复杂公式获得的数字，该公式涉及所有矩阵项的相加和相乘。他们想知道哪些 312 模式避免矩阵的「permanent」值最大，以及「permanent」值可能达到多大，从而对任意大小的方阵进行猜测。

为了回答他们的问题，Wagner 为他的模型设计了一个游戏：猜一个 0-1 矩阵。一项接着一项，它选择 0 或 1。「permanent」值越大，模型的分数越高，因为没有避开 312 矩阵而被扣分。一旦矩阵为 4 x 4 或更大，该模型就会发现击败 Brualdi 和 Cao 猜测的示例。

这项新工作是一个令人兴奋的概念证明，尽管到目前为止它对数学的实际贡献并不大。

「 [模型解决的问题] 都不是超级重要的猜想。」Wagner 说。

在数学研究的许多重要方面，计算机仍然无法与人脑的能力相匹敌。在试图反驳新论文的一个猜想时，Wagner 的模型碰壁了。它的计算能力太少，无法自行找到反例。尽管如此，它还是产生了一系列猜测，使 Wagner 自己很容易找到一个。

Wagner 说：「只要看看它构建的最好的东西，如果你把它带到任何数学家那里，它不一定是图论家，你应该尝试的东西是非常明显的。」

即使对于 Brualdi 和 Cao 的示例，一旦矩阵变得太大，模型也需要一点帮助。

在数学家将他们的领域让给机器之前，如果有的话，还需要很长时间。与此同时，那些想要利用人工智能的人需要睁大眼睛寻找将其纳入研究的机会。Williamson 说，这就是其他新技术（例如电力）最终揭示其潜力的方式，他认为人工智能没有理由与众不同。

「我们没有发现问题，然后说，[我们必须用电来解决这个问题。] 我们更多的是在说，[我们能做哪些简单的小事？] 」

https://www.quantamagazine.org/in-new-math-proofs-artificial-intelligence-plays-to-win-20220307/

编辑：黄继彦

校对：林亦霖