We're sunsetting PodQuest on 2025-07-28. Thank you for your support!
Export Podcast Subscriptions
cover of episode AI and the Future of Math, with DeepMind’s AlphaProof Team

AI and the Future of Math, with DeepMind’s AlphaProof Team

2024/11/14
logo of podcast No Priors: Artificial Intelligence | Technology | Startups

No Priors: Artificial Intelligence | Technology | Startups

AI Deep Dive AI Chapters Transcript
People
L
Laurence Sartrant
R
Rishi Mehta
T
Thomas Hubert
Topics
AlphaProof 团队成员介绍了 AlphaProof 的工作原理、优势和局限性,以及在数学推理方面的应用和未来发展方向。AlphaProof 基于 AlphaZero 的强化学习算法,通过将数学证明过程转化为动作空间的搜索来解决数学问题。其优势在于能够解决复杂的数学问题,尤其是在代数和数论领域表现出色,但目前在组合数学和几何方面能力相对较弱,并且缺乏理论构建能力。团队成员还讨论了 AlphaProof 的可扩展性、应用领域以及与人类数学家的合作方式。他们认为 AlphaProof 可以应用于代码验证、科学研究等领域,并促进数学家之间的合作。此外,他们还分享了 AlphaProof 在解决 IMO 难题时的一些意外发现,例如其独特的函数构造。 团队成员还探讨了数学研究的动机,包括追求真理和发展通用人工智能 (AGI)。他们认为,解决纯数学问题有助于探索宇宙的奥秘,而数学推理能力的提升也有助于 AGI 的发展。在应用方面,他们对代码验证和将 AlphaProof 技术应用于其他领域表示了期待。他们还讨论了在没有明确标准答案的领域(如幽默)中,人类评价的重要性,以及如何将人类输入与强化学习相结合。 团队成员就如何利用 AlphaProof 提升数学研究和教育提出了建议。他们建议数学家尽早学习 Lean 语言,因为它在数学研究和教育中越来越重要。他们还指出,随着 AI 在数学领域的能力提升,人类需要更加关注如何提出有意义的问题。

Deep Dive

Shownotes Transcript

嗨,各位听众,欢迎收听《No Priors》。今天我们邀请到了来自 DeepMind AlphaProof 团队的 Thomas Hubert、Rishi Mehta 和 Laurence Sartrant。AlphaProof 是一个新的 AI 系统,它可以发现和验证数学证明,延续了 DeepMind 在国际象棋和围棋方面的早期成功,致力于解决 AI 最大的挑战之一:数学推理。

在今天的节目中,我们将探讨 AlphaProof 的工作原理、它对数学和 AI 的影响、更多关于测试时间强化学习 (TestTime RL) 的内容,以及这揭示了机器学习进行严格推理的能力。非常高兴能邀请到你们三位。欢迎。感谢你们的邀请。也许你们可以先谈谈你们的背景,以及你们是如何走到一起参与 AlphaProof 项目的。我是 Rishi,我是 AlphaProof 的技术主管之一。我从事计算机科学和机器学习已经有一段时间了。

我是一个国际象棋棋手,我偶然发现了 AlphaZero 的论文,并看到该代理程序产生的一些国际象棋游戏,我发现它非常鼓舞人心,我认为这正是我需要从事的工作。创造出一些美丽、超凡脱俗、几乎是异类的作品感觉很神奇。我来到 DeepMind 和 AlphaZero 团队,Thomas 领导着这个团队,

呃,正在研究数学,这就是我开始接触数学的方式。是的,我在职业生涯早期就开始在行业工作了,呃,在,在我的早期职业生涯中。嗯,

我从事分钟检测计算机网络的工作。我从事广告投放工作,并转向 AI 研究。在那里,我一直对能够花费更多计算资源来解决更难的问题或进行更多思考的系统感兴趣,而数学似乎是实现这一目标的完美途径。是的。在我这边,我,嗯,

我实际上是一个围棋棋手。所以从 10 岁起,我没有进行编程,而是一直在玩围棋。在我的青年时期,我玩了很多围棋。然后在某个时候,我父亲也梦想创建一个计算机围棋程序。

