红杉资本对话Harmonic联创：数学即推理，合成数据是模型的新燃料，计算资源和自博弈是进步的关键

图片来源：Sequoia Capital

Z Highlights

• 数学界对AI在数学中应用的看法存在分歧，但年轻一代更支持AI和验证工具。Vlad指出，通过递归自我改进，AI有潜力在数学和其他复杂问题上取得重大突破。随着AI在模式识别和自我改进方面的进步，它可能参与解决大型数学难题，如黎曼猜想。同时，数学家仍将在引导AI方向、规划研究领域和解释结果方面起关键作用。

• 在数学研究中，数据相对匮乏，因此合成数据成为模型训练的关键。通过自发生成合成数据，系统可以在较低级别上构建复杂性，从而更好地提高自身。Tudor认为，计算资源的投入和自我博弈模式是推动模型进步的重要因素。此外，数学问题可以通过代码复杂性进行分解和解决，使得AI能够处理更大、更复杂的问题。

• Harmonic的目标是成为探索人类知识前沿的工具，不仅能够解决现有数学难题，还能在软件工程和商业应用中提供价值。通过验证软件代码的正确性和进行精准的数学推理，Harmonic希望影响包括物理学在内的多个领域，从而推动科学和工程的进步，并带来更可靠和精确的技术应用。

“数学即推理”：数学提高AI表现的原因

Sequoia Capital: 所以你们有一个核心信念，认为数学就是推理，并且你们持有一种可能与众不同的观点，即训练模型在数学上表现良好的最佳方式是直接教授数学，而不是像许多其他基础模型公司那样，让数学作为规模的属性自然出现。你能谈谈这个核心信念吗？为什么需要直接教模型数学？另外，数学是推理，这句话是什么意思？

Tudor Achim: 在我们创办公司时，我们非常注重数学，我们稍后可以详细谈谈这个话题。如果你观察所有科学和工程领域，几乎所有领域，数学都是它们的基础。数学基本上已经成为人们理解宇宙的一种方式，它是从黑洞到原子建模现象的方法，也是工程中设计事物的方式。这里有几个原因：首先，宇宙恰好可以用数学来解释，所以你可以写下一组相对简洁的符号来解释事物。但另一个非常重要的原因是，它是一种构建共享认知理论的方式，这些理论是非常客观、清晰和透明的。

如果你和我在讨论一些严谨的事情，我们可以写下一套演绎规则，达成关于我们所建模的基础规则的共识，然后从中推导出结论。所以，当人们在数学方面变得非常优秀时，他们往往在科学和工程的其他量化领域也很出色。因此，我们的想法是，如果打造一个在数学方面非常优秀的系统，你可能会看到同样的现象。这意味着它可能不会立即写出世界上最好的历史论文，但当你让它处理科学或工程问题时，它就会表现得非常出色。这就是我们从数学开始的原因。

Sequoia Capital: 在帮我做数学作业和写历史论文之间的界限在哪里？数学在某些方面确实难以跨越。你认为对于一个以数学为核心的模型来说，它的能力极限在哪里？

Vlad Tenev: 我给你一个非AI的视角。我从小学习数学，也一直很擅长数学。我记得在数学课上，总有七年级的学生会举手提问，尤其是在老师教一些抽象概念的时候，比如三角形的边角边定理。那时候，总有个让人烦的学生会问：“我们什么时候会用到这些呢？”然后老师总会有点含糊地回答，说：“你可能很快用不到，但学好数学会让你在其他方面也很优秀。”其他孩子总是对这个说法将信将疑，但我相信了。因此，我不断学习更高级的数学课程，我去了斯坦福大学，主修数学，然后继续攻读数学博士。

我相信，如果我专注于数学，我就会在解决问题上非常出色，商业问题和其他问题相比之下就会容易多了，因为每周花十个小时破解那些让我抓狂的抽象代数题目，那才是真正的挑战。事实证明我基本上是对的。我没怎么关注其他东西，只是上过一门斯坦福的计算机编程入门课程。五年后，我成了一名企业家，发现自己很容易上手代码，也很容易理解合同。所以，我觉得至少对人类来说，数学可以迁移到其他能带来经济收益的领域。对于AI，我的直觉认为也应该是一样的。

