“也许很快OpenAI将能证明陶哲轩是错的。”
好家伙！隔着屏幕都能闻到“硝烟”味了(bu shi~
事情是这样的。数学大佬陶哲轩和OpenAI两位高管最近进行了一场线上对谈，主题为“The Future of Math with o1 Reasoning”，即以推理为主的o1模型如何与数学融合，从而解锁突破性的科学进步。
其中陶哲轩认为，人擅长从非常少量的数据中推断出下一步该做什么，这是AI不擅长的领域。
但OpenAI高管Mark Chen针锋相对地指出，一旦OpenAI研究项目成功，人们将拥有非常高效的推理器，AI也能做数据稀疏推理，也许很快OpenAI将能证明陶哲轩是错的。
BTW，本次活动由Natalie Cone（创立并管理着OpenAI论坛）主持，除了2006年菲尔兹奖得主陶哲轩，还有OpenAI研究高级副总裁Mark Chen、以及OpenAI科学政策&合作伙伴关系负责人James Donovan。
有意思的是，Ilya Sutskever（OpenAI前联创&首席科学家，右下角）去年也参加了这个活动，甚至当时Jakub Pachocki（OpenAI现任首席科学家，右上角）也在。
鉴于直播内容较长，这里直接为大家奉上省流版：
AI可以将数学工作模块化，比如模式识别、形成猜想、验证等；
形式证明助手不可或缺，是进行数学研究和使用大语言模型之间的必要中间层；
论文是否给AI署名？当前AI的贡献仍难以界定；
目前对数学结果进行搜索的最好方式是众包，比如Math Overflow；
AI在竞赛中的表现，既出人意料，也低于陶哲轩预期；
……
话不多说，1小时嘉宾对谈+30分钟观众问答，干货这就整理出来了！
陶哲轩对谈OpenAI两位高管先来看几位嘉宾这次都谈了哪些内容，大致分为以下几个方面：
AI在数学证明和发现方面的潜力
将AI融入传统数学研究所面临的挑战
AI在科学发现与创新中的逐渐演变的作用
AI系统与人类数学家之间的合作机会
以下为重点内容整理。
AI可以帮助同时推进成百上千个数学问题，思考也更深入了James Donovan:你们目前在各自的研究领域中最关注哪些问题，以及为什么解决这些问题如此重要。
陶哲轩：我有很多想要解决的技术性数学问题。更贴近今天会议主题的是，我非常感兴趣我们如何从根本上重塑数学，以及如何利用所有这些新工具以前所未有的方式进行协作，以前所未有的规模开展数学研究。
我认为这可能是一个新的发现时代。现在的数学家一次只研究一个问题，在一个问题上花费数月时间，然后再转向下一个问题。有了这些工具，我们可能可以同时扫描成百上千个问题，并进行不同类型的数学研究。我对这种可能性感到非常兴奋。
Mark Chen: 过去一年，我们的一个主要关注点是推理。不过自GPT-4以来，我们略微改变了关注点。
GPT-4包含了大量的原始知识，但它在很多方面也存在不足。它会被简单的谜题难倒，并且经常依赖于先验知识。如果它对一个谜题的解法有先验知识，它通常会犯同样的模式匹配错误。这些都表明模型在深度推理能力上的不足。
因此，我们一直专注于开发o系列模型。这些模型更像是系统2思考者，而不是系统1思考者。它们不会经常给出直觉的快速反应，而是在生成回应之前花一些时间思考问题。
我想强调我们研究议程中的另外两个关键问题：数据效率和如何为用户创造直观愉悦的体验。
AI可以将数学工作模块化James Donovan: Terry，你多次提到一种潜在的新型数学，也谈到过不同的数学合作方式，能否为我们详细解释一下？
陶哲轩: 数学一直被认为是一项非常困难的活动，现在也是如此。原因有很多，其中之一是我们依赖一个人或一小部分人来完成许多不同的任务以实现一个复杂的目标。
如果你想在数学上取得进展，你必须首先提出一个好问题，然后找到解决它的工具，学习文献，尝试一些论证，进行计算，检查论证以确保其正确性，然后以可以解释的方式将其写下来，然后你必须做报告，申请资助，还有很多其他的事情要做。这些都是不同的技能。但在其他行业，我们有劳动分工。
我认为现在我们有了这些工具，原则上你可以进行一种合作，其中一个人有远见，一个人或一个AI进行计算，然后另一个工具撰写论文等等。因此，你不需要一个人在所有方面都是专家。
我认为很多人因为看到成为一名优秀的数学家所需做的所有事情而感到气馁，这确实令人望而生畏。但也许有些人擅长查看数据和检查模式，然后要求AI检查这种模式是否存在。也许他们不擅长找到正确的问题，但他们可以在一个更大的项目中处理一些非常狭窄的特定部分。
我认为这些工具可以将数学工作模块化，一些任务由AI完成，一些任务由人类完成，一些任务由形式证明助手完成，一些任务由公众完成。在其他学科中，我们有公民科学，例如业余天文学家发现彗星，或业余生物学家收集蝴蝶。我们还没有一种方法可以利用业余数学家的力量，除了一些非常小的边缘项目。因此，我认为有很多潜力，我们必须尝试很多东西，看看哪些有效。
AI与人类具体如何分工James Donovan: Terence，你似乎默认假设人类仍然会划分任务，他们仍然对流程有足够的了解来决定谁做什么，你是否认为因此会出现不同的数学家角色，不同的专业方向？
陶哲轩: 我认为软件工程可以作为数学发展方向的模板。过去，可能有一位英雄般的程序员包揽一切，就像数学家一样。但现在，你有项目经理、程序员和质量保证团队等等。因此，我们可以想象在数学领域也这样做。
我现在参与了几个合作项目，它们既包含理论数学部分，也包含形式证明部分，还有人运行各种代码算法等等。它已经像我预期的那样专业化了。有些人不懂数学，但他们非常擅长形式化定理，对他们来说就像解决谜题一样。还有一些人擅长运行GitHub，进行项目管理，确保所有后端顺利运行，也有人做数据可视化等等。我们都在协调工作。
到目前为止，主要是人类和一些比较老式的AI类型，比如改进器，通常只是运行Python代码之类的东西。但我认为这是一个范式，一旦AI足够好，它将非常适合其中。
James Donovan: 你是否认为这些角色总是由人类担任，或者你是否看到了一个由o系列模型本身分解问题的未来？
Mark Chen: 我现在几乎把AI当作我的同事。有很多我不擅长的事情，我可以交给AI去做。我只是在推测，因为我不是数学家，但就AI在帮助解决数学问题方面的优势而言，首先可能是识别模式。机器非常擅长这一点，尤其是有大量数据或大量需要筛选的内容时。
我认为从识别模式开始，你可以开始形成猜想。我认为它们在这方面可能有独特的优势提出证明策略。我认为今天人类仍然可能对前进的正确步骤有更好的直觉，但在特定步骤上可能存在盲点。我想上次我们提到了一种生成函数方法，一个模型在一个你试图解决的玩具问题中建议了这种方法，结果证明这在那种情况下其实还不错。
此外还有验证。模型可能能够验证你确信正确的某些步骤，但你只是想再找一双眼睛来确认。也许还有生成反例。如果你想考虑一个定理可能是错误的许多潜在方式，一个模型可能能够比你更有效地穷举这些可能性。
形式证明助手不可或缺James Donovan: 你们都提到了定理证明器和形式化的作用，是否可以公平地说，你们都认为这是进行数学研究和使用大语言模型或同等技术之间的必要中间层？
陶哲轩: 基本上是的。证明必须是正确的。数学证明的特点是，如果一个证明有100个步骤，其中一个步骤是错误的，那么整个证明就可能崩溃。AI当然会犯所有这些错误。有一些类型的数学可以接受一定的错误率，就像Mark说的，比如寻找模式，寻找猜想。
如果有AI只有50%的正确率，但你有其他方法来检查它，那么也没关系。特别是如果它想输出一个论证，那么强制AI以类似Lean的形式输出是一个非常自然的协同作用。如果它编译成功，那就太好了；如果没有，它会返回一条错误消息，并更新它的答案。
人们已经实现了这一点，他们可以用这种迭代技术证明一些简短的证明，但这还远没有达到你可以问它一个高级数学问题，它就能输出一个巨大证明的程度。
AlphaFold可以用3天的计算时间做到这一点，但它无法扩展。对于某些软性任务，可以接受正错误率，你不需要形式证明助手。但对于任何真正复杂的、一个错误就可能传播的任务，它基本上是不可或缺的。
Mark Chen: 在OpenAI，我们在不同的时期或多或少地关注形式化数学。我认为今天我们做的少了一些，主要是因为我们想探索更普遍的推理。我们确实希望你在计算机科学等领域学到的推理与你在数学等领域学到的推理非常相似。所以我当然理解进行形式化数学的优势。
数学家的“失败”是AI宝贵的训练数据James Donovan: 即使在训练过程中，可能有很多不正确的解决方法没有进入训练模型，因为数学家通常不会发布和纠正错误的东西，这对于更广泛的科学领域也是如此。你们两位认为这会产生很大的影响吗？我们是否应该努力推动人们也发布失败的答案？
陶哲轩: 我认为这是一个好主意。鼓励这样做很困难，人们不喜欢承认自己的错误。但这对AI来说可能是非常宝贵的训练数据。
当我教课时，有时最有效的课是偶然发生的，我准备了一个证明，然后在课堂上讲，结果证明是错的，我必须实时修改它。课堂上看到我尝试各种方法，比如，如果我改变这个假设，这个例子可能会有效。后来我得到了反馈，说那些是我最宝贵的课。那是因为我犯了错误。我认为这些数据在很大程度上是你们无法获得的。
事实上，许多领域专家的专业知识是建立在几十年错误的基础上的，这些错误教会了他们什么不该做，即负空间。随着我们转向更正式的环境，我认为这方面开始有所改变。