所以我一直在思考,为了能够创建一个计算机围棋程序,我需要了解什么?然后我意识到,也许当时正在构建它。这就是我发现 DeepMind 和 AGI 的方式,这就是我加入公司并参与 AlphaGo、AlphaZero、MuZero 这类工作的方式。

最近我们还参与了 AlphaCode 和 AlphaTensor 的工作。所以,你知道,这在很久以前,呃,但我们已经知道,转换器正在改变一些事情的处理方式。所以我们,你知道,我发现在数学中,是的,你可以得到这种完美的可变性,并且通过 AlphaCode,我们意识到我们可以生成很多好的代码。所以在那个时候,考虑一下,嗯,

数学方面的潜力是很自然的。你能对比一下吗?也许作为背景,对于任何像我一样不是超级酷的数学天才的听众来说,IMO 是最古老的

最负盛名的青年数学竞赛。有一套六个问题。它们感觉难到令人难以置信。AlphaProof 取得了令人惊叹的成果,今年解决了六个问题中的四个。你能谈谈数学,特别是 IMO 作为与游戏博弈和其他搜索问题(如国际象棋)相比的问题吗?

我认为,你知道,首先一个很大的区别在于,在棋盘游戏中,你与某人对抗,这在棋盘游戏中非常有趣。例如,当我们进行 AlphaGo 或 AlphaZero 算法时,我们可以真正做到自我博弈。你总是可以与一个恰好是你优势的对手对抗。事实证明,这是一个强大的想法。当你试图学习做数学时,在某种意义上,你知道,你并没有真正的对手。

你只需要思考它。数学有点特殊,因为它几乎像是一种纯粹的认知性事物,你可以,你知道,你唯一能做的就是多思考。你知道,也许你不能真正进入现实世界并进行实验,但是

我想数学家们说,有时小睡一下让你的潜意识思考问题是一件好事。这是一种想出新主意的好方法。但这主要关乎思考。所以,你知道,当你遇到一个非常棘手的问题时,就会出现一个问题,即如何去尝试解决它。也许现在是时候请你为我们的听众描述一下了,他们中的大多数是技术人员或在科技领域工作的人,但也包括更广泛的商业受众。就像,你知道……

AlphaProof 的整体架构是如何工作的?是的,当然。AlphaProof 基于这个叫做 AlphaZero 的东西。所以也许我先从这里开始。AlphaZero 是我们开发的一个程序,基本上可以处理完美信息棋盘游戏。它的工作方式也基于强化学习算法。所以你可以把 AlphaZero 想成三个组件,比如一个神经网络。

二,一种大规模的智能学习速率,基本上是从试错中学习。三,它还有一个规划和搜索组件,用于尝试在给定当前情况的情况下,尝试搜索最佳答案。

事实证明,你知道,也许我们在下国际象棋时并没有想象到这一点,但是如果你可以处理无限的动作空间,那么,你知道,与其寻找国际象棋的走法,不如寻找,例如,证明的步骤。

这就是我们在开始 AlphaProof 时试图做的事情。基本上,我们的动作空间是生成证明步骤。也许非常重要的是,我们使用形式语言来做到这一点。基本上,另一种说法是,我们使用代码来编写数学。最近这变得非常流行。

这样做的好处是,一旦证明完成,机器就会给你一个信号,告诉你你的证明是否正确。所以我们可以搜索正确的证明。一旦我们找到一个正确的证明,我们就可以从中学习。

并获得更好的神经网络,并进入这种自我改进的循环,以解决越来越难的问题,并学习越来越多的数学知识。在非常高层次的图景中,这就是它的工作方式,以及 AlphaZero 背后的思想是如何适应数学的。你们公告中一个有趣的细节是,你知道,有一系列问题,在几分钟内解决了一个问题,三天解决了其他问题。

你能不能描述一下数学的搜索空间,或者 AlphaProof 在哪些领域比其他领域更好,比如数学中的推理类型?与国际象棋或其他棋盘游戏相比,数学中的搜索空间相当大。所以,你知道……

