「讲座-Mike Douglas@IAS2025」人工智能在数学与物理学中的应用
视频链接： https://www.youtube.com/watch?v=yuvqVXFVjt0
本次讲座由哈佛大学 Mike Douglas 主讲，深入探讨了人工智能（AI）在数学和物理学领域的应用现状、发展趋势及未来潜力。讲座首先回顾了 AI 领域的快速发展，特别是近年来计算能力的指数级增长和以 AlphaFold 为代表的重大突破，引出了 AI 对科学研究，尤其是理论物理和数学研究的潜在影响。
尽管 AI 在这些领域的应用尚处于起步阶段，但讲座详细介绍了几个当前已经取得成功的范例，包括辅助科学计算、数学数据科学、组合优化以及交互式定理证明。通过这些具体的例子，展示了 AI 如何帮助研究人员发现数据模式、搜索文献、辅助编码、提出猜想，甚至解决复杂的数学问题。
讲座的核心部分着眼于 AI 的未来发展，特别是“数学研究助理”这一概念的提出。Mike Douglas 详细阐述了这类助理的潜在功能，包括但不限于辅助编码、文献搜索、定理证明、形式化以及探索数学概念等。他强调，虽然目前的 AI 技术还无法完全实现这一愿景，但随着语言模型和强化学习等技术的不断进步，这一目标正变得越来越触手可及。
此外，讲座还探讨了一个更具前瞻性的话题——自主数学研究的可能性。通过一个思想实验，引发了对 AI 是否能够在没有人类直接干预的情况下进行数学发现的思考。
最后，讲座总结了 AI 在数学和物理学中的应用前景，并预测在不久的将来，AI 将在这两个领域发挥越来越重要的作用，甚至有可能达到或超越人类顶级研究人员的水平。本次讲座为读者提供了一个全面了解 AI 在数学和物理学中应用的窗口，并对未来的发展趋势进行了展望，适合对人工智能与交叉学科研究感兴趣的读者阅读。
讲座框架与要点
演讲主题：人工智能在数学与物理学中的应用
├── 开场介绍 (0:15-0:34)
│ ├── 介绍演讲者 Mike Douglas
│ └── 晚餐邀请
├── 引言：人工智能的快速发展 (0:34-1:30)
│ ├── 人工智能领域发展迅速，逼近通用人工智能 (AGI)
│ └── 关注 AGI 对数学和科学研究的影响
├── 人工智能在科学中的应用现状 (1:37-3:28)
│ ├── 人工智能并非全新领域，影响力与计算能力相关
│ ├── 计算能力指数级增长，推动人工智能进步
│ ├── AlphaFold 作为潜在影响力的例证
│ └── 展示人工智能性能指数增长图表
├── 人工智能在理论物理和数学研究中的应用现状 (3:28-4:35)
│ ├── 目前影响力较小
│ └── 已有应用：
│ ├── 发现数据模式
│ ├── 搜索文献
│ ├── 辅助编码
│ └── 提出猜想
├── 人工智能研究助理的愿景 (4:35-5:32)
│ ├── 长期愿景：
│ │ ├── 协助实验、计算、解决问题
│ │ ├── 改进数学和科学搜索引擎
│ │ ├── 易用的交互式定理证明
│ │ └── 推动科学发现
│ └── 探讨愿景尚未实现的原因，认为无根本障碍
├── 2025年后可能取得的突破 (5:50-6:19)
│ └── 对比五年前的预测和现在。
├── 当前成功的范例 (6:26-8:19)
│ ├── 介绍几个成功范例：
│ │ ├── 辅助科学计算和数学数据科学 (6:49)
│ │ ├── 组合优化 (6:57)
│ │ └── 交互式定理证明
│ └── 计算机象棋的例子，预测数学研究的类似发展
├── 机器学习简介 (8:19-12:52)
│ └── 简要回顾基本概念和技术：
│ ├── 参数化模型（如神经网络）
│ ├── 监督、自监督、强化学习
│ ├── 目标函数和优化
│ └── 数据集、泛化、可解释性
├── 机器学习在科学计算中的应用 (12:59-19:12)
│ └── 举例说明应用：
│ ├── 求解偏微分方程
│ ├── 数据驱动模拟和降阶模型
│ ├── 子网格建模（天气预报、气候模型）
│ ├── 优化大型强子对撞机
│ ├── 神经科学建模
│ ├── 流体动力学数学理解
│ └── 寻找纳维-斯托克斯方程奇异解，计算 Calabi-Yau 和 G2 度量
├── 数学数据科学 (19:19-24:31)
│ ├── 介绍概念和应用：
│ │ ├── 分析数学数据集模式，发现猜想
│ │ └── 定义“数学数据集”（柏拉图数据集）
│ └── 举例说明应用：
│ ├── L 函数系数中的“murmurations”
│ └── 结不变量之间的新关系
├── 约束优化和约束满足 (24:37-30:31)
│ ├── 介绍问题及机器学习应用：
│ │ ├── 可满足性问题 (SAT)
│ │ └── NP 类问题
│ └── SAT 求解器在数学问题中的应用：
│ ├── Szemerédi 猜想
│ ├── Cap Set 问题
│ ├── 空六边形数问题
│ └── Andrews-Curtis 猜想
│ └── 语言模型生成程序解决 Cap Set 问题
├── 交互式定理证明 (30:38-38:01)
│ ├── 介绍概念和应用：
│ │ ├── 证明形式化，计算机验证
│ │ └── 已验证的著名定理：四色、Feit-Thompson、开普勒
│ └── Lean 定理证明器及其应用
│ └── 讨论使用 Lean 的困难，以及人工智能简化证明的努力
├── 语言模型及其在定理证明中的应用 (38:07-44:04)
│ ├── 介绍语言模型：
│ │ ├── 统计语言模型、Transformer 模型
│ │ ├── 大文本语料库训练
│ │ └── 生成文本、回答问题、解决问题
│ ├── 讨论推理、长链推理、处理错误的挑战
│ ├── “系统1”和“系统2”思维模型，训练与推理时间权衡
│ └── 强化学习与语言模型结合，人类反馈、过程奖励、Lean 验证器
├── 语言模型在文献搜索和自动形式化方面的应用 (44:10-47:17)
│ ├── 文献搜索和总结示例
│ └── 自动形式化进展
├── AlphaGeometry 和指数级进展 (47:17-53:11)
│ ├── AlphaGeometry 解决 IMO 几何问题
│ ├── 重温人工智能性能指数增长图表：
│ │ ├── 衡量人工智能进展的指标
│ │ ├── 与计算机象棋进展比较
│ │ └── ELO 评分系统及对应关系
│ └── 预测人工智能在数学研究中的类似增长
├── 对数学研究助理的展望 (53:17-59:46)
│ ├── 具体功能：
│ │ ├── 辅助编码、文献搜索、定理证明、形式化
│ │ └── 探索数学概念、寻找反例、估计
│ ├── 提出“工作流”概念
│ └── 强调可靠性、可解释性、与现有工具集成
├── 关于自主数学研究 (59:54-1:03:05)
│ └── 讨论可能性，思想实验，当前架构和训练方法的不足。
└── 总结与结论 (1:03:13-1:06:11)
├── 总结机器学习在数学和物理中的范例
├── 强调交互式定理证明的重要性
├── 重申人工智能性能指数增长
├── 预测未来两三年出现“数学研究助理”
├── 预测人工智能在数学研究中达到/超越人类水平
└── 呼吁积极迎接机遇和挑战
讲座基本信息
普林斯顿高等研究院高能理论研讨会
主题：人工智能在数学和理论物理学中的应用：现状与展望
演讲人：Michael Douglas
单位：哈佛大学
日期：2025年3月17日
简介：人工智能的进步正在加速，现在行业领导者们预计将在未来 2 到 3 年内出现“通用人工智能”（AGI）。虽然这令人难以置信，但我们必须为这种可能性做好准备。我们可以从之前计算机超越人类的事件中吸取一些教训，例如在国际象棋领域。我们将讨论数学Copilot和自主数学发现系统的概念性研究。在我看来，这些系统很可能在未来几年内变得真正有用。
讲座实录
开场介绍 (0:15-0:34)
大家好！非常高兴今天能邀请到我的老朋友 Mike Douglas 来做客。他将为我们带来关于人工智能在数学和物理学中应用的精彩演讲。今晚我们还将带 Mike 去共进晚餐，如果有兴趣参加的朋友，请与我联系。我们大约晚上 6 点在 Bloomberg Lobby 集合。非常感谢大家！对我来说，回到这里总是非常愉快的，我在这里有很多老朋友。
引言：人工智能的快速发展 (0:34-1:30)
我一直关注着人工智能这个领域，以及我们如何将其应用于数学、物理和科学问题。如果你读过报纸，或者体验过最新的模型，你就会知道这个领域正在飞速发展。以至于这个行业的许多领导者都表示，我们应该期待在不久的将来出现他们称之为“通用人工智能”(AGI) 的东西。那么，这对我们这些研究人员意味着什么呢？我将重点关注这对数学和科学研究意味着什么。
人工智能在科学中的应用现状 (1:37-3:28)
我们已经看到了这种进步，也看到了其中一些应用。当然，人工智能并不是一个新领域，自上世纪以来，这个想法就一直存在，并且一直在发展。实际的影响很大程度上取决于用于实现它的计算机的性能，而这种性能几十年来一直在呈指数级增长。首先是芯片特征尺寸的缩小，然后是你可以购买的计算机的性能。这是一个主要原因，但不是唯一原因，解释了为什么人工智能的进步持续且呈指数级增长，并且在一段时间内将继续保持指数级增长。我们开始看到它在科学研究的许多领域产生影响。当然，我认为真正衡量其潜在影响力的“黄金标准”是 AlphaFold，它在蛋白质折叠方面的突破确实彻底改变了结构生物学领域。而且，人工智能在实验中也得到了广泛应用，你肯定在用不同的方法。你可能也在使用机器学习工具来分析数据，稍后我会回到这一点。这里有一张图，量化了这种指数级进步的概念。这是一个对数坐标图，你可以看到各种衡量进步的指标，都呈现出相当稳定的增长趋势。我会回过头来解释这些指标是什么，它们是衡量进步的不同方法。但到目前为止，情况一直是这样。
人工智能在理论物理和数学研究中的应用现状 (3:28-4:35)
那么，到目前为止，人工智能对理论物理研究、数学以及你们许多人所研究的领域产生了什么影响呢？它的影响还不是很大。我想你们很多人肯定都尝试过人工智能，有些人可能正在使用它。我想举手示意一下，谁在研究中实际使用过人工智能？好的，有一些人，但不是大多数。所以它有它的用途，我稍后会讲到。本次演讲的一部分将是对当前技术水平的综述。你可以用它来发现数据中的模式，搜索文献，寻找例子，比如猜想，还可以辅助编码。你们很多人读过论文，也尝试过，你会发现编码实际上是这些最新语言模型的强项之一。
人工智能研究助理的愿景 (4:35-5:32)
但是，让我们来看看人们多年来提出的想法，因为这些想法也不是全新的。我们应该拥有某种人工智能研究助理，来帮助我们，无论我们是什么类型的科学家，进行实验，做计算，为我们解决简单的问题等等。它还应该拥有非常好的数学和科学搜索引擎，我认为这已经开始成为现实了，稍后我会回过头来谈这个。它还应该提供易于使用的交互式定理证明，特别是如果你是一位数学家，你可能听说过像 Lean 这样的技术，可以用来验证计算机上的证明。但是如果你尝试过使用它，你会发现学习曲线非常陡峭，它并不容易使用。我们还希望计算机能在科学上有所发现，稍后我会论证，你不会是唯一一个这么想的人。
那么，为什么这些事情还没有发生呢？是否存在某种根本性的障碍，使得这些事情比我们目前看到的更难？我的猜测是否定的，不存在这样的根本性障碍。但这是否意味着这些事情将会发生？这正是本次演讲要探讨的问题，也是我一段时间以来一直在思考的问题。事实上，我大约五年前在这里做过一个类似主题的演讲，只不过那时技术还比较原始。内容包括幻灯片等等，所以将我现在所说的与我当时所说的进行比较会很有趣。
2025年后可能取得的突破 (5:50-6:19)
将现在所说的与五年前所做的预测进行比较。
当前成功的范例 (6:26-8:19)
这里有一些我认为到 2025 年真正有用的范例，人们，包括数学家和物理学家，正在使用它们来解决各种问题。我们在哈佛大学 CNSA 举办了一个关于这个主题的项目，有很多人参与了这种类型的合作。讨论了很多关于学习如何辅助科学计算、数学数据科学、组合优化和交互式定理证明等方面的内容。这些都是有用的东西，我不会详细介绍，但会向你们展示人们现在正在做的事情。它们都是在 2025 年之后出现的，并且在现阶段都非常有用，可以帮助你解决问题，但它们是渐进式的。然而，我们面临着指数级的进步，我们可以回顾过去，看到有些活动，你可以称之为“智力工作者”所做的活动，确实经历了从“还不错”到“超越人类”的过程。当然，一个非常著名的例子是计算机象棋。在 1994 年，计算机象棋的水平可以和象棋大师们一较高下，互有胜负。1997 年发生了著名的“深蓝”事件。到了 2004 年，即使是一台个人电脑上的象棋引擎也能击败最优秀的棋手，虽然不是每次都能赢，但胜率非常高。非常快地，计算机象棋就进入了超越人类的阶段。这是一个计算机从某种程度的胜任能力发展到超越人类能力的例子。这种现象可以用我之前展示的那种图表来量化，稍后我会回过头来量化这一点。这让我相信，我们正处于数学研究进入类似阶段的边缘。
机器学习简介 (8:19-12:52)
接下来，我将非常简要地回顾一下机器学习。你们中的许多人可能已经看过这些材料，但将它们总结起来可能会有用。机器学习涉及统计学、计算机科学、应用数学等领域。其中有一些典型的、不是全部但非常标准且广泛适用的问题。其中一个主要工具是参数化模型，例如著名的前馈神经网络。从数学的角度来看，你可以说它是一个大型的参数化函数集合。我有一些输入，比如高维实空间，和一些输出空间。我有很多这些函数的参数，很容易写出这些参数化的函数族。这里是一个标准的前馈神经网络，我有输入，有这些线性变换（矩阵），还有这些激活函数。这里有一些常用的非线性函数，作用于每个分量，比如 tanh 或 ReLU。我将这些组合起来，就得到了这个非常通用的函数逼近器。我可以调整参数来逼近实践中出现的许多函数。
然后，使用这些函数逼近器，我们可以学习一个函数。这在机器学习中非常常见。例如，要训练一个模型来识别猫和狗，输入将是图像，编码为每个像素的强度或颜色值的实数。输出可以是 1（如果是猫）或 -1（如果是狗），或者是你认为它是猫的概率。令人惊讶的是，识别和分类图像的问题可以用学习这个函数的方式来有效地表达。这就是监督学习。
一般来说，自监督学习就是给你一组输入，然后你学习这组输入的概率分布。强化学习则是当你没有明确的输入数据集或要预测的目标时使用的，例如下棋。在游戏结束时，你会发现所有的学习都必须基于这个结果。
然后，所有这些工作都可以通过定义一个明确的目标函数来描述系统在执行这些任务时的表现，例如你拟合数据的程度。然后，你可以通过梯度下降或类似的方法来优化这个目标函数。这就是这项技术的核心，当然，它在 GPU 上得到了非常高效的实现，并且有非常巧妙的软件。
还有很多概念、技术和技巧与之相关，例如数据集的重要性，拥有干净的数据，以及理解这些函数何时可以泛化到原始输入数据之外的内容。人们对这种情况的发生方式只有部分了解，例如，为什么具有大量参数的模型能够泛化。即使在 15 年前，如果你问统计学家，他们对神经网络的看法是什么，他们可能会说，这些模型实际上很糟糕，它们参数太多了，肯定会过拟合。这是一个合理的论点，但事实证明它是错误的。
还有这些训练和测试的技术，以及关于哪些模型有效的更多信息。当然，它们适用于某些问题，但也存在各种困难或缺陷。一个著名的例子是，你可以用一个具有数十亿参数的模型来很好地拟合一个经验给定的函数，达到 99% 的准确率。但是，它到底告诉你了什么呢？它可能什么也没告诉你。因此，有一些工具可以用来解释模型，看看你是否能从中提取出人类可以理解的东西。人们通常更喜欢易于解释的模型。
以上非常简要地回顾了这个领域和应用类型。现在，我将简要介绍一下我将要讨论的第一个主题：机器学习在科学计算中的应用。
机器学习在科学计算中的应用 (12:59-19:12)
到目前为止，我相信你们已经看过很多关于这个主题的演讲。机器学习在科学计算中的应用可能包括尝试求解偏微分方程、进行模拟等等。同样，有一些方法可以最大限度地利用机器学习技术。例如，你可以使用神经网络来代替有限元或基函数表示，因为神经网络是一种经过优化的、具有大量函数的机器学习模型。你不需要使用定制的求解器来解决你的问题，只需要将你解决问题的程度表示为一个误差和目标函数，并通过梯度下降来最小化它。这样，你就可以使用所有这些非常高效的机器学习硬件和软件，而工作量相对较小。
最终，你往往不会像传统分析那样，对问题有深刻的理解。传统分析是经过几十年发展起来的，但你仍然可以得到很多好的结果。
另一个在这个领域非常有效的想法是“蒸馏”。你可能有一个大型的模拟数据集，现在你可以让人工智能学习一些特征，甚至生成比实际模拟更简单、更便宜的模拟。
子网格建模是另一种方法。在传统的基于网格的方法中，你会有一个网格，误差的大小由网格间距决定。但是你可以说，为什么要局限于网格呢？我们可以通过模拟很多更小的尺度来模拟更小尺度上的行为。
机器学习在科学和数学中有大量的应用，而且是实用的。例如，它现在被用于天气预报和气候模型，特别是建模的思想。它可能不一定更好，但速度快得多。因此，你可以进行大量的预报，而不仅仅是单一的预报。你可以得到更好的不确定性估计，即预报的分布。
拟合模拟的思想也被广泛使用。在粒子物理学和基础物理学中，它被用于优化大型强子对撞机。神经科学建模也是一个重要的课题。
流体动力学的数学理解是一个有趣的领域。我将在下一张幻灯片中介绍这一点。有一个有趣的项目试图证明纳维-斯托克斯方程是否存在奇异解（如果存在的话）。他们使用机器学习来寻找这些解，然后使用数值解来证明存在一个严格解。
我将在这张幻灯片上稍微介绍一下我们正在进行的项目，我们还没有完成，但这是一个与弦理论家非常相关的主题，即著名的 Calabi-Yau 度量。这是一种平坦的 Kähler 度量，通常是在六维空间中。Yau 在 70 年代证明了这些度量的存在，这成为了弦理论紧化的基础。最近，人们开始对这些度量进行计算机计算，因为它们没有解析表达式，但可以通过数值计算得到。然后，使用机器学习技术，可以得到非常通用且相当准确的数值计算结果。我最近与 Daniel Platt 和合作者一起将这项工作推广到了 G2 度量。有趣的是，这个论证虽然还没有完全完成，但可以转化为一个严格的证明。
数学家有一个定理：如果你能在这样的特殊流形上找到一个没有零点的调和 1-形式，那么你就可以将其提升为一个一维 G2 流形。我们可以想象证明我们找到的数值解满足这些条件，特别是它不为零，这不仅仅是数值精度的问题。
这是该问题的线性、相对简单的版本。目前的项目是尝试对实际存在的 Calabi-Yau 度量进行证明。这涉及到一些技术细节，Yau 的定理大致分为两部分：第一部分是，如果你能证明解在某种精确的意义上足够接近 Ricci 平坦度量，那么你就可以将方程重新表述为一个不动点条件。如果你能证明它确实是某个点附近的不动点，那么就一定存在一个精确的、接近这个数值解的 Ricci 平坦度量。Yau 证明的第一部分是，在对度量几乎一无所知的情况下，证明度量实际上满足这些条件。通过一些初步的论证，你可以得到足够接近的结果，这部分非常困难，涉及到先验估计。但我们的计划是，我们取得了一些进展，基本上采用数值计算，并将其做得足够好，以证明先验估计。然后，你可以严格地证明这些技术，例如，验证数值计算，严格地证明它。这是机器学习用于科学计算并直接产生数学成果的一个例子。
数学数据科学 (19:19-24:31)
这是我的四个主题之一。数学数据科学，顾名思义，就是你有一个数学数据集，你正在寻找数据集中的模式，这些模式可能会启发你提出猜想，然后你可以帮助证明或证伪这些猜想。
那么，什么是数学数据集呢？这个讨论是我们项目的一个主要议题，这是 Duong Le 的工作，稍后我会回过头来介绍他的工作。数学和数据科学的关键在于，数据应该有一个简单的定义，这样如果你发现了什么，你就可以准确地说出你发现了什么。你必须有一个可以证明的精确陈述。从这个角度来看，我们可以定义一个数学的、我喜欢用“柏拉图式”的数据集。它是一些数学对象的集合，比如纽结。有一些定义在这些对象上的函数，通常映射到高维向量空间，表示对象的属性和不变量。然后，必须有一种方法来选择对象的子集，因为它显然是有限的，而且应该相对简单。可能有一些复杂性的度量，比如交叉数，这个数据集包含了所有交叉数不超过 19 的纽结，这个数据集包含了所有导子不超过 500,000 的椭圆曲线等等。但它应该是精确和简单的。可能有一些精确的概率分布样本。这就是你可以说“我发现了这个数据集，我想尝试证明一些东西”的数据集。
这就是机器学习的输入。基本上，我们有这个集合，可能是纽结或其他东西，然后我们对这个集合应用函数 F，就得到了高维空间中的这团点。这就是我们提供给机器学习的内容，它不懂任何数学，但它会寻找模式。
人们发现了什么样的模式呢？这里有一个例子，可能至少目前最著名的一个，叫做“murmurations”。我假设你们中有些人已经听说过这个数论中的概念。这里是椭圆曲线的 L 函数。基于将方程约化到任意给定的素数 p，并计算系数，有一个非常简单的公式，与解的数量有关。然后，如果你做一件以前没有人真正尝试过的事情，但如果你尝试用机器学习来处理这个问题，并将其与 Q 进行比较，这解释了 Duong 和他的合作者是如何做到这一点的。你可以对某个范围内的曲线进行平均，比如导子为 2 的曲线，并对给定素数索引的系数 a 进行平均，比如第一个素数、第二个素数、第三个素数。这里是我们没有做平均的情况，这里有一堆曲线，蓝色表示秩为 0，红色表示秩为 1。你可以看到，你可以区分秩为 0 和秩为 1 的曲线，秩为 0 的曲线在上面。所以有一个信号表明机器学习可以预测曲线的秩。
但是，这里有一种振荡，一开始红色在下面，但最终会振荡并上升，然后继续这样做。他们很惊讶，他们到处询问，所有人都很惊讶。这是一个发现，最近有一些工作，不是针对椭圆曲线，而是针对模形式，证明并了解了这些振荡的来源。这是人类使用机器学习的一个例子，但人类仍然需要组装数据。
在我们研讨会之外，还有一个类似的例子，在模形式系数中发现了“murmurations”。
这是在这个范例中发现有趣结果的另一个例子。这是一篇四年前的论文，由 Alex Davies 和 DeepMind 的研究人员与 Mark Lackenby 等数学家合作完成的。他们使用回归和非监督学习，能够识别出纽结不变量之间的新关系，Lackenby 能够证明这些关系。
这就是数学数据科学的一个例子。我想这些就是我本次演讲要讲的例子。如果有人想打断我，我可以多说一点。
问 (24:04): 这些结果中有任何被证明了吗？
答 (24:10): 那个结果（指结不变量之间的新关系）被证明了。
问 (24:20): “murmurations”呢？
答 (24:25): 有一个结果，我相信是 Melanie Matchett Wood 证明的，她是这里的一位数学家，她已经证明了模形式的“murmurations”的一个版本。
约束优化和约束满足 (24:37-30:31)
好的，第三个主题是约束优化和约束满足。这像是一个很酷的计算机科学主题。你正在寻找满足一大堆离散约束或条件的解。这个问题的典型例子，实际上是定义性的例子，是可满足性问题 (SAT)。给你一个布尔变量列表，这些变量可以是真或假，以及一个大的布尔表达式，比如这个。你必须找到一个变量赋值，使得表达式为真，或者证明不存在这样的赋值。这就是 SAT 问题。
这是 NP 类问题的典型例子，即判定问题。证明不存在解属于另一个不同的类别，称为 Co-NP。这两者之间没有对称性。众所周知，这些问题很难解决，没有通用的方法，人们认为没有通用的方法，可以在多项式时间内解决这些问题。粗略地说，即使是暴力尝试所有可能性，那也是指数时间的，很难做得更好。当然，有更好的算法，但仍然是指数级的。
还有各种各样的问题，比如计算解的数量，找到使真子句数量最大化的赋值，将变量从布尔变量推广到取多个值的变量等等。有很多软件可以解决这类问题。因此，如果你的问题符合这种类型的方案，我们就可以讨论很多这样的问题。
例如，Szemerédi 猜想：一个具有 n 个顶点的图中，最多可以有多少条边，使得不存在四个顶点的环？如果你考虑三个顶点的环，那很简单，但四个顶点的环仍然是一个开放问题。最好的结果是通过 SAT 求解器找到的。
Cap Set 问题：在有限域 F3 上的 n 维空间中，我们有向量。我们想找到最大的集合，使得没有三个向量共线。
空六边形数问题：在实平面上，一般位置（没有三个点在一条直线上）的点集中，点的数量最多是多少，使得存在一个六边形，你可以画出这个六边形，内部没有点。
令人惊讶的是，这个问题已经被证明了。有一个特定的数字来自 SAT 求解器的结果，被证明是这个问题的答案。同样，这个问题结构稍微复杂，但没有明显的方法来解决它。计算机可以解决涉及搜索大量约束的问题。
然后，你可以进行推广，定义我的约束。一个更一般的离散问题的例子是，在一个大的 K 图中找到一条路径。
最近听说的一个例子是 Andrews-Curtis 猜想，它与四维流形拓扑有关。可以表述为：这个无限群的某个图是连通的还是不连通的？
我不会详细介绍，幻灯片可以供大家参考。有一些标准的技术，然后你可以在这里加入机器学习。机器学习可以提供帮助，但通常最好的求解器并不是完全基于机器学习的，但它是用于解决数学和数学问题的计算范式的一部分。
这是我们在项目中研究的一个例子。事实上，最近又有一篇论文发表了，是 FUN-SAT，它也使用语言模型生成函数来解决问题，我稍后会简要介绍。
让我向你们展示这个例子。大约一年前，DeepMind 与 Jordan Ellenberg 和合作者一起使用它来寻找 Cap Set 问题的解。回顾一下，这是在有限域 F3 上的 d 维向量空间中，我们正在寻找最大的集合，使得没有三个向量共线。然后，一个语言模型生成了这个解。这是一个程序，给定一个向量，它会产生一个实数分数。那么，如何使用它来生成集合呢？你只需从上往下遍历，如果一个向量可以被添加到集合中，你就将它添加到集合中，然后继续下一个向量。你检查它是否违反了“没有三个向量共线”的条件。如果违反了，你就把它扔掉；如果没有违反，你就将它添加到集合中，并继续遍历列表。因此，你已经将定义集合的问题简化为生成一个向量的函数。然后，这个 Python 程序，为 8 维情况生成了这个破纪录的结果，是由一个 Google 语言模型生成的。
这个项目被编程为提示式的。你可以和它玩游戏，你给它一个列表，这个列表包含了一些这种类型的程序，它们是问题的候选解。它们生成向量的函数，并产生分数和排名。然后，你给它一个这些程序的列表，然后你说，给我生成另一个像这样的程序。它会这样做，然后你评估新程序以及其他程序，并保留最好的。这有点像老式人工智能中的进化算法，但使用了生成式方法，从一个程序群体中生成更小的程序。
这是一个有趣的、基于机器学习的组合优化例子。当然，最近发表的这篇论文也对其他一些问题进行了类似的研究。
交互式定理证明 (30:38-38:01)
好的，这是我的第四个回顾主题。我试图向你们展示我认为到 2025 年最成功的范例是交互式定理证明。
这又是一个历史悠久的思想，在 20 世纪初得到了精确的表述。这个思想是，证明可以被归结为公式，只需要检查用形式语言写出的步骤，并应用有限的规则列表来推导，看看你是否能将其简化为某个陈述。
著名的哥德尔不完备定理表明，这个过程可能非常漫长。
在实践中，证明 1 + 1 = 2 据说需要 10 页。这个问题最终得到了解决，它与每个计算机程序员和软件工程师面临的问题非常相似，即程序是庞大而复杂的。我们有所有这些工具，我们有计算机科学工具来构建这些程序，生成库，并在以前的工作基础上进行构建。此外，数理逻辑和框架方面也有重要的发展。你可以使用集合论，但在所有实际系统中使用的都是类型论，我将更多地谈论依赖类型论。这些也大大简化了问题。
有一些旗舰级的、复杂的、困难的定理已经通过这种方式得到了验证。四色定理不仅仅是计算验证了许多图，而且这个检查实际上已经通过一个定理证明器进行了验证。这是在 2000 年代在法国完成的。有限群论中的 Feit-Thompson 定理，Thomas Hales 关于开普勒猜想（三维空间中球体的最密堆积）的著名证明，也通过 Emery-Tucker 证明器进行了验证。LA 系统就是其中的一个例子。
一个引起了最多关注并且我认为目前是最好的系统叫做 Lean，现在是 Lean 4，第四个版本。有一个相当大的社区，可能你们中的许多人读过 Quanta 和其他地方的文章，有数百名数学家正在开发这个系统，构建它的库，目前已经涵盖了几乎所有的本科数学课程，以及一些研究生课程。最近的一些成就，可能最著名的是 Peter Scholze 的凝聚数学基础引理的验证，以及与 Dustin Clausen 合作的液体数学。
我猜这是他开发的相当抽象的框架，并证明了他们的基础引理。他认为这是一个证明，但它是一个不够直观的证明，以至于他想进行检查。所以他联系了社区，并问他们，你们声称能够用计算机检查定理，你们试试这个。他们接受了挑战，在三个月内，他们就能够解决他最担心的问题。在假设这个和这个成立的情况下，我们可以证明那个。在大约一年半的时间里，一个由大约 10 个人组成的团队，我猜他们是兼职工作的，能够从逻辑基础开始完全证明并验证这个引理。这可能是这些计算机定理证明器解决实际数学家提出的问题并真正想知道它是否正确的第一个例子。这是一个里程碑。同样，还有许多其他重要的、有趣的演示，证明了这种方法的力量。Kevin Buzzard 和 Imperial 还有一个非常雄心勃勃的项目，试图证明数学的很大一部分。
坦率地说，目前的情况是，这是一件很难学习的事情。这就是为什么只有数百人而不是数千人在使用它。你需要一年的学习才能熟练掌握它。
问 (34:39): 对于这种技术（交互式定理证明），你必须将现有的证明解释成这种语言吗？
答 (34:46): 这就是为什么你可以做到这一点。你也可以开发一个新的证明，但人类负责提出证明，计算机负责验证。我将举几个例子，也许会有助于理解。
这叫做引理，这很容易理解。从 P1 到 P3 的距离的平方等于从 P1 到 P2 的距离的平方加上从 P2 到 P3 的距离的平方，如果它是一个直角三角形。然后是证明，以及对更一般角度情况的推广。
为了简化一点，这些定理和定义的陈述实际上非常容易理解。如果你去看看这些东西，这些证明真的是，我不想说“乱七八糟”，但我只能说，它们非常计算机化。它们使用这些，虽然有一定的系统，但你需要大量的知识和结构才能写出明确的操作，你可以使用这些操作来重新排列公式，引入公理等等，来证明它。我认为你会希望定理证明的最终解决方案不需要你写或读这样的东西。
那么，一个解决方案是，人工智能可以写这些证明，为什么不呢？这是另一个计算机科学中的核心主题，形式化方法。有一个相当成功的方法，目前最成功的方法叫做 Sledgehammer，它存在于一个叫做 Isabelle 的系统中。Isabelle 是一个竞争系统，它有其他缺点，但在这一方面它更好。有一种技术，高阶逻辑，你需要它来表达相当一般的数学，允许你量化任何函数，这是非常通用的。一个简单得多的问题是，你有量化和变量，但你只能量化集合，而不能量化函数。你可以用这种方式表达数学中很大一部分有趣的内容，但你不能表达实数。你需要谈论序列，无限序列，或者某种构造方式。所以这不是你可以在一阶逻辑中表达的东西，你必须量化那个序列。另一方面，基于事实证明，你有你想引入的所有引理的列表，以及你想证明的陈述，你实际上可以找到一种非正式的翻译，将其转化为一阶逻辑，引入所有这些额外的符号，来表示问题中可能出现的所有对象。然后，一阶逻辑证明实际上是一个容易得多的计算问题。这已经存在于 Isabelle 中，更容易阅读，并且正在为 Lean 开发。它可能在未来一两年内出现，这表明这些困难并不是这个概念固有的，只是它的水平还不能令人满意。
语言模型及其在定理证明中的应用 (38:07-44:04)
好的，这就是计算机科学的方法。然后，人们非常努力地尝试使用机器学习和人工智能来做这件事。你可以把它当作一个强化学习问题，假设进行证明的步骤就像在玩单人纸牌游戏一样。如果你证明了，你就赢了。所以我们将使用 AlphaZero 类型的技术。这已经被尝试过了，它有一定的价值。最近的工作将强化学习与语言模型结合起来。
现在开始谈论语言模型。Go Pro 确实加速了这个过程。我们不需要详细阅读这个，但它类似于“完成平方，将这一项移到那一侧，引入这个引理”，然后验证证明。
问 (38:58): 我用过一个可以接受自然语言命令的(Lean) 界面。它会被 Lean 取代吗？
答 (39:09): 这正是我们现在要讲的内容，你说得对。这就是我们想要的。(指用AI、自然语言的方式进行交互式证明)
这里是对语言模型的非常简要的回顾。我们有这些统计语言模型，给定一个单词或标记的字符串，它可以预测下一个单词的概率分布。Transformer 是一种非常好的模型，似乎非常擅长这类任务，并且可以在大量的文本语料库上进行训练。从某种意义上说，你可以使用从互联网上抓取的任何内容。你一次处理一个单词，并预测下一个单词。这个单词出现了，这就是一个样本，来自于经验概率分布，然后它会一直这样做。令人惊讶的是，它不仅能生成貌似合理的文本，而且能生成越来越合理的文本，其中可能包含你提出的问题的答案，解决方案等等。这显然是近年来人工智能最重要的进展。
毫无疑问，你玩过 ChatGPT，你可能听说过 ChatGPT 的问题，这是一两年前的技术。它会出现幻觉，无法进行长时间的论证。人们正在这方面取得相当大的进展，这就像我们现在所说的那样，仍然是人工智能领域的一个重大研究课题，要让系统能够进行推理，解决需要更长链条的问题，或者对错误不容忍的问题。这些问题可能需要提出假设，然后证伪它，回溯并尝试其他方法。人们已经取得了很大的进展。我将向你们介绍一些概念性的方法，人们用这些方法来思考这个问题。
一种方法是类比于认知过程理论，Kahneman 提出的“系统1”和“系统2”思维模型。人类的思维被建模为一个“系统1”，它可以立即对问题做出反应，识别图像等等。从某种意义上说，这类似于语言模型所做的事情，它立即产生下一个单词。然后，如果是一个需要你退后一步、制定计划、思考或假设的问题，那么“系统2”就会介入。这需要有意识的努力，感觉像是一种努力。心理学中有各种各样的实验来区分人类思维中的这些东西。从这个角度来看，目标是说，到目前为止，语言模型具有“系统1”的功能，现在我们必须赋予它“系统2”的功能。
我们取得了一些成功。人们谈论的另一个概念是训练时间和推理时间之间的权衡。基本上，这个想法是，与其让它只生成下一个单词，不如给它更多的时间来做更多的事情，来评估下一个单词，也许可以回溯。它可能需要生成一个合理的论证路线，然后由于某种原因决定放弃，并继续另一条路线。这也可以量化为一种权衡。
很多这方面的工作都是专有的，这是许多实验室的竞争优势。著名的 DeepMind 在他们的论文中比 OpenAI 更开放。很明显，DeepMind 和其他公司都在使用强化学习，因为如果你想让模型给出问题的正确答案，你不能逐字逐句地判断它，你必须看答案，并判断它是否正确。这就是强化学习的定义，你会在之后得到奖励，然后你必须将其反馈回去，并弄清楚你采取的各种行动中，哪些导致了成功或失败。因此，这就是强化学习技术。
但是，信号可以基于各种各样的东西。有一种著名的技术叫做“通过人类反馈进行强化学习”。许多公司会给出 AB 测试的例子，比如，这里有两个答案，哪个更好？人类会坐下来判断，这个更好。然后，他们会训练另一个模型来概括这一点，形成一个训练信号。还有一种叫做“过程奖励”的方法，你不一定检查结果，但你会说，至少它看起来像是一个合理的论证，第一句话，第二句话依赖于第一句话等等。这很有帮助。当然，如果你正在生成像 Lean 语言这样的数学证明，你可以将其输入 Lean 验证器，并直接获得信号：这个证明是正确的。这就是“黄金标准”，这也是人工智能研究人员对这个应用领域如此感兴趣的原因之一。
语言模型在文献搜索和自动形式化方面的应用 (44:10-47:17)
这里有一个例子，是 OpenAI 和 DeepMind 的研究成果，几个月前发布的。这是第一个这样的语言模型系统。
午餐时，我们谈到，一两年前，你输入一个文献搜索，一个你感兴趣的问题。这里，我问的是，告诉我一些关于超对称的实验搜索的信息，如果我们有一个 100 TeV 的对撞机，会发生什么？弦理论对此有什么看法？
一两年前，这完全是浪费时间，你最好自己去找一篇综述文章。但现在，同样的系统会产生一个相当不错的答案。它花了大约 10 分钟，我不会说我 100% 检查了它，但这是我了解的主题，其中很多内容显然是正确的，它给出了正确的参考文献，这对于进一步研究来说是一个非常有用的起点。这已经成为我进行文献搜索和查找最近论文的首选工具。我知道这个领域的一些文献，所以我可以将它与我所知道的文献进行比较。
问：(45:41)（关于语言模型给出的结果）它提到 CMSM (紧凑μ子螺旋管) 是一个可以忽略它的理由吗？
答：(46:00) 这是一个很好的理由忽略它。
问: (46:10) 不管怎样，这些是（语言模型给出的）参考文献引用吗？
答: (46:13) 是的，你可以点击这些东西，并得到它引用的论文。它不是 100% 准确，但与一年前相比，这是一个巨大的进步。
这是一个自动形式化的例子。这里有一个简单的问题，这里是如何在 Lean 中形式化它。这里是系统在这方面取得的进展，通过各种方法，在这些基准测试中。这里是 2021 年，当这个问题被提出时，大约 20% 的系统能够做到这一点。然后，计算机科学领域的人们会竞争，让系统在基准测试中表现得更好。这些是那些没有表现得更好的系统。到目前为止，最先进的系统已经达到了 60% 以上的水平。所以，这是一个稳定的进步，这就是人们看待这些事情的方式。
这是一个自动形式化的例子，将非正式数学转化为形式化数学。
问: (47:05) (关于自动形式化的图表）这是正确率吗？
答: (47:11) 是的，所以 miniF2F 是一组几百个这样的问题，这是正确完成的百分比。
这里是另一个例子，这是 AlphaGeometry 和 AlphaProof，来自去年夏天。AlphaGeometry 在解决 IMO 几何问题方面达到了获奖水平。
我希望我们能在秋季邀请到主要作者来做一次演讲。如果你关注这些事情，你会知道还没有关于它的论文，我也不知道，但他计划为我们做一次演讲。
这是所有这些方面的一个例子。现在，让我们继续。
AlphaGeometry 和指数级进展 (47:17-53:11)
这是最先进的技术。现在，让我们回到这张图，它说明了指数级的进步。
这些东西是什么呢？好的，红点。蓝点是 ImageNet，这是其中一个基准测试。这是一个指数，只是针对那个基准测试的。基本上，每次有人做得更好，你就会取改进的比例，即新旧性能之比减 1，然后你把它加起来，一直加下去。它大致相当于一个逻辑函数，或者说指数关系。然后，使用数百个基准测试，这个指标来自于这里，但有数百个这样的基准测试。我的合作者 Sergey 和我开发了一个指标，它结合了许多基准测试，并跟踪了人工智能领域的整体进展。这就是这些红点所表示的。你可以看到这种相当稳定的指数级增长。
这个性能指标基于改进的程度。例如，从 50% 提高到 95%，相当于 5% 的错误率，这就像性能提高了 10 倍。按照这种衡量标准，自大约 2010 年这些基准测试开始以来，人工智能的性能一直在呈指数级增长，大约每两年半或三年翻一番。
这些线是更传统的衡量指标，基于论文和专利数量。经济学家过去可能会用这些指标来衡量这个领域的进展。
这个绿色的是什么？这个绿色的是计算机象棋。计算机象棋，当然，我们看到了所有这些进步。如果计算机不断进步，那么它们必须变得更好。我们如何看待这一点呢？这里有一个领域，这种情况已经发生了，早在 90 年代，我认为是 1994 年。
有一个非常客观的评分系统，叫做 ELO 系统。它有一个简单的数学定义。基本上，它是概率性的，你比较两个棋手，你想描述棋手 1 击败棋手 2 的概率。基本上，400 点的 ELO 优势相当于胜率提高了 10 倍。
我们有这个相当客观的衡量标准，人们已经使用它很长时间了。所以我们对有多少人具有这些不同水平的能力有一个相当好的了解。这是 2015 年国际象棋联合会的数据。
从 2200 分开始，这个人可能会参加锦标赛，可能准备好赢得比赛，成为一名大师，这是基于赢得锦标赛的。在法国，大约有 5000 名这样的棋手。一直到 2800 分，这是最优秀的棋手的水平，在 2015 年，大约有 40 名。中间的水平是国际象棋大师，大约在 600 分的范围内。
现在，这条绿线是想对计算机进行类似的衡量。有一些人，特别是瑞典象棋计算机协会 (SSDF)，他们从 80 年代开始就通过让象棋引擎相互对弈来对它们进行排名。所以他们可以非常稳定地跟踪这一点。这就是这些绿点所表示的。它确实非常稳定，斜率大致相同。这些是人工智能，这是在深度学习之前，不是人工智能的进步，而是当时最好的象棋引擎，现在是个人电脑。同样，性能翻倍。
ELO，这是 ELO 的线性坐标，正如我所说，ELO 400 分相当于性能提高了 10 倍。
问：这里有一个不连续性？
答：是的，我们没有深究，但我认为他们当时更换了个人电脑。他们每隔几年就会升级他们的个人电脑。他们在他们的网站上说了这一点。我们没有试图去查证，我们只是采用了他们的数据。总的来说，情况是，有一个非常稳定的进步，每年大约 54 个 ELO 点，斜率与此相匹配。ELO 和 FRenchmark 性能之间存在典型的对应关系，具有相同的斜率。这导致了一个明显的猜想：人工智能在做其他事情方面的进展也可以遵循同样的进程。如果一台计算机能够在某种程度上达到候选大师在象棋方面的表现水平，并将其转化为其他任务，比如数学或物理研究，那么大约每两年，它的水平就会沿着这个等级下降。12 年后，它将达到人类顶级研究人员的水平。这就是我已经有的想法。
这比我之前想的要量化得多。
这大致类似于象棋的历史，我认为这种指数级的增长在许多人的脑海中都有，但你可以更具体地说明这一点。这就是我将要提倡的。当 Sam Altman 和 Yann LeCun 谈论 AGI 时，他们不是在谈论这个，他们是在谈论这个。我们谈论的是一个有用的助手系统，至少值得你把你的数学问题交给它，有时它能够为你做一些有用的事情，但不是超级人类。我相信，基于前面的讨论和我所想的一切，这可能在两三年内实现。然后，我们将面临这种类型的进步。
问 (54:06): ELO (评分系统) 主要跟踪计算能力吗？
答 (54:13): 我的意思是，基本上是的。论文中有另一张图，展示了计算机的指数级增长，这不仅仅是摩尔定律，还有人们在计算机上花了多少钱。对于这些人来说，他们只是在使用个人电脑，所以他们不是……但大致上是的。在某种意义上，这些东西以对数方式跟踪计算能力，因为 ELO 实际上是在这个指数坐标系中。
对数学研究助理的展望 (53:17-59:46)
那么，这意味着什么呢？我说，可能在两三年内，对我们来说，AGI 将是这个数学研究助理。那么，什么是数学研究助理呢？这又是人们已经提出了一段时间的想法。我找到了 Jerry Sussman 的一篇文章，他是人工智能的先驱之一。在 80 年代，他提出了“动力学家工作台”的想法。他非常喜欢天体力学，与 Jack Wisdom 合作。这将是一个帮助在常微分方程（比如天体力学）中进行计算机实验的东西。在那个时候，这需要大量的编程，但现在它开始变得触手可及。
所以有这样一个愿景：我们可以和它交谈，就像我们和 ChatGPT 交谈一样，进行研究。这绝对是一个有效且非常有价值的助手功能，但还有许多其他功能。
辅助编码是其中之一。如果你关注这方面的进展，你会看到这是如何发展的。这显然是研究的一个方向。直接的编码就是写出这些形式化的证明，以及其他语言，还有反向的过程，即将形式化的证明转化为非形式化的证明。这方面还没有达到 99% 的成功率，但已经达到了 60% 左右的水平。我们有理由相信，这已经走上了可以预测进展的轨道。人们相当合理地预测，在不到五年的时间内，系统将能够很好地处理自然语言的详细描述，并将其转化为 Lean 语言。
语言模型并不是万能的，它不擅长检查详细的计算和论证。因此，即使是超级智能的语言模型也可能使用 ITP 来实现它自己的目的。但这是逻辑部分，我们对它更了解。
然后，还有许多其他方面，在数学和物理中写作和研究，还没有被形式化。这里有一些我与之交谈过的人，他们试图发展这些方面，因为这不是最前沿的东西。助手可以为我们做什么？我们应该如何表达这一点？我们应该如何训练模型，或者设置一个基准测试来让它做到这一点？
“工作流”是其中一个例子，即一系列操作。比如在这个动力学家的例子中，这是我的方程和初始条件，现在我可以使用所有这些方法等等。我想看看它在接下来的 10 年里的表现，我想得到相空间的某种图像等等。可以陈述总体的目标，以及问题和解决方法中的许多变化。这不是一个编程问题，不是执行一个算法，它比 AGI 要简单。这可能是系统可以做的非常有价值的事情。
同样，你可以看看人工智能在文本和代码方面的应用，你会得到其他想法，了解助手可以在哪些层面上帮助你，比如动机、例子和反例。通常是特定的定义，从某种意义上说，它们只是定义，但它们有很好的动机，因为它们证伪了这个有趣的分类，或者其他类型的估计。
同样，如果你深入研究计算机科学分析，有很多方法可以用自然语言来思考这些事情，有时形式化是有用的。
我认为可靠性是一个限制因素，事情会出错。你总是可以提出一个长度为 1 的论证，但这只是一个限制因素。你需要一些东西，你不希望它做所有的计算，你应该能够使用工具。
这是一个明显的共识，这是我们的人工智能共同科学家的一个例子。这是在生物医学领域，不同的问题，你需要面对大量的文献，所以很难做任何实验，但这是一个真正的研究项目，但类似的事情，即使是试图具体化……我不想花太多时间在具体化细节上，因为这是人们现在正在试图弄清楚的事情，因为人工智能正在改变，使许多事情比以前更容易，也使一些事情不像以前那么容易，也许有些工作不值得做。这就是我们今天面临的挑战，有了这些新的能力，你如何最好地利用它们来产生最大的效益，为你的研究提供帮助？
关于自主数学研究 (59:54-1:03:05)
假设你想反驳这一点，我想反驳的一点是，尽管要求计算机开始做某方面的研究是非常合理的，但……
“murmurations”呢？
那是人类使用计算机，人类设置了数据，然后使用数据科学。自主性肯定意味着它设置了数据，然后指出……至少，在他的列表中的第一或第二位是，看看这个，这真的很有趣。它不是人类浏览 100 个项目的列表，然后说，啊……
我认为这是一个目前合理的说法。你可以进行各种各样的有趣测试，这些测试可能比让计算机真正进行数学研究更容易，这就像人类一样。作为一个有趣的、目前只是思想实验的东西，但人们可以研究的一个想法是，让计算机拥有大约 1800 年代人类数学家的知识。我们知道在那之后有一些重要的发现，比如黎曼几何。计算机能够做出这些发现吗？我认为，目前没有任何系统能够做到这一点，但这并不意味着存在某种障碍，某种原因导致它永远无法做到。我认为答案是否定的，这只是超出了目前的能力范围。
我在另一个地方做过一次演讲，是在网上，是关于这个主题的。同样，有一些探索性的工作，但还没有真正得到重视，但我认为它现在已经触手可及。我想提一下我的朋友 David McAllester，他从现代人工智能的角度出发，对这个问题进行了思考。
是的，这是一个有效的反对意见，不像我说的其他大部分内容，我们有点说，计算机正在从接近零的能力发展到潜在的超越人类的能力。这听起来有点疯狂，但另一方面，也有一些非常疯狂的事情发生了，比如写关于素数有无穷多个的诗。你们可能都见过 ChatGPT 做出这样的事情。我不是说这是一个类比，我只是说，有些东西可以从接近零的水平发展起来，如果它依赖于足够丰富和复杂的技能组合，那么在你掌握这些技能之前，它看起来可能像是零。我也认为，假设我们现在的架构，但即使是我们现在的训练数据，这种在问答、问答、问答上训练模型的方式是不够的，这是非常合理的。你显然需要更深入地理解才能做出发现，并意识到为什么它很重要。但我不认为这是一个你无法做到的论证，这是一个你需要不同的训练集、不同的方法来让计算机做到这一点的论证。
总结与结论 (1:03:13-1:06:11)
我的结论是，我回顾了机器学习的各种范例，主要是在数学和物理中的应用。 有很多选择，有用的、渐进式的进步。你当然可以将其与 AlphaGo 进行比较，那是一场革命。革命是可能的，但还没有发生。
交互式定理证明，比如 Lean，非常有前途，显然是计算机化数学故事中可能必不可少的一部分。但是，基础已经存在，但很难使用，它不像 Mathematica 或 SageMath，你可以直接启动它并尝试，并获得有用的结果。
尽管如此，尽管有这些限制，我们仍然处于指数级的增长轨道上。那些被提出的、预计会使指数级增长崩溃的原因，比如摩尔定律，已经失效了，但人们现在花更多的钱来建造他们的计算机，他们投资于它们。我们确实用完了互联网上的训练数据，但我在本次演讲中谈到的大部分数据都是合成数据，是由计算机自己生成的。合成数据没有限制。这些大型数据中心最终显然会有一个限制，但它不会是摩尔定律。
我会这样解释 AGI 将在未来两三年内出现的预测：我们将拥有这些有用的数学助手。许多人将被诱惑使用它作为你工作的一部分，即使它不能解决所有问题，但它是有用的。
然后，我会进行类比，将其与候选大师进行比较。当然，这是一个可以讨论的点，在这一点上有点主观。但我认为这是一个合理的类比，人们谈论的人工智能在其他领域的表现，类比于这种低水平的、但在技能上达到大师水平的能力。然后，我们处于这样的轨迹上，大约五年后，人工智能将与世界各地的顶级研究人员相当，五年后，将跻身最伟大的人类数学家之列。
我认为，这种类型的论证比我之前更有说服力，因为我一直在思考这些问题。我认为，关于这将如何影响整个社会以及我们如何应对，有很多话要说。我认为，在 2030 年之前，对这种情况的回应不是绝望，而是说，我们真的应该有更大的雄心。我们将拥有比以前强大得多的工具和能力，我们应该找到我们真正想解决的重大问题，并开始更多地关注这些问题，因为它们将开始变得触手可及。这仍然非常危险，但也是巨大的机遇。
我就讲到这里。
(1:06:19) 感谢 Mike 的精彩演讲！大家有问题吗？
问答环节
问 (1:06:19): 大量的数学文献都在 PDF 格式的期刊中。是否有任何有组织的努力来扫描和数字化这些期刊？
答 (1:06:27): 嗯，我可能比你更不了解这方面的情况。有些期刊已经被扫描了，但很多还没有。我同意，这是一个动机。我想说的是，在使用这些材料作为人工智能系统的数据时，是否存在版权问题？
问: (1:06:51) 是的，（版权问题）这方面的情况如何？
答: (1:06:58) 我认为最大的问题是大公司，比如《纽约时报》和这些人。我认为，在这些问题得到解决之前，一切都将是不确定的。当然，数学没有那么大的商业价值，所以更容易与特定的出版商达成协议，并更容易地解决问题。
问: (1:07:18) 自主数学意味着什么？
答: (1:07:25) 打开电脑，然后说，做点什么。是的，就是这样，不是像自动驾驶那样，没有人在驾驶。
问 (1:07:30): 我有一个问题。机器学习有一个明显的缺点，即它在数学结构中搜索模式，这些模式是由算法强加的。在这个特定的例子中，这些是平滑函数。换句话说，这是一种美化的拟合，在一个空间中使用平滑函数。例如，如果你将所有关于经典物理学的知识输入机器学习，它永远不会推导出量子力学。同样的事情也适用于天文学，它永远不会推导出相对论，因为它们是一些非常简单的假设。这个缺点可以通过将人工智能与机器学习相结合来克服。人工智能将能够改变和建议机器学习中使用的空间结构。我还没有看到这一点。
答 (1:08:34): 不，我认为这是许多人的想法，这是我在前半部分提出的主题。前半部分主要是机器学习的方法，然后我说，人工智能将如何帮助我们做这些事情？不是全部，但很大一部分是帮助我们更有效地做这些机器学习的事情，并最终自己做这些事情。人工智能可以使用机器学习作为工具。我同意你的说法，我认为这是人们思考的一部分。
问 (1:09:04): 这个房间里的许多人都使用路径积分做出了惊人的发现。你的数学助手需要做什么，才能取代伟大的数学家？
答 (1:09:13): 这是一个有趣的问题。我想说的第一点是，如果你回到五年前，我的印象是，每个人都认为，所有的数学都必须被形式化，才能让计算机真正处理它。现在，我们有了这些语言模型，它们不需要这样做，也可以处理非形式化的东西。所以有一些推理能力，不是做路径积分，而是思考它，但它是存在的。这是其中一部分。因此，我们看到，推理不必完全基于逻辑。另一个答案是，数学家关于形式化的概念和物理学家思考问题的方式之间有什么区别？他们都在进行精确的逻辑论证，只是数学家将其简化为 ZFC，它是一个非常小的数字，也许物理学家的脑海中有 1000 个公理，但仍然是……它可能比我们的更具分析性。这是一个有趣的讨论话题。