Tudor Achim: 在业内，这已经是个公开的秘密，就是用大量代码数据进行训练能大幅提升在推理测试中的表现。所以你可以想象，当你拥有包含更多一般性推理的出色数学数据集时，效果会是什么样子。

Sequoia Capital: 没错，这个观点很有共鸣，就是数学教会人们如何进行批判性和逻辑性思考，而这种能力可以迁移到其他很多领域，这在人工智能中也应该适用。Vlad，你刚才随口提到你学过一点数学，对于不太了解你数学背景的人，我记得你曾在Terry Tao门下学习过一段时间，他可能是当今世界上最伟大的数学家之一。你还提到过，你偶尔会和他见面，比如在洛杉矶时一起吃午饭。所以我很好奇，当你和Terry Tao一起吃午饭时，你们都聊些什么？你会提供股票建议吗？

Vlad Tenev: 不，我不能这样做。作为金融领域上市公司的CEO之一，我有很多关于股票的建议，但不能分享。我必须把这些建议保留给自己，而且基本上也不能进行交易，这很可惜，因为我非常喜欢交易。

不过，说回我怎么去到UCLA的。Terry Tao是UCLA的教授，他的工作广度真的让人惊叹。大多数数学家都在一个相对狭窄的领域深入钻研，而Terry在数十个领域都有深入的贡献，比如数论、组合数学、调和分析和应用数学等。他是该领域的主要贡献者之一，他现在正在用Lean形式化自己的论文，还会参与社区的讨论，和学生互动。他还有一个非常受欢迎的博客。我认为他之所以能做到这一点，是因为他比99.999%的人都聪明，从很小的时候就表现得与众不同。

我在本科期间，跟随一位同样很厉害的教授Larry Guth完成了数学论文，他最近在数论或黎曼猜想方面的一个结果是突破性的。在非人工智能的数学领域，这一结果确实让人印象深刻。他建议我看看UCLA，我对他的领域非常感兴趣，最后幸运地能在Terry Tao教授门下学习。但我要说明，我虽然读了研究生但算是辍学了，我只在UCLA读了一年。Terry Tao教了我研究生阶段的分析课程，真的很了不起。我记得有一次和Tao教授一起阅读时，他给了我一本书并签了名，我想他是想确保我读完后会还给他。结果他不知道，这样一签名他就永远得不到那本书了。每次见到他我都提起这件事，说那本书在我的书架上，与我其他签名版首版书放在一起，他是拿不回去的。

数学界如何看待AI数学？在分歧中寻找数学新意义

Sequoia Capital: 数学界对AI数学怎么看呢？大家意见分歧吗，还是认为这是通往理想境界的途径，是解决黎曼猜想和其他问题的方法？

Vlad Tenev: 我觉得看法是分裂的，年轻的数学家似乎更支持AI、验证和像Lean这样的工具，而年长的人则有些怀疑。这种情况在几乎每个领域都存在，不足为奇。我猜想这种情况会演变，我的想法类似于国际象棋的发展，开始时可能会有一个较长的阶段，人类与AI辅助共同协作，这会带来很多好的成果。但随着时间的推移，AI会变得越来越出色，比如现在的国际象棋，如果有一个人类辅助AI，AI可能会因为输入信息不准确而感到烦恼，因为这些输入只会让结果变差。

我不确定我们是否会达到那种程度，但我认为人类在某种程度上需要引导算法，而数学家的定义和角色会发生根本的改变。我和一位在麻省理工学院的数学家朋友聊过，当我们刚开始这个话题时，我问他怎么看。这是一位年轻的教授，对这个领域非常感兴趣。我问他：“你是否担心自己所在的领域会发生根本性变化？”他说，数学领域一直在变化。在19世纪，数学家曾被认为是皇室的计算器，他们手动解二次方程。当计算机和计算器出现时，人们担心这个职业会消失。但数学家定义数学是什么，所以在某个时候，他们可能会通过提示来引导这些AI来解决问题。我认为这会非常重要。即使AI解决了黎曼猜想，人类仍然会参与其中，因为黎曼猜想本身就是人类提出的。