有些人可能会认为编写数学证明就像在每一步都从一堆已知的技巧中挑选一样。但事实上,在许多证明中,你必须想出一些不平凡的构造,比如你必须凭空发明一个函数,或者你必须想出一些方法来操作,即使你只是重写一个表达式。

你可以用无限种方式重写它,而只有少数几种方式可以重写它才能在证明上取得进展。有时,思考一些新颖的问题需要几十年的理论构建,并从全新的角度来解决它,才能找到帮助你解决它的角度。所以在这种意义上,你知道,为什么有很多

数学问题很容易陈述,但经受住了时间的考验,因为它们甚至已经未解数百年了,这是因为搜索空间在大多数情况下并不容易导航。

我认为 AlphaProof 在 IMO 类别中擅长的是它总体上都擅长。IMO 问题分为四类。有代数、数论、组合数学和几何。它最擅长的两类是代数和数论。它在组合数学方面相对较弱,尽管它在一些 IMO 组合数学问题上做得相当好。今年的竞赛中,我们没有将其应用于几何。并且

它导航这个巨大搜索空间的方法之一是我们想出的一个想法,我们称之为测试时间强化学习 (TestTime RL)。所以这是一个想法,比如——

假设你遇到一个你不知道如何解决的问题,你可以用你现在所知道的知识进行一些搜索,并且你无法找到它的证明。然后代理程序所做的是,它构建了该问题附近许多不同的变体,并尝试解决所有这些变体。如果它设法解决了任何一个变体,它就会从这种经验中学习,并逐渐接近解决原始问题。你可以把它想象成……

当遇到一个新的科学问题时,你从其他问题中获得的许多先验知识可能并不直接适用于它。因此,你必须对这个问题本身进行非常专门的实验才能了解它。然后你会朝着这个问题的解决方案攀登。所以这个过程有点模仿了这一点。所以当你谈到三天后解决的问题时,

这些问题在这个循环中:我们无法用基本网络解决它,但我们提出了许多、许多变体。我们尝试所有这些。我们变得越来越好,越来越好,越来越好。然后我们在推理时间计算后,通过爬坡的方式到达最终的解决方案。AlphaProof 的局限性或扩展方法是什么?或者说,增加 AlphaProof 可以解决的问题集?我想这有两个方面。

正如你所说,它已经做得相当好的领域有一组,代数和其他领域。然后还有一组领域,你可能需要新的训练数据形式或其他东西,比如几何的某些方面或其他数学领域。我有点好奇你如何看待从这里开始大幅提高性能所需要的东西。显然,你们所做的事情令人难以置信。我只是很好奇你如何看待未来增长的障碍?

也许 AlphaProof 最主要没有做的事情是理论构建。它不投资于理论。AlphaProof 只装备了这个。

数论将无法提出进行数论推导所需的复分析。所以这是我们甚至没有重新生成方差并通过解决这些问题而变得更好的主要方面之一,这使我们能够解决感兴趣的原始问题。理论构建是一个组成部分

这将需要你的父亲。也许是另一个维度。

组合数学问题可以用某种模糊的方式来陈述。这并不意味着所有组合数学问题,提醒一下,组合数学问题都是关于计算事物数量的。例如,如果你抽屉里有 40 只袜子,你有多少双?它可以用某种模糊的方式来陈述,以及如何翻译它们是一个主要难题,然后如何

所以它有点笨拙。如何最好地解决这个问题仍然是一个悬而未决的问题。我认为这与你的理论构建有点联系,因为例如,你知道,如果在某种意义上,

部分困难来自于这样一个事实,即你表达这些事物所需的工具实际上并不存在于我们正在使用的库中。例如,如果你有一些表达的东西,你知道,什么是代理,什么是环境,什么是策略,那么,例如,许多组合数学问题将更容易陈述。

但是因为目前还不存在,所以在某种意义上,自动形式化需要事先提出所有这些东西,然后才能真正形式化这个问题。所以这就是,也许这就是与这样一个事实相关的,你知道,在某些时候,你需要能够开发新的定义、新的数学对象,提出它们的属性和证明等等。所以我想,我认为是 1900 年,大卫·希尔伯特提出了他著名的 23 个问题问题

