近日，Meta AI 构建了一个神经定理证明器 HyperTree Proof Search（HTPS），已经解决了 10 场国际数学奥林匹克竞赛 (IMO) 中的问题，比以往任何系统都更多。此外，该 AI 模型的性能比数学基准 miniF2F 上的 SOTA 方法高出 20%，比 Metamath 基准上的 SOTA 方法高出 10%。

 

 

论文地址：https://arxiv.org/pdf/2205.11491.pdf(opens new window)

在一定意义上，定理证明要比构建 AI 来玩国际象棋等棋盘游戏更具挑战性。当研究者试图证明一个定理时，可能移动的动作空间不仅很大而且有可能是无限的。相比较而言，在国际象棋或围棋中，这些游戏的一系列走法会被预测出来，即使算法没有给出最好的走法也影响不大。而在定理证明中，当算法走入死胡同就没办法解决了，性能再好的求解器也只是白费力气。Meta AI的新方法解决了这个棘手的问题，LeCun也转推称赞。

 

 

我们用一个例子来说明 HTPS 的优势：假设 a 和 b 都是质因子为 7 的自然数，并且 7 也是 a + b 的质因子，如果假设 7^7 可以整除(a + b)^7 - a^7 - b^7，那么请证明 a + b 至少是 19。

假如让人类来证明的话，他们大概率会用到二项式。而 HTPS 使用 Contraposition 方法，大大简化了方程，然后再检查多种不同的情况。

contrapose h₄,

simp only [nat.dvd_iff_mod_eq_zero, nat.add_zero] at *,

norm_num [nat.mod_eq_of_lt, mul_comm, nat.add_mod] at h₄,

如下图为本文模型发现的证明示例，即在 miniF2F 中另一个 IMO 问题的证明：

 

内容中包含的图片若涉及版权问题，请及时与我们联系删除