很快OpenAI能证明陶哲轩错了？陶哲轩一句话，被OpenAI高管怼回去
这周，OpenAI连更两弹，又将o1模型推向全网最高潮。
就连奥特曼本人激动地预告，「迫不及待期待着下周的Day3发布，感觉周一是那么地遥远」。
首更第一天，放出的满血版o1，相较于之前的o1-preview在数学、代码能力上大幅提升，分别暴涨了27%。o1Pro版数学性能更是飙升36%。
作为o1早期的访问者，菲尔兹奖得主陶哲轩在OpenAI研究高级副总Mark Chen访谈中，畅聊了o1推理的数学未来。
OpenAI科学政策与合作负责人James Donovan主持这场采访
这场对谈以1小时的讨论开始，然后是30分钟的问答环节，含金量就不用多说了。
9月o1-preview发布之后，大西洋月刊曾写道，陶哲轩描述了一种前所未有的、由AI驱动的「工业级数学」。
至少在近期，AI并非独立的创造性合作者，而更像是数学家假设和方法的润滑剂。
简言之，AI还仅仅是一种辅助的工具。
这种新的数学协作模式，可以揭开知识的神秘面纱，保持人类创造力的核心地位。
不知这次，天才数学家又是如何看待o1的?
一个全新的发现时代，正式开启
陶哲轩称，我认为这可能开启一个新的发现时代。
当前，数学家们一次只能专注单个问题，花费数月时间解决完一个问题后，再去攻克下一个问题。
但有了这些工具，我们可能同时处理数百个，甚至数千个问题，同时开展完全不同类型的数学研究。一想到这种可能性，让他异常地非常兴奋。
Mark Chen肯定道，「太酷了。没错，在过去一年中，我们的主要关注点之一是推理能力。自GPT-4发布以来，团队稍微转移了研究的重点」。
GPT-4学习了很多世界知识，是一个非常智能的模型。但不得不承认地是，它在很多方面也表现得很愚蠢，会在简单的谜题上犯错，而且经常过度依赖先验知识。
比如，如果它对某个谜题应该如何发展有某种先验认知，它往往会陷入相同的模式匹配错误。
正是这些问题，向OpenAI团队指出了模型在深度推理能力方面的不足。
因此，我们才看到了O系列模型的诞生。它们更像是System2的慢思考者，而非System1快思考者。在给出回应之前，模型需要花费一定时间去反思问题。
有传言称，在OpenAI总部有一个o1实例已经持续运行/思考了6个月之久.....
AI解耦数学任务，开启全新协作模式
主持人James Donovan接着问道，「你所描述的『工业级数学』是一个怎样的未来，包括数学合作的不同方式，能否具体展开描述下」?
陶哲轩称，数学一直以来被认为是一项非常困难的活动。
原因之一是，它依赖于一个人，或者可能是少部分人来完成许多不同的任务，去实现一个复杂的目标。
如果你想在数学上取得进步，必须首先提出一个好问题，然后再找到解决它的工具。
再之后，还得学习各种文献，尝试一些论点，还得进行计算、检查算法。
如果结果是正确的，你还必须以一种可解释的方式写下来等等，集合了不同的技能。
在其他行业中，我们有劳动分工，就像制作一部电影一样，需要不同的人同时负责制片、剪辑、演出和融资等所有工作。
陶哲轩表示，在数学领域，直到最近我们才找到一种解耦这些任务的方法。
原则上。可以实现这样的协作:一个人负责构想，一个人或AI负责计算，另一个工具负责写论文等。这样就不需要一个人在所有方面都成为专家。
我认为，很多人不敢从事数学研究，是因为他们看到了成为一个优秀数学家所需要完成的所有事项清单。这确实令人望而生畏。
不过AI工具能够让一些重复性工作被解耦，变得更加模块化。
一些任务由AI完成，一些由人类完成，有些任务可能需要预先协助，有时甚至可以由普通大众来完成。
Mark Chen好奇问道，不考虑AI的情况下，迄今为止，最大规模的数学合作项目中，能够同时合作的人数上限是多少?
陶哲轩表示，在真正的实践中，限制大约是5-6人。超过了这一阈值，就真的很难了，因为你必须互相检查彼此的工作，还要考虑把所有人召集在同一个房间等问题。
确实有少数项目有很多作者，比如证明形式化项目，大约有20-30个作者，这是数学领域中为数不多的。
目前，已经的如何众包任务方式之一是，将其放在GitHub上，都使用Lean这样的形式化语言，所有的贡献都可以被验证。
主持人James Donovan问道，当你解释这些时，听起来你的默认假设是人类仍将分配任务，他们仍将对整个过程有足够的理解来决定谁在哪里做什么。你是否认为数学家角色是否会分化，是否会出现新的专业方向?
陶哲轩表示，我认为软件工程可能是数学未来发展的一个可借鉴的模板。
过去，可能有一个英雄式的程序员包揽一切，就像现在的数学家那样。但现在，我们有项目经理、程序员和质量保证团队等等。我们可以想象现在就这样做。
他称，我目前参与的几个协作项目就同时包含理论数学部分和形式化证明部分。人们还在运行各种代码算法等。而且正如我所预期的那样，已经开始出现专业化分工。
有些人可能不懂数学，但他们非常擅长形式化定理，对他们来说这就像解谜题一样。
还有一些人擅长管理GitHub和做项目管理，确保所有后端工作顺利进行。
还有人负责数据可视化等工作。我们都在协调合作。到目前为止，主要还是人类在工作，使用的是更传统的AI工具，比如改进器（improvers），通常就是运行Python代码之类的。
「但我认为，一旦AI足够强大，它会很自然地融入这个范式中」。
Mark Chen同样表示，对我来说也是这样的。在很多方面，我几乎把AI当作同事看待。有些我不擅长的事情，我可以交给AI去做。
虽然我不是数学家，但就AI在帮助解决数学问题方面的优势而言，首先可能就是模式识别。机器在这方面相当擅长，特别是在需要处理大量数据或信息的时候。从识别模式开始，就可以形成推测。我认为AI在这方面可能有独特的优势。
针对制定证明策略，我认为现在人类可能在判断正确步骤方面仍有更好的直觉。但也许在某个特定步骤上，人类也可能会有盲点。
此外，在验证方面，模型能够验证某些你认为正确，但想要再次确认的步骤。
还有就是生成反例，比如当你想要考虑很多可能使定理失效的情况时，模型可能比你更有效率地穷尽这些可能性。
主持人再次问道，可以说，你们都认为改进器在进行数学研究和使用LLM或类似技术之间，必要的中间层吗?
陶哲轩表示，基本上是这样的。
数学证明的特点是，如果一个证明有100个步骤，其中一个出错了，整个证明就可能完全崩塌。而AI，我们知道它会犯各种错误。在某些类型的数学科学中，一定的错误率是可以接受的。
就像Mark所说的，比如在模式识别、形成猜想时，即使AI只有50%的正确率也是可以接受的，只要你有其他方法去验证。
特别是当它试图输出论证时，强制AI使用类似Lean形式化语言输出是很自然的协同方式。如果能编译通过就很好，如果不能，它会返回错误信息。
当前，人们已经实现了这点，他们可以用这种迭代技术证明一些本科作业级别的简短证明。当然，现在还不能直接问一个高层次的数学问题，就期待它输出一个庞大的证明。
接下来，陶哲轩提到了，虽然Alphaproof可以用3天的计算时间做到，但这种方法无法扩展。
对于一些可以接受正向错误率的简单问题，你不需要形式化证明助手。但对于任何错误可能会传播的复杂问题，形式化证明助手基本上是不可或缺的。
人类数学美学，AI难以复刻
数学，也有自己的美学。
陶哲轩表示，就像关注抽象概念一样，我认为人类对数学有一种特殊的美学感觉，这种感觉与数学的核心是紧密相连的。
因为这种美学感受是由人类来判断的，所以AI模型在定义问题和品味方面可能会更难模仿这一点。
不过，陶哲轩还认为，AI在数学领域的应用将带来一种 「不同的美」，计算机生成的证明将有别于人类生成的证明，具有自己的一种优雅。
接下来，James Donovan提出三连问，「你对年轻数学家有什么建议吗?他们应该把重点放在哪里?应该解决什么样的问题?」
陶哲轩认为，年轻数学家必须保持灵活性，因为数学已经逐渐变成了一个技术性学科，越来越考验协作性。
50年前，数学家还可以独立解决某个子问题，但现在几乎行不通了，不过对于数学来说，也算是良性发展了，通过利用AI，数学家们可以进行更广泛的合作，帮助互相补齐知识。
但需要注意的是，这些工具也有局限性，不能盲目，要用自己作为人类的聪明才智来驯服、监督AI，而不是把AI当作一根魔法棒。
James Donovan表示，OpenAI也不鼓励人们盲目相信AI，如果没有足够的专业知识，就会陷入另一个技术陷阱。
为了更好地利用AI工具，Mark Chen建议现在的学生认真学好各自领域内的技术知识，然后参与一点人工智能相关的研究，至少要了解神经网络的基础知识，比如如何训练模型，底层运行机制，以及局限性。
人们越是对AI的能力保持怀疑，越是会提升自己与AI工具的协作效率。
1%最难数学题，AI还未取得突破
针对「谷歌DeepMind拿下IMO奥数银牌」一事，James Donovan询问陶哲轩是否对这一进展感到出乎意料。
陶哲轩表示，确实相当超出预期，过去几年中一直有很多相关工作，比如DeepMind在IMO数据中合成了很多证明过程，但大部分都是错误的，所以普遍观点是这条路并不可行，但现在却一下子实现了。
还有一个问题是，目前的AI还只停留在数据阶段，并没有想象中的那么有用，只是解决了2000万个小的数学问题，理想中的AI系统是能够解决一个大问题。
目前数学项目里的问题，99%都可以通过传统的暴力搜索解决，但还有1%是相当困难，且需要人为干预的，而正是这1%的问题最具挑战性，直击AI技术的本质，目前的突破不算特别有意义。
James Donovan则提出疑问，现在的工作主要是教模型以一种特定的方式进行推理，那思路应该一个模型，多种类型推理;还是多个模型来应对多种推理?进一步，需要什么样的推理才能让AI解锁这些有难度的小问题?
Mark Chen的思路是大道至简，并不需要单独设计多个模型，简单也是开发AI产品的关键咒语。但在连接复杂系统的时候，可以由人来建立结构，让AI模型以某种方式进行合作。
增加数据，比如一万个类似的样本，让模型学习推理模式，未来或许从这方面探索一下。
陶哲轩则认为，AI的问题解决和人类是非常互补的，AI主要以数据驱动的解决问题的方式，对于某些任务，AI实际上比人类更重要，但人类需要做的是，重新校准对某些问题的难度感知，或许只是因为之前没有尝试使用数据驱动的方法来解决那些经典问题。
数学中，有些问题真的很难，甚至都无法被确定，也没有大量的可用数据来学习，甚至无法继续证明这些问题无法被证明，而这些问题正是人类擅长，而AI不擅长的事。
如果仅仅以智力作为唯一评估尺度，可能是不够的，所以AI和人类进行互补或许才是终极解决方案。
Mark Chen则打趣道，我希望我们的研究计划能成功，构造一个非常高效的数据推理器，然后证明你是错的。
陶哲轩则表示，我也很希望被证明我是错的!
AI在数学定理发现和检索方面的潜力
在做数学研究时，一个最让人崩溃的事，莫过于其他人抢占了先机，而你自己并不知道。
比如在试图证明一个小引理时，就算你心里知道肯定有100个人证明过了，可能是在代数、几何，还是社区代数、群论、Pds等领域，但就是很难找到答案。
对于问题「是否在不久的将来，人们可以很轻松地检索到某些数学定理?」，陶哲轩表示，把数学计算机化，并支持检索，是一个很棒的想法。
OpenAI的o1模型实际上已经开始做了一点点，比如对于某个定理，你大概知道是什么，但不记得名字了，所以没办法用搜索引擎，或者从大量论文中检索某个定理，这些都是很关键的使用场景。
AI可解释性的理论滞后
AI经常会有幻觉问题，生成的答案可能是不正确的，人工检查非常关键。
比如ChatGPT说周六下午两点有一场歌剧，去了以后发现并没有，这种问题带来的损失还算比较小，并且可验证，但在科研领域，比如AI辅助药物开发，用户也不知道真正的答案，也无从验证，还会带来长远的影响。
对于这个问题，Mark Chen鼓励用户在使用大模型时结合搜索结果，模型会引用特定的网站或特定的来源来反映真实情况，未来模型也会更精确，用户可以到网站上自行检查结论。
需要注意的是，o1目前还不具备搜索能力。
反哺数学
历史上，总是先有数学或数学理论，再有其他如物理学、化学等进行理论应用。
随着AI的进步，比如物理学，已经有人开始使用机器学习来模拟像Pds的计算解和传统方法无法解决的问题，数学是否也从其他领域获得了理论上的新思路?还是说只是生成了更多数据?
陶哲轩回应说，数学是一条非常宽的双向车道，比如物理学家可能已经发现了数学原理，但没有解释，然后还需要再回过头发展数学理论。
比如狄拉克发明了狄拉克δ函数的东西，根据正统数学，它并不是一个函数，所以我们还需要扩大对函数的概念，所以理论发现永远是双向的。
可以想象到，一个非常实用的、科学驱动的应用程序，可能由于人工智能发现一些新现象而无法解释，或许是经验上的发现，然后促使科研人员利用数学工具去寻找理论解释。
演讲者介绍
陶哲轩是加州大学洛杉矶分校的数学教授，研究领域包括调和分析、偏微分方程、组合学和数论。
他曾获得了多项大奖，包括2006年菲尔兹奖。Mark Chen是OpenAI研究高级副总裁，负责监督高级人工智能计划，推动语言模型、强化学习、多模态模型和人工智能对齐方面的创新。
James Donovan领导GA的科学政策和合作伙伴关系，专注于如何最好地使用模型来加速科学研究和商业化。
他加入OpenAI之前，曾是Convergent Research的创始人、风险投资人和合伙人;在那里，他帮助创办了多个「登月」科学组织，包括Lean Fro（一种复杂数学的自动定理证明器）。
更新于：3天前