它们定义了当时他认为对数学很重要的许多重要领域,以及当时重要或热门的未解问题。

或者说,作为一般性问题,是否存在某种图灵测试等价物?这是一个极好的问题。这完全定义了 20 世纪的数学,也许千禧年问题,七个千禧年问题中只有一个已被解决,这是对定义什么的另一次尝试

你知道,21 世纪数学可能的一种轨迹是什么?我们解决这个问题的机会有多大?这是一个非常难的问题,因为我们知道,你知道,我们的大脑线性地思考,但我们从在 AI 上工作的经验中知道,我们实际上应该尝试指数地思考。

事情可能会很快改变。与此同时,你知道,我认为我们不知道像黎曼假设这样的东西有多难。是,你知道,是两个数量级,三个数量级吗?也许它比我们现在能做的要远 10 个数量级,对吧?

因为我们没有存在性证明,所以很难估计这实际上有多难。但我认为,解决这个问题将涉及创造全新的数学、全新的理论等等。所以如果我们想让 AlphaProof 一直走到那里,我认为这是我们需要……

要么它出现,这是可能的,因为你知道,为了证明更难的问题,你开始需要能够引入这种新的数学对象来分解问题或问题。我们已经看到这在 IMO 中小规模地发生了。但很有可能,你只需要尝试解决问题就能出现,或者可能,你知道,我们必须更明确地思考构建理论意味着什么,以及我们如何鼓励

如何接近做这些事情。是的,对于那些不花太多时间研究未解数学问题的听众朋友们,为了更好地理解一下,黎曼假设本质上预测素数遵循特定的模式。

并且它具有重要的意义。也许我们可以从那里开始思考,当你开始将数学作为搜索空间进行研究时,有很多有趣的假设,比如为什么要去研究数学。一个是领域本身,对吧?所以我很想知道你们是否有什么想研究的问题。另一个前提是,数学

这种推理的进步将使我们能够将其转移到其他领域,无论是科学,还是我们认为更像基于语言的、不太可验证的非代码、非规则的领域。你们想把这个带到哪里去?我不是数学家,所以我没有绝对想解决的问题,但它一直是我学生时代最喜欢的科目。

我认为,是的,你是绝对正确的。至少有两个主要原因可以解释为什么你可能想要在数学上花费大量时间。一个原因是,我想它被描述为宇宙的语言。而且,你知道,它在描述和预测自然世界方面都非常强大。当然,还有塑造它。你会看到,你知道,基本上我们看到数学是现在我们正在使用的所有技术的核心。所以对数学有很好的理解可能是一种

了解我们当前世界非常重要的事情。然后,当然,正如你提到的那样,你可以争辩说,你知道,

解决数学问题或,你知道,这需要,你知道,推理、泛化、抽象,所有这些我们在谈论认知 AGI 时都会想到的事情,将是,将是,是一条通往 AGI 的道路,这可能真的有助于 AGI 的发展。所以至少对我来说,你知道,这些也许是关于为什么数学

是一个特别有趣的话题,即使你知道数学好吧,让我们说它仍然是一个受约束的领域,但这种无限的复杂性实际上代表了很多东西,但它可能更糟,因为它是一种非常……专注的努力,因为它可能产生的所有潜在影响,我可以说一些关于我自己的情况……

我一直对创建通过更多思考而变得更好的系统感兴趣。我在机器翻译、文本扩散和导航代理中看到了这一点,这些代理发现了它们如何通过更多思考来更好地了解环境和世界。

数学似乎特别是在证明陈述方面。所以 AlphaProof 的核心似乎是最后几个重大挑战领域之一,我还有很长的路要走。当我

关键要素之一是找到一种更多思考的方法。这可能是更多地搜索,这可能是测试 MRL,也许下一步的更多思考将是如此多的思考,以至于代理会提出它自己的理论。所以数学作为更多思考的测试平台是我的动力。追求 AGI 的一个重要原因是揭开宇宙的秘密,你知道,比如,

