“教学参考-44”版本间的差异

2022年8月24日 (三) 10:13的最后版本

人工智能与数学是天然的朋友。“用计算来模拟人类智慧”是人工智能的基本思想，而这一思想最早是由数学家提出来的。另外，人工智能从诞生到现在，不论是哪个阶段，都离不开数学的支撑。
反过来，人工智能又为数学家提供了新的工具，不仅极大提高了工作效率，也激发了数学家的灵感。事实上，人工智能最初的成果即是在定理证明上取得的巨大成功。

除了定理证明，机器更擅长的是对猜想进行证伪。给出一个猜想，机器可以快速生成很多实例，用来验证猜想是否成立。和定理证明不同，猜想证伪只要找到一个反例就可以了，因此只要速度足够快，总能找出反例来。
看起来好像很简单，但是仅靠不停地“试”来寻找反例还是非常困难的。科学家们提出了基于机器学习的证伪方法，通过训练一个神经网络，让他生成更具有“威胁”性的反例，从而显著提高证伪过程的效率[1] 。我们用AutoGraphiX猜想来说明这一证伪过程。
AutoGraphiX猜想: 对任何一个包括n个结点的图G，𝑓(𝐺) ≥√(𝑛−1)+1，其中𝑓(G) 是描述G的结构属性的量，可以由G计算出来。
基本思路：设计一个基于神经网络的生成模型，使其生成的G对应的𝑓值尽可能小，从而更有可能是AutoGraphiX猜想的反例。
学习过程：初始化神经网络，生成一批样例图并计算每个样例的其𝑓值。保留𝑓值较小的样例，利用这些样例更新神经网络，使网络倾向于生成这些样例。经过反复迭代，神经网络所生成的样例𝑓值越来越小，越有可能是AutoGraphiX猜想的反例。
经过实验发现，当n ≥ 19时，确实可以发现AutoGraphiX猜想的反例，从而证伪了AutoGraphiX猜想。然而，当𝑛≤18时，计算机并没有发现反例，说明AutoGraphiX猜想有可能是正确的。

机器不仅可以证明或证伪猜想，还可以为数学家出题，主动提出猜想。历史上有很多著名的猜想，比如鼎鼎大名的“哥德巴赫猜想”，“费马大猜想”等等。这些猜想基本都是由一些天才数学家提出来的，不论证明与否，本身就需要顶尖智商和对数学结构的深刻洞察。
2020年，一个以色列研究团队在Nature上发表了一篇论文，报告了他们设计的一款称为“拉马努金机”的程序，可以批量生产数学猜想。他们把精力放在各种数学常数上，如圆周率𝜋和自然对数的底e等，想办法寻找这些数学常数的多项式表达。

数学猜想生成和猜想验证（包括证实与证伪）共同组成了一个数学发现的闭环：猜想生成是为了从大量数学实践中发现潜在规律，而猜想验证是对这些发现进行证明或证伪。这一过程正是人类发现知识、积累知识的过程。
机器生成猜想、证明（伪）猜想的过程重现了人类对知识的发现和积累过程。事实上，在“猜想证伪”一节中出现的AutoGraphiX猜想就是由一个名为AutoGraphiX的计算机程序生成的。机器自我归纳、自我过滤、自我证明，展现了强大的知识总结能力。有趣的是，这一强大能力很大程度上源于对数据的大批量尝试和检验。这种看似非常简单的策略却产生了强大的智能。