Tudor Achim: 我觉得未来会有很多计算资源专门用于数学，而问题是一个很人性化的问题，即人类要通过什么方式决定将这些计算能力用在哪里。我认为这将是数学家的工作，他们需要选择研究的方向，如何解释结果，以及如何理解未能找到答案的情况。

Sequoia Capital: 你觉得AI数学系统能解决黎曼猜想吗？你认为它的极限在哪里？

Vlad Tenev: 我认为它应该能够解决这个问题，或者证明它是不可判定的，那也是一个有趣的结果。如果你考虑一下像Tao这样的大数学家能够做到的事情，他们能够综合大量的论文和前沿成果，并且以其他顶尖数学家也能做到的方式从中学习，找到这些之间的联系，并利用它们创造新的、更复杂的理论。这正是我们正在构建的系统的工作方式，这也是计算机和AI模型的强项，能够综合大量信息、发现模式并递归自我改进。

我记得上次在Metaculus上查看时，有43%的概率认为下一个千禧年大奖会由AI或人类在AI的协助下解决。我觉得这个概率是被低估了。我们可能很幸运，Larry Guth正在解决黎曼猜想，那将是惊人的。如果下一个问题是由人类解决的，那很可能会在不久的将来发生。而再下一个问题，很可能会在很大程度上由AI解决。

Sequoia Capital: 你提到的一个观点我想重点讨论，就是递归自我改进的概念。在AI领域中，若从全人类到全AI画一个光谱，人与AI的协作就位于中间，从大量人类参与、少量AI参与，到大量AI参与、少量人类参与。有趣的一点是，至少以我理解的方式来看，由于Lean的存在，你可以将数学和代码封装起来。由于形式验证，可以客观地判断对错，这意味着你有一个客观的奖励函数，可以用于自博弈（ZP注：自博弈，self-play指的是智能体通过与自身副本或历史版本进行博弈而进行演化的方法，近年来在强化学习领域受到广泛重视），以实现快速的循环时间和强化学习的进步。

这意味着你的模型可能会进步得非常快，因为其中没有人类参与，递归自我改进有明确的目标函数，你可以通过自博弈不断提升模型的能力。大多数AI领域都没有这种特性，因为循环改进的过程往往比较复杂。你能否详细讲一下这个系统的一些细节，比如是什么促进了你的模型提升？是什么决定了它能多快变好？因为这看起来似乎能够在相当快速的时间内变得更好。

Tudor Achim: 在谈到这个之前，我觉得最有趣的是，递归自我改进在其他领域也能发挥作用，比如像AlphaGo这样的棋类游戏。但很多人没有意识到的是，在这些完全可观察的零和游戏中，你可以通过自博弈不断提高，直到达到最优策略。到那时，无论你有什么系统，都无法再做得更好。而数学最令人兴奋的地方在于它没有上限，所以你可以不断投入计算资源，让它持续改进，没有尽头。因此，当我们讨论AI能否解决黎曼假设或获得千禧奖时，那些只是非常人类化的里程碑。我认为真正的问题是它是否会停止，因为显然它会达到那些目标。我相信我们最终会解决远比黎曼假设更难的问题，那些我们甚至还没构思出来的问题，因为它们几乎超出了我们能够描述的难度。

Vlad Tenev: 你们有没有看过那个AI在20秒内通关《我的世界》的视频？那听起来是个不错的比喻。你知道《我的世界》是怎么回事，人类是怎么玩的，然后AI在20秒内通关，这简直让人难以理解。你甚至无法弄清楚视频里到底发生了什么。

Tudor Achim: 如果我们谈谈Harmonic的工作原理，可以把它看作是一群agents在尝试解决问题。因为我们使用Lean，所以能够检查答案是否正确，从而提取各种用于改进系统的训练信号。不过需要说明的是，Lean只是用来验证结果，并不会告诉你是否更接近答案或者是否变得更聪明，只是告诉你结果是否正确。因此，要让它快速变得更好，还有很多科学上的挑战需要解决。

Sequoia Capital: 你能简单介绍一下Lean是什么吗，以防有人不太了解。