为什么事情会按照它们的方式运作?我们为什么在这里?而且,你知道,我为什么有意识?发生了什么事?我想就像数学一样,解决这些纯数学问题,感觉就像我们已经……

就像,有很多已经这样做的人。他们将数学视为对真理的探索。就像,你知道,人们感知这些问题并不是因为它们通常有任何应用,而是更多地是因为,你知道,答案到底是什么?为什么这件事会这样运作?像你一样解决黎曼假设,感觉就像,你知道,一种对真理的纯粹探索,这很有吸引力。我想与之相关的是,在数学中,人们长期以来一直试图

或者在科学中,或者在科学和数学中,为了它们自身的目的,或者为了知识的追求而做事情。莎拉以数论及其在密码学中的应用为例。

零知识证明正在以不同的方式出现在不同的加密货币中。群论和代数随着时间的推移出现在量子力学中,并且是在之前开发的,然后在那里得到应用和进一步发展。从应用领域来看,你们对你们正在做的工作中最兴奋的具体领域有哪些?或者主要是因为对理论部分的热爱?

这是一个好问题。我认为我们可以,也许,你知道,也许答案取决于我们每个人。我认为我感兴趣的一件事是从数学家那里学习,你知道,他们感兴趣的是什么,以及他们在当前的数学世界中发现什么有趣的东西。所以,例如,你知道,我一直在阅读关于这个叫做 Langlands 程序的东西,它试图连接

不同的数学领域。它对我来说有点像,你知道,就像在物理学中,你试图寻找统一的物理学理论一样。它就像试图寻找统一的数学理论,也许,你知道,我们在这里有数论,在那里有几何。但是,也许背后有一些东西,你知道,更统一。所以我个人喜欢这些抽象的想法,即使我可能不太理解它们。

但是是的,我很想看看,你知道,数学家关心的是什么,他们之间也可能会有分歧。我认为他们会不同意,对吧?如果你看看历史上的例子,比如当 Vombelli 开始研究虚数时,他受到了当时更重要的数学家的完全嘲笑。并且……

许多年后,我们得到了交流电和描述电力的方法。我认为这是一个非常有趣的问题。如果你有机器,机器能够发展它自己的定理。你最终会把它指向哪里以获得兴趣或效用?这是一个非常大的问题。我特别感兴趣的一个领域是代码验证。

也就是说,目前当我们编写软件时,我们编写代码并编写测试,当测试通过时,我们相当满意。偶尔会出现通过测试的错误,甚至是安全问题。

如果我们可以用代码表达算法应该验证的属性,并用代码证明算法确实验证了这些属性,那就好多了。所以对于像航空电子、密码学这样的非常关键的领域,这已经做到了,这非常重要。它必须由人类完成。我认为如果……软件行业会处于更好的位置。

因为验证更加普遍。如果我们消除了瓶颈,那就是人类编写这些证明。所以如果人类能够通过专用工具得到支持,我们就可以处理这些证明的微型版本。我认为我们已经为我们迈出了重要的一步。我认为我感兴趣的另一个应用领域是这项技术向许多其他领域的转移。所以有两类参与者。一个是仅仅将数学推理技能

这个代理通过这种训练获得的技能转移到许多其他领域。而且,你知道,正如我们所看到的,数学对于工程和科学至关重要,并且,

等等。但同时,我们在这里开发的一些技术,例如扩展强化学习和找出如何花费大量推理时间来计算这些东西,感觉它对许多其他问题都非常适用。我将问一个更具推测性的问题。我们一直在谈论数学、代码和

呃,不容易形式化但可以形式化和验证的领域……你认为这在语言领域中适用多少?nai 能否创造出更有趣的东西,而且判断某事物是否有趣比编写一个好的脱口秀节目更容易,对吧?呃,所以我认为这是一个很有启发性的例子,但是,你对……有什么直觉吗?

利用关于在强化学习方法中验证正确性或质量的能力的一些学习成果?我想,你知道,正如你所说,有些领域存在基本事实,有些领域不存在基本事实。所以当它们不存在时,而且,你知道,比如幽默可能是一种,你知道,人类的

