孔某人 2024-11-15 11:55 北京
本文是2024.11.14 No Priors采访DeepMind AlphaProof 团队3人的播客的“脱水”版。
No Priors Ep. 90With Google's DeepMind's AlphaProof Team播客视频链接https://www.youtube.com/watch?v=uX6ceY1vcUg
什么是“脱水”版
脱水版workflow的调教目标是：力求保留所有信息。根据经验来说，从英文到中文跨语言脱水时大概会保留访谈原始文字稿一半左右的文本大小。
跟之前一样，本文也是一个阶段性的技术能力展示，内容都由workflow自动生成。
文中的粗体是我人工标注的我认为重要的信息。节选的选择也是我人工进行的。
本公众号没打算大量转载内容，所以同样技术方案的内容大部分会由别的号发出，例如以下文章就是与本文同样版本的方案：
Claude之父Dario Amodei专访: 回应关于Claude、AGI和人类未来的一切 | 3小时播客脱水总结
Anthropic安全对齐主管Amanda专访：理想的AI是世界旅行者；保持同理心才能写好Prompt
关于播客内容的评论
从我个人角度，我读完觉得这个播客中有用的内容不多，不看也罢。
但考虑到这个内容会是不少人感兴趣的点，我不会因此就丢弃这个内容，阻碍大家观看。
另外近期也没有合适的内容作为展示case放在本号上，所以就把这个拿来做了。
正文
介绍
00:00:06
Sarah Guo(主持人):
今天我们邀请到了来自DeepMind的AlphaProof团队的Thomas Hubert、Rishi Mehta和Laurence Sartran。
AlphaProof是一个新的AI系统，它能够发现和验证数学证明，这是继DeepMind在国际象棋和围棋领域取得成功之后，在AI领域的又一个重要突破。
在今天的节目中，我们将深入探讨AlphaProof的工作原理、它对数学和AI领域的影响，以及关于test time RL的内容，同时也会讨论这个系统在机器学习严谨推理能力方面的表现。
能否谈谈你们的背景，以及是如何开始一起在AlphaProof工作的？
Rishi Mehta:
我是AlphaProof的技术负责人之一，一直在计算机科学和机器学习领域工作。作为一名棋手，我看到A0论文中展示的那些棋局后备受启发。创造出如此优美且近乎超越人类认知的智能让我感到神奇。后来我加入了由Thomas领导的DeepMind AlphaZero团队，开始研究数学领域的应用。
Thomas Hubert:
我早期在计算机网络异常检测和广告定向投放领域工作。后来转向AI研究，我特别关注那些能通过增加计算量来解决更难问题的系统。我认为数学是这类系统的完美应用领域。
Laurence Sartran:
我年轻时投入了大量时间练习围棋。我父亲一直梦想开发一个计算机围棋程序，我开始思考需要掌握什么知识才能实现这个目标。后来发现DeepMind正在做这件事，这让我了解到AGI。加入DeepMind后，我参与了AlphaGo、AlphaZero、MuZero等项目，最近还参与了AlphaCode和AlphaTensor项目。
AlphaProof 的工作原理
00:02:49
Sarah Guo:
让我先提供一些背景信息。对于那些像我这样不是超级数学天才的听众来说，IMO是最古老和最负盛名的青少年数学竞赛。比赛包含6道难到不可思议的题目，而AlphaProof今年取得了令人惊叹的成果，成功解决了其中的4道题目。我想请你谈谈，数学和IMO这类问题与下棋等搜索问题相比有什么不同？
Laurence Sartran:
首先，在棋类游戏中，你是和其他人对弈，这让游戏变得很有趣。比如在我们开发AlphaGo和AlphaZero这些算法时，我们实现了自我对弈，这样你总能找到一个恰好和你水平相当的对手。当你尝试学习数学时，这种方式就不太适用了，因为你并没有真正的对手。数学几乎是一种纯粹的认知活动，你能做的就是不断思考。你可能没法真正到现实世界中做实验。数学家们说睡一觉让潜意识思考问题是个好主意，这确实能带来新想法，但大部分还是需要思考。所以当你面对一个非常困难的问题时，关键就在于如何去尝试解决它。
Sarah Guo:
能否向我们的听众介绍一下Alpha Proof的整体架构？我们的听众大多是技术领域的从业者，但也包括更广泛的商业领域听众。
Laurence Sartran:
让我从AlphaZero开始介绍。AlphaZero最初是我们为解决完美信息棋类游戏而开发的程序。它基于强化学习算法，包含三个核心组件：神经网络、大规模强化学习（从试错中学习），以及规划和搜索组件（用于在当前情况下搜索最佳答案）。
我们发现，如果能够处理无限动作空间，就可以将原本用于搜索棋步的方法扩展到搜索证明步骤。这就是Alpha Proof的基本思路，它的动作空间是生成证明的步骤。我们使用形式化语言，也就是用代码来书写数学，这种方式最近变得很流行。当证明完成时，机器会给出反馈，表明证明是否正确。一旦找到正确的证明，我们就可以用它来改进神经网络，形成一个自我提升的循环，解决越来越难的问题，学习更多数学知识。这就是AlphaZero的思想如何应用到数学上的高层次概述。
00:06:27
Sarah Guo:
你们的公告中有个有趣的细节，有些问题几分钟内就能解决，而其他问题需要三天。你能描述一下数学整体的搜索空间，以及Alpha Proof在不同数学领域的优势吗？
Rishi Mehta:
数学的搜索空间比象棋等棋类游戏要大得多。有人可能认为写数学证明就像从已知技巧中选择，但实际上很多证明需要非常规的构造，比如凭空创造一个函数或找到特定的表达式操作方法。即使是重写表达式，也有无限多种可能性，但只有少数方式能推进证明。有些问题需要数十年的理论建设和全新视角才能解决。
在IMO的四个类别中——代数、数论、组合和几何，我们在代数和数论方面最强，组合方面相对较弱，但仍能解决一些IMO组合题。今年的比赛中我们没有尝试几何题。
我们开发了一个叫test-time RL的方法来处理这个巨大的搜索空间。当遇到无法直接解决的问题时，系统会构造很多相近的变体问题并尝试解决。如果能解决任何一个变体，就从中学习经验，逐渐接近原问题的解决方案。这就像科学家面对新问题时，可能需要做很多针对性实验来学习问题本身，然后逐步攀爬到解决方案。那些需要三天才能解决的问题，就是通过这种方式，我们不断尝试变体，一点点进步，最终经过数天的计算才找到解决方案。
AlphaProof 面对的挑战
00:09:28
Elad Gil(主持人):
我想了解AlphaProof在扩展性和解决问题范围方面的局限性和方法。这个问题有两个维度：一方面，它在代数等领域已经表现得相当出色；另一方面，在几何等其他数学领域可能需要新的训练数据。你们已经取得了令人印象深刻的成就，我很好奇你们如何看待显著提升性能所需要的关键因素，以及未来发展的障碍。
Thomas Hubert:
AlphaProof最主要的局限是无法进行理论构建。它不能发明理论，而是进行证明。比如在数论领域，它无法构建必要的复分析理论来推导结果。我们目前通过生成问题变体并解决这些变体来提高性能，这使我们能够解决原始的目标问题。
理论构建是需要进一步发展的一个组成部分。这可能是另一个维度。一些组合数学问题可能会以晦涩的方式呈现，但需要说明的是，这并不是所有组合数学问题的特点。本质上，组合数学问题都是关于计数的问题。比如说，如果你在抽屉里有40只袜子，要计算有多少双，这个问题可能会以某种晦涩的方式呈现。如何理解这些问题的含义是一个主要难点，而解决方案也比较复杂。如何最好地处理这类问题仍然是一个开放性问题。
Laurence Sartran:
我认为这在某种程度上与理论构建有一点联系。某种程度上说，目前的困难部分在于，我们使用的库中缺乏表达某些概念所需的工具。比如，如果我们有专门用于表达agent、environment、strategy等概念的工具，很多组合问题的描述就会变得简单得多。由于这些工具当前并不存在，自动形式化系统需要在真正开始形式化问题之前，先构建这些基础概念。这意味着我们需要具备开发新的定义、新的数学对象的能力，并且能够推导它们的性质、证明等相关内容。
00:12:09
Elad Gil:
1900年希尔伯特提出了著名的23个问题，这些问题定义了当时他认为对数学重要的领域和未解决的问题。我想问，是否有类似图灵测试这样的标准问题？
Laurence Sartran:
这是一个很好的问题。希尔伯特的问题完全定义了20世纪的数学发展方向。现在的千禧年七大难题是另一个类似的尝试，到目前为止，它定义了21世纪数学的一个可能发展轨迹。这是一个很难预测的问题，因为我们的思维往往是线性的，但从AI领域的经验来看，我们应该用指数思维来思考，因为事情可能会变化得很快。同时，我们对某些问题的难度完全没有概念，比如黎曼猜想，我们甚至不知道它比我们现在的能力高出2个数量级还是3个数量级。
因为我们没有存在性证明，所以很难估计这类问题的实际难度。我认为解决这些问题需要创造全新的数学理论和方法。如果要让AlphaProof达到这个水平，这种能力要么自然产生，因为在证明更难的问题时，你需要能够引入新的数学对象来分解问题。我们已经在IMO的小规模问题中看到这种情况，这种能力可能会在解决问题的过程中自然产生，或者我们需要明确思考如何构建理论以及如何引导AlphaProof发展这种能力。
Sarah Guo:
为了帮助不太熟悉未解决数学问题的听众理解，黎曼假设本质上预测了素数遵循特定的分布模式，这具有重要意义。
为什么要解数学题？
Sarah Guo:
让我们来思考一下为什么要研究数学领域。这里有很多有趣的假设：一是数学领域本身，我很好奇你们想解决什么问题；另一个前提是这种推理能力的进步可能会迁移到其他领域，无论是科学还是更多基于语言的、不太容易验证的非代码、非规则的领域。你们想把这项技术发展到什么方向？
00:15:11
Laurence Sartran:
我虽然不是一个数学家，但数学一直是我在学生时代最喜欢的学科。
我认为研究数学有两个主要原因。首先，数学被描述为宇宙的语言，它在描述和预测自然世界，以及塑造自然世界方面都展现出了强大的力量。实际上，数学是我们现在使用的所有技术的核心，所以对数学有良好的理解对于理解我们当前的世界来说非常重要。
另外，数学需要推理、泛化、抽象等能力，这些都是我们在讨论认知AGI时会考虑的关键能力，这可能是通向AGI的一条路径。虽然数学是一个受限的领域，但它具有无限的复杂性，考虑到它可能带来的所有潜在影响，投入大量精力研究它是值得的。
Thomas Hubert:
让我分享一下我的个人动机。我一直对如何让系统通过思考更多来提升性能这个问题很感兴趣。我在Metropolitan Station的研究中观察到，无论是在扩散模型还是在环境探索的导航代理中，系统都能通过更多思考来获得更好的表现。
数学领域，特别是在证明定理方面，AlphaProof似乎是仍然存在的最大挑战之一，我们还有很长的路要走。其中一个关键要素就是找到思考更多的方法。这种思考可以是更多的搜索，可以是testimony，甚至可能发展到让代理能够提出自己的理论。这就是为什么我选择数学作为测试思考更多能力的领域。
00:17:42
Rishi Mehta:
理解AGI的一个重要原因是为了揭示宇宙的奥秘，探索那些深层次的问题。比如，为什么事物会以现在的方式运作？我们为什么会在这里？我为什么有意识，这一切是怎么回事？
纯数学问题的研究就是一个很好的例子，已经有很多人在从事这样的工作。他们将数学视为寻求真理的方式。人们追求这些问题往往不是因为它们有实际应用，而是想知道真正的答案是什么，想理解为什么这些事物会以这种方式运作。比如解决黎曼猜想这样的问题，就具有纯粹追求真理的特质，这很吸引人。
Elad Gil:
在数学和科学领域，有着为了追求知识本身而研究的悠久传统。就像Sarah提到的数论在密码学中的应用，我们现在也看到零知识证明在加密货币领域中不断涌现出新的应用。群论和代数理论最初是独立发展的，后来在量子力学中得到了应用并进一步发展。对于你们正在进行的研究工作，是否有特别令你感兴趣的应用领域，还是主要出于对理论研究本身的热爱？
Laurence Sartran:
这是个好问题。我想，答案可能要取决于我们每个人。对我来说，一个动力是向数学家学习，了解他们在当前数学世界中感兴趣的内容。
最近我在阅读一个叫做Lang links program的项目，它试图连接数学的不同领域。这有点像物理学中寻找统一理论一样，试图在数学中找到一个统一理论，将数论、几何等不同领域连接起来。也许在这些领域背后，存在着某种更统一的东西。我个人很喜欢这些抽象的想法，尽管可能我并不是很理解它们。我会非常想要了解数学家们关心的内容，他们之间可能也会有不同的观点。
00:19:59
Sarah Guo:
我认为他们会不同意。比如看历史上的例子，当Bombelli开始研究虚数时，他被当时更重要的数学家们完全嘲笑。而多年后，我们通过虚数理论发展出了交流电，并能够用它来描述电力系统。我认为这是一个很有趣的问题，如果你有一台机器能够发展出自己的定理，你要把它引向哪个方向？从兴趣或实用性的角度来说，这最终是一个很大的问题。
Thomas Hubert:
我对验证这个领域特别感兴趣。目前我们开发软件时，写完代码后编写测试，当测试通过时我们就基本满意了。但问题是，有时bug甚至安全问题也会通过测试。更好的方法是在代码中直接表达算法应该验证的属性，并且能够证明算法确实验证了这些属性。
这种方法已经在Agenix密码学等关键领域使用，但目前需要人工完成。我认为如果验证能够更普遍地使用，并且我们能够消除人工编写这些验证的瓶颈，软件行业会更好。如果我们能有专门的工具来帮助处理这些证明的细节，这将是一个重大进步。
Rishi Mehta:
我认为另一个令我兴奋的应用领域是这项技术向其他领域的迁移。这里有两类参与者：一类是将这个agent通过训练获得的数学推理技能迁移到其他领域，因为数学对于工程、科学等领域都是至关重要的。另一类是我们在这里开发的技术，比如说扩展RL以及如何利用大量推理时间进行计算的方法，这些看起来都能广泛应用于很多其他问题。
强化学习中的验证正确性
00:22:05
Sarah Guo:
我想问一个更具推测性的问题。我们一直在讨论数学、代码等可形式化和可验证的领域。这些在语言领域中如何应用？AI能让内容变得更有趣吗？判断内容是否有趣比写出一个好的单口相声段子要容易得多。这是一个很有启发性的例子，你对如何在RL方法中验证正确性或质量有什么见解？
Laurence Sartran:
有些领域存在客观真理，有些则没有。比如有趣这个概念是一个模糊的人类概念，也许外星人会有完全不同的幽默感。对于这类问题，我们只能通过人类来获得基准，而在某些其他领域，现实世界可以作为基准。
RL框架让我们思考奖励来源的问题。有时奖励来自现实世界，有时可以完全确定，有时则来自人类。当可以进行机器验证时，我们能达到与人工验证完全不同的规模。特别是对于幽默这样的领域，每个人都可以对什么是有趣发表意见，这里仍有很大的扩展空间。RL框架是思考这些问题的很好方式，我们的一些工作可以迁移到这个领域，但那些依赖完美验证的部分可能不适用。
Sarah Guo:
在可验证的领域中，人类评分或输入对于显式描述或标注推理有什么价值？比如说，如果我们能无限制地请陶哲轩（Terry Tao）为我们做标注，这会有用吗？我们应该如何看待这与增加搜索量和改进形式化之间的关系？
Thomas Hubert:
AlphaProof目前的运作方式是自主发现证明，当证明有效时，它会从中学习并发展出自己的风格，这种风格被认为看起来相当陌生。如果有无限访问陶哲轩的机会，我们可以创建既正确又具有人类认为的优雅性的证明。我们可以在有效证明集合中进行优化，使证明更适合教学目的。在有效证明空间中仍有偏好选择的余地。
Sarah Guo:
这实际上是一个相当严厉的说法。因为这只是一个偏好问题，而不是能力提升的问题。如果我们能获得新知识，证明看起来陌生又有什么关系呢？虽然可理解性在这种情况下似乎有用。
Thomas Hubert:
是的，我只是说这是其中一个角度。有了更多的监督数据，我们可以避免探索问题，并转化所有已知的人类证明。这肯定会让系统变得更好，并节省多年的计算时间。随着时间推移，通过计算和理论构建，我们可能能够重新发现已知的证明。我们可以使用自动化，但它能提供我们无法通过其他方式获得的信号。随着时间和计算理论的发展，我们可能能够重新发现一些已知的证明。
00:26:34
Rishi Mehta:
这是个很有趣的问题，因为它突出了专家人类数据和RL数据的互补性。这在language models中特别明显，因为它们通过在大量人类数据上预训练获得了很强的人类先验知识。当我们对它们进行RL训练时，它们能够在这些人类先验的基础上继续发展，形成自己的解决方案风格，就像Alpha Proof做到的那样。
在这个项目中，我们发现少量珍贵的人类数据就能很好地引导agent的行为，让它从零开始快速达到一个更高的水平，从而能更高效地与环境交互。在此基础上，它能继续发展，用自己的风格达到或超越人类水平。我觉得这可能就是LLMs结合RL的未来发展方向——专家人类数据帮助LLM从一堆什么都不会做的权重发展到令人惊讶的强大水平，然后RL将其推向超人类水平。
AI 如何能够促进数学家之间更多的合作
00:27:53
Elad Gil:
我认为是庞加莱，有一位数学家是最后一个掌握所有数学知识的人。现在，我们有了可能在单个程序中包含所有数学知识的AI系统，它不仅能帮助检查证明，还能推动数学家的研究进展。特别是在更深奥的领域，能够验证或检查证明的专家非常少。那么，目前有多少数学家能够使用Alpha Proof？你们是如何考虑与数学界进行日常互动的？
Laurence Sartran:
目前数学家还无法访问AlphaProof。坦白说，我们现在完全无法与Terry Tao这样的数学家相比。我们已经证明系统可以几乎从零开始学习数学，达到令人印象深刻的高中水平，但我们需要继续扩充知识库来提高实用性。
Terry Tao在最近一年的访谈中提到，数学领域的合作规模相对较小，大多数论文只有1-2位作者，最多5位。这是因为验证他人的工作非常耗时。但如果有形式化系统来检查工作，就可以像天文学领域那样，即使是生活在偏远地区的业余爱好者也能参与合作。你不需要直接信任合作者，而是信任机器的验证结果。如果机器确认证明正确，那就是正确的。这样不仅可以促进更多人之间的合作，还可以实现人类与AI之间的协作。这是我们正在思考的方向之一。
我们在想，也许我们可以与这些项目进行合作。目前我们是这样考虑的，我们希望能像一个研究生那样，让数学家们给我们一些研究问题。这与理论构建有关。目前我们还不太擅长提出正确的问题，所以我们真的希望能依靠整个数学界来提出他们关心的问题，看看我们是否能帮助解答这些问题，哪怕只能提供一点点帮助。
AlphaProof证明的一个案例
00:30:45
Sarah Guo:
我在成长过程中也是一名围棋选手，所以看到围棋比赛中那些如你所说的陌生的下法，让我感到非常有趣。
在AlphaProof中，是否有什么让你感到陌生或令人惊讶的发现可以分享？
Rishi Mehta:
好的。让我给大家展示一下AlphaProof对IMO第6题的部分证明。我觉得在屏幕上展示会更容易理解。这是第6题。IMO通常有6道题目，其中第3题和第6题是最难的。这道题不仅是今年最难的题目之一，而且是IMO历史上最难的题目之一，因为500多名参赛者中只有5人成功解答。所以你们知道，这真的非常难。
我们可以快速过一下这道题的内容，因为在我们现有的时间内完整的证明可能难以理解。但我会指出我想出的一个很酷的构造。这道题讨论了一个叫做Aquasulian的函数定义。Aquasulian并不是一个真正的数学术语，这是个典故，因为比赛举办地Bath在罗马时期被称为Aquae Sulis。
题目给出了两个方程来定义Aquasulian函数，我们需要证明存在某个整数C，使得对任何Aquasulian函数F，这种形式的有理数最多有C个不同的值。这个表达式本质上是函数的偶部分。你可以给任何Aquasulian函数输入很多有理数，可能会得到无限个、5个或3个不同的值。题目要求证明存在一个上界C，并且要找出这个上界的具体值。
什么是C？在尝试回答这类问题时，一个常用策略是找出C的上界和下界，然后证明它们收敛。在证明的这个阶段，Alpha Proof已经证明了C小于等于2，这个证明本身很有趣，你们可以在我们的博客文章中查看详细内容。现在，Alpha Proof需要判断C到底是1还是2。
证明C可以等于1是很简单的，难点在于证明是否存在满足这些性质的函数F，使得C等于2。你们可以暂停一下，试着找找这样的函数F，看能否找到使F(r)+F(-r)有两个不同值的情况。有趣的是，即使是Fields奖获得者Tim Gowers也花了几个小时都没能找到这样的构造。当然，这并不是说AlphaProof比Gowers更擅长数学，但这确实说明了问题的难度。
AlphaProof找到了这个特殊的构造：F(x)=-x+2⌈x⌉，这是一个看起来很特别的函数，我已经把它画出来了。有趣的是，当我们代入r=-1和r=1/2时，这个函数会得到两个不同的值，这就证明了C必须等于2。
这可能是AlphaProof解决过的最难的问题，它使用了一个很酷的特殊构造，依赖于seal函数。
数学和人工智能的未来：对数学爱好者和研究人员的建议
00:34:36
Rishi Mehta:
形式化数学将变得越来越重要，不仅因为AI将成为形式数学中的强大工具，也因为它正成为数学家之间合作的方式。虽然目前在数学界使用Lean的人还是少数，但这个群体在不断增长，AI将加速这个趋势。我不是数学家，所以不敢妄加评论，但我的建议是尽早学习Lean。
Laurence Sartran:
我意识到Lean是一个很好的教育工具，因为大多数证明都是按照作者的抽象层次来写的。如果作者认为某个步骤是显而易见的，就不会解释。但在形式化语言中，你可以根据需要深入了解细节。这让你能够按照自己的水平来学习。你还可以进行自我练习，特别是在学习抽象数学时。数学难以解释是因为它很抽象，你可能无法确定自己的推理是否正确。在纸上做题时，你需要找老师确认，这可能需要很长时间。但使用形式化语言，你能立即知道哪些还需要证明，是否有推理错误。所以即使是出于教育目的，这也很有价值。
Thomas Hubert:
这不是建议，更像是一种推测。有人说数学家分两类：建立理论的和证明定理的。我理解证明定理有时也需要建立理论，就像费马最后定理那样。在建立理论方面，人类的创造力、品味和技能似乎有更大的发挥空间。
Sarah Guo:
我在这个问题上有些困惑。在AI不断发展的多个领域中，品味似乎变得越来越重要。比如陶哲轩在研究素数等差数列时的品味，这导致了方法和工具的进步。让人培养好品味是比'确保学习Lean'更微妙的建议。这与你们的工作很相似，在某些领域应用计算时，会抽象地改进解决问题的能力。我想也许正如你说的，我们都需要做更多的test time RL。我不知道我们是否都能培养出这种品味，即使它看起来有用。
Rishi Mehta:
我看到一个很有意思的观点：随着机器在寻找答案方面变得越来越好，我们人类需要在提出问题方面变得更好。这些系统本身并没有对什么问题是有趣的这种认知。关键在于如何将一个大问题分解成更小的、可能更有趣的问题。这种情况不仅存在于数学领域，在很多领域都是如此。比如作为一名软件工程师，我发现自己的工作越来越多地不是关注那些低层次的细节，而是做出好的高层次决策，然后让工具来协助完成这些工作。这种情况很可能会在越来越多的领域出现。
交流与合作
如果希望和我交流讨论，或参与相关的讨论群，或者建立合作，请私信联系，获取联系方式请点击 -> 联系方式。
本文于2024.11.15首发于微信公众号