Tudor Achim: 当然可以，Lean就是另一种很棒的编程语言，由Leo Deora创造，可能是最好的编程语言。未来我们或许都会写Lean，或者AI会写Lean。它的理念是将数学命题编码到语言的类型系统中。简单来说，Lean里面有函数，输入类型对应数学定理的假设，输出类型就是结论。Lean的重点在于，如果你写了一个实现该函数的程序并且能够通过编译，那就意味着你可以从输入类型推导出输出类型，这就意味着你可以从假设推导出结论。这就是如何将Lean用于数学的基本方法。

Vlad Tenev: 我觉得Lean特别有趣的一点是，它的创作者Leo Deora现在在Amazon AWS工作，他并不是数学家，而是把Lean写成了一种软件验证工具。他相信未来的软件将会被验证，而现有的工具，比如Isabelle等，都是几十年的老软件验证工具，使用体验很差，对开发者来说很不友好。所以他想创造一个更好的软件验证工具，希望通过创建一个更好的工具吸引更多人使用，从而提升软件质量，这本身是个很高尚的目标。

但他没想到的是，软件验证其实只是在证明软件具备某些性质，这个工具在数学界变得非常流行，有成千上万的数学家和学生在构建一个名为mathlib的有机库。你可以把它看作是最大的开源数学教科书，它在GitHub上，并以相当快的速度在增长。我认为Lean在数学上的应用某种程度上已经超出了人们的预期，可能现在在数学方面的应用比在软件验证方面更多，随着时间和AI的发展，这可能会发生变化。

Sequoia Capital: 我们总是要问的一个问题是，为什么是现在？因为强化学习已经存在很长时间了，数学存在的时间更长。现在似乎数学正好迎来了一个拐点，你们选择在这个时候开始做Harmonic，为什么是现在呢？

Tudor Achim: 我觉得现在有两个很好的理由。首先，AI系统在一些有趣的方面取得了很大的进步。我其实在2015和2016年跟一个好朋友讨论过用强化学习来改进理论的问题，当时的问题是并没有一个AI系统能在无限的动作空间内进行预测。在围棋中，你可以把棋子下在特定位置，不管是黑棋还是白棋，但是在数学中可以做任何事情，比如你可以生成任何下一步。当时我们没有好的系统去做这个，但现在自回归语言模型已经变得相当不错，所以这是其中一个使其成为可能的原因。我说的时间跨度大概是十年，这很重要。

另外一个很惊人的事情是Lean变得非常好用。如果你20年前告诉数学家，有很大一部分领域会对数学中的形式方法感兴趣，他们可能会觉得你疯了，因为那时形式方法真的只限于形式逻辑或某些类型的图论，比如你们可能听说过四色定理，那是形式数学的一大成功。但Lean是如此的灵活和令人兴奋，人们因此贡献了一个叫mathlib的东西，现在有很多知识可以用于证明事情。因此，AI已经开始有可能适应这个问题，再加上Lean的良好表现，这两个因素结合在一起，真的使现在成为解决这一问题的好时机。

合成数据作为模型燃料，为算法进步提供动力

Sequoia Capital: 你们可以谈谈数据，特别是合成数据，以及它是如何驱动你们正在构建的模型的吗？

Tudor Achim:合成数据是模型的燃料。我们有一个很棒的资源叫做mathlib，这是一个开源库，里面有很多人工编写的Lean代码，它们以一种非常通用和简洁的方式编写，主要用于证明复杂的定理，但不一定适合用来解决具体问题。因此，几乎唯一可以使用的数据就是你自己生成的合成数据，因为原始数据并不太适用。所以，相比AI的其他领域，这是一个数据非常匮乏的环境。因此，我之前描述的过程，即agents自发解决问题并由此产生训练信号，是获取数据的主要方式。另一个挑战是你必须通过不同的智能水平以逐步进展，所以你一开始并不一定要证明黎曼猜想，而是从证明简单的东西开始，然后在整个过程中递归地自我增强。

Sequoia Capital: 事实证明，互联网上的数学数据远没有猫咪视频多。

Tudor Achim: 当然没有。