这是一个模糊的人类概念,也许那里有一些外星人。他们会有不同的幽默感。所以对于那些问题,我认为你获得基础的唯一方法是通过人类作为你的基础。

对于其他领域,也许现实世界是一种基础,然后你必须进入现实世界才能获得你的基础。但基本上,强化学习将允许你说明,“我的奖励来自哪里?”我想有时它来自现实世界,有时你可以完美地找到它,有时奖励来自人类,我认为这很好。

有一些技术基本上是我们开发的,从某种意义上说,当然,当你可以机器检查事物时,你可以以与必须询问人类不同的规模运行,即使我们有很多人类。所以可能仍然有很多扩展是可能的,特别是对于像幽默这样的事情,每个人都应该对什么是有趣的发表意见。

所以当然,例如,强化学习框架,我认为仍然是一个思考这些问题的伟大框架。

并且强化学习工作的一部分,也应该转移。也许我们依赖完美验证的地方,也许那不会转移到那个特定问题。在更可验证的领域中,对于人类评分或输入的空间在哪里?例如,如果你有……

无限地访问 Terry Tao 来为你做标记。这有用吗?或者我们应该如何看待它,而不是仅仅做更多的搜索和改进形式化?AlphaProof 目前的工作方式是,它发现它自己的证明,当它们有效时,它会从中学习并发展它自己的风格。

这被评论为看起来相当奇怪。因此,通过无限地访问领土,我们创建了有效的证明,并具有人类感知到的一些优点。

我们可以开始在有效证明的集合中优化,以获得对人类来说看起来不错的证明,用于可解释性,用于教学。所以在这个有效证明的空间中,肯定仍然有空间来证明人类可能更喜欢的证明。这实际上在某种程度上是一个相当严厉的陈述,对吧?因为这就像……

偏好与也许像,你知道,能力提升?如果我们有了新知识,我是否关心证明看起来是否奇怪?在这种情况下,可解释性似乎很有用,但是……是的,我认为这绝对是唯一的一个角度。有了更多有监督的数据,我们可以避免探索问题,我们可以翻译所有为人所知晓的证明,并且

这当然会使代理变得更好。这肯定会为我们节省多年的计算时间。我并不是说可解释性是我们唯一可以使用教条式转换的方式。但它可以为我们提供我们无法通过其他方式获得的信号。可以推测,随着时间的推移,计算、理论构建,我们也许能够……

也许应该重新发现那些已经知道的证明?我认为这是一个有趣的问题,因为它突出了专业人类数据和强化学习数据之间的互补性。我认为这在大型语言模型中尤其突出,因为大型语言模型具有非常强的人类先验知识,因为它们是在大量人类数据上预训练的。但是,当我们用它们进行强化学习时,它们就有机会利用这些人类先验知识,并在其基础上发展出自己的知识。

嗯,风格就像AlphaProof做的那样,我认为在这个项目中我们看到的一件事是,少量宝贵的人类数据可以非常有效地超越智能体的行为,并且可以将它从完全零的状态提升到更高的水平,在那里它可以更有效地与环境互动,然后超越它,也许可以与人类匹敌甚至超越人类,但它有自己的风格,我想就是这样。

我觉得这可能是强化学习与大型语言模型未来发展方向,专业人士将帮助大型语言模型从一堆什么都不会做的权重变成令人惊讶的强大模型。然后,强化学习将带你从那里到达超人的水平。我认为是庞加莱还是其他人,是最后一位了解所有数学或至少理解大部分数学的数学家。

突然之间,你拥有了一个人工智能或系统,它有可能在一个程序中囊括所有数学知识。它可以真正用作帮助检查证明的工具,它可以帮助数学家推进他们自己的研究。现在,如果有人证明了一些东西,如果他们在更偏门的领域,那么实际上能够验证或检查他们所做的证明的人并不多。现在有多少数学家可以使用AlphaProof?或者你怎么看待与数学界就该软件的日常使用进行互动?