Sequoia Capital: 这很有趣，因为基础模型公司遇到了数据壁垒，到现在他们已经耗尽了互联网上可用的数据。如果你能生成大部分所需的训练数据，这也算是以数学为核心的另一个优势，而不是指望数学作为规模的一种涌现属性。

Vlad Tenev: 我认为数据壁垒体现在两方面，一方面就像你说的，我们已经耗尽了互联网数据。另一方面是现有互联网数据的质量，这可以看作是这些模型智慧的上限。如果你仅依赖猫咪视频、维基百科和各种互联网内容进行训练，如何让模型变得显著更聪明是一个开放性问题。因此，我们认为需要进入某种自博弈的强化学习模式，以达到在人类数学家和研究人员在多个任务上的能力之上。

我认为这个路径是不可避免的，类似于AlphaGo到AlphaZero的过程，我们需要学习如何让这些模型生成大多数的数据，并随着模型的不断迭代，让数据复杂性增加。数学的优点在于它有一条简单的路径来实现这一点，你可以通过Lean代码行数来衡量数学问题的复杂性和难度。通过观察系统的复杂性，许多问题可以被拆分成更小的部分，然后一个一个解决。这样的话，小任务变得更容易处理，因为它们需要解决的问题的代码行数比大的任务少。所以如果你在这方面做得很好，然后在解决这些小问题上也很在行，那么你就可以训练模型做得更好，并随着继续推动这种极致，模型将逐步适应更复杂和更难的问题。

这在数学中很有效，因为它反映了我们用笔和纸解决数学问题的方式。我们已经能够从简单的公理出发，构建庞大而复杂的结构。黎曼猜想可能需要数百页甚至更多才能解决，费马大定理据说需要200页，非常复杂。所以，我相信，最终你会达到一个水平，能够解决这些问题，而数学在某种程度上就像是原始的合成数据。

Sequoia Capital: 是什么决定了你的模型提升速度？

Tudor Achim: 我认为最高层次的因素是能量。投入的能量越多，就能并行进行更多尝试，这意味着数据生成得更快。虽然有很多限制速度的步骤，但没有根本性的限制来决定它能提升多快。因此，关键在于你投入了多少计算资源。

Vlad Tenev: 我觉得在这个领域仍有很多未解决的问题。比如，我们从过去已经证明的核心定理中受益匪浅。就像在数学竞赛中，有些定理是每个学生都需要学习并使用的，比如AM-GM不等式之类的。而且，某种程度上，mathlib是不完整的，比如几何内容非常少，并且内容非常理论化和抽象化。所以一个限制因素就是mathlib的内容。

当然，最终的模型必须解决创建新理论和新结构的问题，并扩展到其他领域，尤其是擅长于将人类尚未形式化的东西进行形式化。我认为这会是一个重要的突破，并且在未来几年内肯定会发生。到时候，你可以给出一个简单的情境，比如一个棒球队互相传球的情境，系统就可以自动将其形式化，并即时将其转化为Lean代码。我觉得我们还没到那个可以可靠实现的阶段，但一旦达到，我认为这将是一个巨大的突破。

创办Harmonic， 探索人类知识前沿

Sequoia Capital: 如果一切顺利，你认为Harmonic会变成什么？

Tudor Achim: 我们的使命是探索人类知识的前沿，确保我们产出的东西对人类是正确且有用的，这对我们来说非常重要。我认为在最佳情况下，我们能够打造出一个工具，许多数学家可以用来解决所有的千禧难题，并在此基础上走得更远。我认为这将是对人类的巨大贡献。

此外，这个软件在商业应用上还有其他领域的潜力。对于软件工程来说，梦想就是能够验证代码的正确性。为此，你需要对代码的运作有一个非常好的模型，能够理解库的工作原理及其承诺的功能。如果能开发出一个非常擅长数学推理并能很好地验证自己推理的系统，将会有很多应用。我们认为这将会有很大的应用前景。