非常惊人的进步。目前,数学家无法使用AlphaProof。老实说,目前我们根本无法与陶哲轩这样的人相提并论。我认为我们所展示的是,我们可以几乎从零开始学习一般数学,并达到令人印象深刻的高中水平。

然后,我们需要扩展我们的知识库,以便变得有用。但我不确定你是否看过陶哲轩去年的一些采访。他说,数学中一件有趣的事情是,合作规模相对较小。许多论文只有一到两位作者,最多五位作者。这是因为与更多数学家合作非常困难,因为你需要检查

他们在做什么。所以非常耗时。但是,如果你依靠一个形式系统来检查其他人的工作,那么你就可以像天文学一样,让一个业余爱好者住在偏远地区,你从未见过他。

然后你就不必信任他,在某种意义上你可以信任机器来检查工作。如果机器说这是一个正确的证明,那么它就是一个正确的证明。然后,在某种意义上,你可以开始与更多的人合作。这很酷,因为你可以开始考虑在许多人之间进行合作。

也可能包括人工智能,对吧?所以这可能是我们也在考虑的一种方式,就像,哦,我们能否与这些项目合作?目前,我们认为自己更像是一种,如果我们能成为一名研究生,那将是很棒的,数学家可以向我们提出问题。我认为这可能与目前的理论构建有关。

我们不太擅长提出正确的问题。我们肯定希望依靠整个数学界来提出他们关心的问题,看看我们是否能够在回答这些问题上提供一点帮助。我小时候也是围棋选手。所以,看到

看到李世石对战AlphaGo的比赛,正如你所描述的那样,围棋中出现了一些不可思议的招数,这对我来说也极其有趣。到目前为止,AlphaProof有没有什么让你觉得奇怪或意外的事情可以谈谈?当然,让我向你们展示AlphaProof为IMO的第6题提出的证明的一部分。如果我把它显示在屏幕上,你们会更容易理解。

这是第6题。IMO通常有六道题,第3题和第6题是最难的。所以这应该是今年IMO最难的题目之一。但它实际上成为有史以来最难的题目之一,因为500多名参赛者中只有5人成功解答。

所以,你知道,这真的很困难。所以我们可以很快地回顾一下这个问题在说什么。我不会讲解整个证明过程,因为在我们现在的时间里,它可能难以理解。但我会指出它提出的一种很酷的构造。这个问题谈到了函数是Aquasoulian的定义。Aquasoulian并不是一个真正的数学术语。这只是对巴斯(比赛举办地)曾经被罗马人称为Aquasulius这一事实的戏谑说法。但无论如何,他们给了我们两个方程来描述Aquasoulian函数。我们必须证明存在某个整数c,使得对于任何Aquasoulian函数f,

这种形式最多有c个不同的有理数。这有点复杂,难以理解,但本质上,这种形式是函数的偶数部分。它想说的是,你可以取任何Aquasoulian函数,并赋予它许多有理数,计算出许多有理数的表达式,你可能会得到无限个值,也可能得到五个值或三个值。

它要求你证明存在某个界限c,超过这个界限你不能有更多唯一的值,并且要求你找到这个界限c。所以,好的,这就是问题,c是多少?所以通常,当你试图回答这样的问题时,你可以使用的一种策略是显示c的上界和下界,然后显示这两个界限收敛,然后你找到c。

所以我要从AlphaProof已经证明c小于等于2的地方开始证明。这本身就是一个相当有趣的证明,如果你感兴趣的话,你可以在我们的博客文章中查看。但在证明的这一点上,AlphaProof必须决定,c是1还是2?

它必须决定这一点的方法是找到……所以证明c可以是1是很简单的。困难的是,是否存在任何Aquasoulian函数f使得c为2?而且,你可以暂停一下,尝试找到遵循这些属性的函数f,看看你是否能找到一个函数,你可以为其找到两个不同的f(r)+f(-r)函数值。

表达式。但有趣的是,蒂姆·高尔斯(Tim Gowers),我们的评委之一,也是菲尔兹奖获得者,尝试了这个问题几个小时,但他找不到具有此属性的函数的构造,当然,这并不是说AlphaProof在数学方面比蒂姆·高尔斯更好,但这只是突出了这个问题的难度。