Vlad Tenev: 软件工程作为一个学科正在快速变化。我相信你们也看到过各种关于人们用Cursor和Claude 3.5做疯狂事情的报道。我认为在未来，软件工程将不太涉及代码的审查和协作，而更多地关注规范上的协作——我们希望代码做什么？我们能否对此更加严谨？这就是为什么验证会变得更加重要。随着软件成本趋近于零，经过验证的软件成本也将趋于零。因为需要专业人士，这件事情本来非常不切实际且昂贵，但有了AI则会大大加速。

5到10年后，如果我们沿着能力曲线继续进步，那么绝大多数的软件将是经过验证的，并且可以证明是正确的。这是一个非常令人兴奋的未来。从更理论的角度看，不仅是数学，物理本质上也是数学。理论物理学是数学的一个前沿应用。我个人觉得能够加速一些基础物理研究进程，去真正理解为什么宇宙是现在的样子，为什么存在这些物理定律，并帮助设计实验来验证这些理论，会是一件令人自豪的事情。

Sequoia Capital: 你觉得你主要会贡献于数学及其相关领域，比如物理和软件工程，还是说你认为任何涉及推理的领域都在Harmonic的范畴内？

Vlad Tenev: 我们目前还是一家小公司，所以我们尽量专注于一些特定领域。从长远来看，如果你认为数学就是推理，而我们确实这么认为，那么如果我们在数学和计算机科学方面做得非常好，那么任何领域都可能在这些模型的范畴内。即使是历史论文，我认为我们也能应对。不过，我个人一直很喜欢写历史论文，尽管我的父母说人文学科和语言艺术不用太在意，但我觉得我的数学能力也让我写出了不错的历史论文。所以希望有一天，Aristotle也不例外，毕竟他也写过一些伟大的历史评论。

快问快答

Sonya Huang：我们来个快速问答环节吧。你们认为自己会在哪一年赢得国际数学奥林匹克竞赛（IMO）？

Vlad Tenev：也许是2024年吧。 

Pat Grady：好，我们帮你们登记2024年。

Sonya Huang：那么千禧年大奖呢？ 

Vlad Tenev：2029年。 

Pat Grady：2029年？我们听说是2028年。 

Vlad Tenev：可能是AI与人类合作的方式，完全由AI解决的话，我想也许会更快。

Vlad Tenev：如果你定义为能够在数学问题上超越任何人类的推理能力，例如给Terry Tao（陶哲轩）带来挑战的那种水平，我认为我们还需要几年时间。但我相信在接下来的一年内，模型能够达到99.99%的顶尖水平。

Sonya Huang：你觉得Terry会同意这个看法吗？

Vlad Tenev：我想他会同意的，但最好还是亲自问问他。

Pat Grady：我们最喜欢问的一个问题是：在AI领域中，你最崇拜谁？不过我们稍微调整一下问题，对你们来说，在AI或数学领域中，你最崇拜谁？

Vlad Tenev：我喜欢冯·诺依曼。他从数学家起步，他的父亲曾试图劝阻他从事数学，因为数学不太能赚钱。但最终冯·诺依曼的才华显现出来，他不仅开创了计算机科学，还为现代计算机提供了蓝图，并且为博弈论做出了开创性的贡献。他的贡献不仅限于学术，还影响了社会的多个方面。作为一位来自东欧的科学家，我非常钦佩他的广泛成就。

Tudor Achim：我对科学家和数学家都充满敬佩，但如果要提到一位特别值得称赞的数学家，我会提到莱布尼茨（Leibniz）。他与牛顿竞争开发微积分，尽管牛顿的体系后来占了上风，但莱布尼茨提出了一个非常有远见的概念，称为“普遍符号体系”（universal characteristic），这一概念本质上预示了我们今天在2024年看到的情况：自动化的推理过程，以及在一个可以被推理的语言中构建知识的百科全书式的体系。莱布尼茨在没有现代计算机的情况下，能够预见到这些远超他时代的理念，实在令人惊叹。

Pat Grady：太棒了，谢谢你们的分享。

Vlad Tenev&Tudor Achim：谢谢邀请我们来！

原视频：Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters

https://www.youtube.com/watch?v=NvAxuCIBb-c

编译：Weiyi He & Entong Zhang

文章来自于“Z Potentials”，作者“Weiyi He & Entong Zhang”。