AlphaProof提出了这个构造,即这个函数f(x)=-x+2C(x),这是一个看起来很奇怪的函数,我在这里绘制了它的图像。有趣的是,这个函数,如果你代入r=-1和r=1/2,你会得到两个不同的值。所以你可以看出,c必须等于2。

在我看来,这可能是AlphaProof解决过的最难的问题。这是一个非常酷、非常奇怪的构造,它依赖于这种C函数。非常酷。非常酷。我们可以从对今天从事数学工作并投入时间的人的建议开始,考虑到AlphaProof和相关的模型?形式化数学在未来将变得越来越重要,这不仅是因为人工智能将成为形式化数学中非常强大的工具,

一种数学形式,而且因为它正在成为数学家之间合作的一种方式,许多著名的数学家正在采用它。目前,使用Lean的数学家仍然只是少数,但这是一个不断增长的少数群体。人工智能只会加速这一进程。所以我想我不是数学家,所以我有什么资格给数学家建议呢?但我从外部的建议是,尽早学习Lean。 FRANCESC CAMPOY:我也意识到它是一个很好的教育工具,因为——

大多数证明都是以编写证明的人的抽象级别编写的。

例如,如果那个人认为这一步是微不足道的,那么你就不会有任何解释。但是,如果你用形式语言写出这个证明,那么你可以放大到适合你的细节级别。所以这是一点。你可以根据自己的水平学习更多。第二点是,你实际上可以与自己进行自我博弈。

从某种意义上说,你可能正在尝试学习数学中非常抽象的一部分。通常的情况是,很难解释数学,因为它相当抽象。然后你可能无法判断你正在做的事情是否正确。如果你在纸上做,那么你接下来能做的最好的事情可能是尝试找到某个人或你的老师。这可能需要你很多时间,对吧?才能得到一些反馈。

但是,如果你使用形式语言,那么你知道,你会确切地知道还有什么需要证明。如果你正确地做了这件事,或者你有点自欺欺人。所以即使是为了教育目的,我认为这也很有趣。这并不是建议,而是更多的推测。

有人说有两种类型的数学家,一种是构建理论的,一种是证明定理的。我理解为了证明定理,有时你必须构建整个理论,就像费马大定理那样。但我认为在构建理论方面,人类的创造力、品味、技能和……

比在证明方面有更大的空间。我在这里有点纠结的一件事是,在许多领域,人工智能正在攀登的山峰,我认为技术

似乎越来越重要。这可能是陶哲轩对问题的品味,因为如果你研究素数的算术级数,它实际上会导致方法和工具的进步。但我实际上认为这真的很……第一,这很有挑战性,因为告诉某人培养良好的品味比确保你学习Lean更细致入微,对吧?但第二,它也与你们一直在做的工作非常相似,在某种程度上,如果你观察你应用计算的行为,你会发现,哦,为什么不抽象地研究这个领域周围的一些问题,因为它会提高你解决问题的能力

问题,对吧?所以我想也许,正如你所说,我们都会做更多测试时间的强化学习。我不知道我们是否都会培养品味,即使这看起来很有用。我从某个地方看到过这个说法,那就是随着机器越来越擅长找到答案,我们将不得不越来越擅长找到问题。这些系统没有自己的

对哪些问题有趣的想法。给定一个大的问题,我该如何将其分解成可能有趣的小问题?而且,你知道,这可能不仅仅是在数学领域,在许多领域,即使作为一名软件工程师,我也发现,

我的工作越来越不是弄清楚这些低层次的细节,而是做出一些高层次的决策,工具可以帮助你做到这一点,这可能在越来越多的领域都是如此。非常感谢你们这样做,很高兴见到你们所有人,感谢你们这样做。

在Twitter上关注我们@NoPriorsPod。如果你想看到我们的脸,请订阅我们的YouTube频道。在Apple Podcasts、Spotify或你收听节目的任何地方关注该节目。这样你每周都会收到新的剧集。并在no-priors.com上注册电子邮件或查找每集的文字记录。