How AI Could Be A Mathematician's Co-Pilot by 2026 (Prof. Swarat Chaudhuri)
01:44:42 Share

神经符号编程是一种人工智能方法，它使用神经网络和经典符号代码的混合来表示模型。你提到了AlphaProof是一个很好的例子，但我认为，即使是那些使用语言模型生成一些代码，然后执行代码，然后获取结果并用它来做决策的代理，它们实际上也在做一些神经符号的工作，对吧？因为你实际上是在使用Python解释器，它也是一种符号工具。

现在有一个宇宙，你再次拥有一个极其低级的语言，比如汇编语言，然后你让机器随着时间的推移自己弄清楚要使用什么样的指令。对我来说，这可能很有价值，因为你可以发现人类永远无法想象的东西，这将使你有潜力进行新的数学、新的物理学、新的学科研究。你将发现这些更高级别的构建块。

是的，你知道，还没有人弄清楚这一点。这个AI做到了。但随后你使用这个构建块来构建简约的程序、能够做惊人事情的模型，然后你只是很好地捆绑它们，你正在构建一个全新的数学和计算宇宙。可以想象这样一个价值。Emily由Senate赞助。

Senate是用于机器学习工作负载的模型服务平台。现在你登录他们的平台，首先看到的是SaaS选项。所以这是一个非常简单的选项。

就像在OpenAI上一样，你可以发送请求，在那里粘贴你的访问令牌，你可以访问所有最新的开源模型。它更快、更节能、更便宜。顺便说一句，当你注册时，你会获得十个免费积分，这意味着你可以在不花一分钱的情况下做一些事情。

我还观看了我前几天与Kenni（CEO）做的采访。

由Tufa AI Labs赞助。这是一个由Benjamin Crouzier在苏黎世创立的研究实验室。他们刚刚收购了MindsAI——ARC挑战赛的当前获胜者。

他们的唯一目的是尽可能快地弄清楚AGI。他们特别关注ARC挑战赛。如果你在苏黎世，Anna，加入他们的每月聚会。

如果你有兴趣作为研究员为他们工作，请联系他，访问tufalabs.ai。欢迎来到MLT。非常感谢你。

感谢你的邀请。

很高兴见到你。你能告诉我们你的背景吗？

我是德克萨斯大学奥斯汀分校的计算机科学教授，今年我也是谷歌DeepMind伦敦的访问研究员。我最初的研究背景是推理和编程语言的符号方法。但在过去的十年里，我也非常参与机器学习。如今，我想说我在两方面都有涉足，即符号方法和机器学习。

很好。我们在来这里的路上就推理进行了非常有趣的谈话。没错。什么是推理？

对我来说，推理在某种程度上取决于观察者。你知道，这是那些你看到它时就知道它是什么的事情之一。嗯，我认为从在AI环境中定义它的角度来看，记住一些标准是有意义的。

那么，什么构成了推理呢？所以，在我看来，在数学或编程或规划这些人们与更深入的思考和推理联系在一起的任务中表现良好，对吧？所以我会说，如果一个系统在这些任务上的表现比现有方法更好，那么我会说它正在做，你知道，它正在显示推理的改进。

所以我犹豫是否要说一个模型要么进行推理，要么不进行推理，因为对我来说，这不是一个布尔值。它实际上是一个定量度量，并且你可以看到，你知道，随着时间的推移，在这个度量上的进展，嗯，现在这更多的是关于它的“什么”，你知道，为了进行推理，模型做了什么。还有一个“如何”的问题，我认为将“如何”的考虑与这个分开非常有用，因为我认为有很多很多不同的推理方法。我们在最近的过去看到其中一些方法越来越突出，但也存在其他类型的。

是的，这，这正是……你认为，你知道，有些人，像人类主义者，他们说这并不是我们推理的方式，而是更好的方式。约翰·塞尔就是一个著名的例子，他认为存在某种复杂的物理因果关系，机器很难复制。但我们可以同意，你当然在模拟中，有无数不同的方法可以使某些东西表现得好像它在推理。

有什么区别，对吧？所以，我认为再一次，这是我们必须决定我们标准的事情之一。所以，如果你有一个系统，它需要大量的计算才能解决一个非常困难的数学问题，那是推理吗？根据你的定义，我认为这可能不算。嗯，但是，我认为，你知道，有人可能会争辩说，重要的是结果，如果你能够解决这个难题，那么你就在很好地进行推理。

我的意思是，它也有一个正确性方面，因为，例如，你可以模拟物理世界中发生的事情，你可以重现轨迹，你可以说，好吧，这是同一件事，为什么它不是推理？但是真正的现象将能够在许多许多不同的情况下进行推理。

当然，对于语言模型来说，当它们在特定类型的推理上进行训练时，它们当然可以在这种环境中进行泛化。但是瑞士奶酪上到处都是洞。所以总是有这个问题。我们有文本污染。

不是吗？是的。所以，我认为，然后你知道，你刚刚命名了一个额外的标准，一个模型进行推理的标准，那就是你需要有这种形式的鲁棒性。我会补充一点，回到前一点，也许计算预算也是一个考虑因素，如果它需要，你知道，五千小时的计算机在一个大型集群上才能解决一个数学问题。

也许它也不是在进行推理，对吧？但对我来说，再一次，你必须决定你的定义是什么，对吧，你的标准是什么，然后你才能谈论一个系统是否在这些度量上取得进展。根据，你知道，类似人类的行为来谈论一个模型是否在进行推理，对我来说，这有点太模糊了。我会说……

是的，这个与人类对齐的挑战，我们当然有的存在性证明是人类在做这件事。但是，如果我们必须创造一个类似人类的模型，从AI的角度来看，这不会特别好。

但我确实相信存在某种推理强度谱，对我来说，感觉那些创建这些自下而上的电路的语言模型，它没有在不同的情况下重用相同的电路，而且我们似乎具有这种令人难以置信的能力，嗯，反映这些非常简约的抽象动机，以及一些认知心理学家认为这些动机有一些根本的东西。也许这就是宇宙运作的方式，当然，这就是我们的认知运作的方式。这似乎不是语言模型的工作方式。

我完全同意。我们长期以来一直在争论这些更模块化、组合式的模型，我认为构建是人类拥有的现代语言模型所缺乏的一种基本能力。但我认为这正在进入“如何”的领域。

你知道，我想要实现某些目标，完成某些任务，对吧？对我来说，将我们试图做什么的定义与我们如何实现它分开是有用的，对吧，使用具有明确分解机制的模型。我们将在前进的过程中讨论我的工作和其他人的工作的一些例子。

但我认为，嗯，你知道，可能会有某种类型的语言模型出现，你知道，也许有不同的训练目标，但是即使它没有明确地处理，嗯，处理模块化，它仍然能够具有鲁棒性，对吧。我不知道这种可能性不存在。然而，我想说，鉴于我们从最近的语言模型中看到的一切，在鲁棒性方面似乎存在一些根本性的挑战，对我来说，你知道，分解和模块化的机制将是一个，嗯，嗯，一个好的选择，嗯，来实现这些目标。

来自OpenAI的一个，它是否在推理？

对我来说，这是一个推理的里程碑。前面还有很大的空间。但是，根据我们刚才讨论的标准，你知道，在编程任务和解决数学问题方面的表现，它似乎比之前的模型要好得多。所以对我来说，这是朝着能够……

推理的模型迈进的一步。很有趣。在哪些情况下，也许我们应该首先说在哪些情况下它在进行推理，这意味着它符合你的标准。我认为可以说，是的，是的，它在推理。然后是它可能不进行推理的情况的空间，可能是由于计算原因，它可能试图解决一个NP难题，而它只是简单地用完了上下文，嗯，或者它可能试图，嗯，在一个它没有接受过训练的环境中进行推理，例如，所以存在局限性。但你认为原则上这些局限性是可以克服的吗？

我认为，嗯，一个增强了很多其他东西的模型可以朝着克服这些限制迈出实质性的一步。好的。现在这里有一些我含糊不清的东西。对我来说，这就是真正的问题所在，那些需要添加到类似于GPT-3的东西中的额外部分，才能实现……

再一次，我不会说它是否在推理，而是在推理任务中表现更好，对吧？对我来说，有一些，嗯，明确的候选者，例如，拥有更多基础机制，使用更强大的符号工具。但这只是推测性的，并且，嗯，在接下来的几年里，我认为我们将看看这些方法是否真的有效。

看到向神经符号的转变很有趣。所以，嗯，在连接主义空间中有很多关注，例如，在NeurIPS上，例如，谈到了软件2.0。有这个想法，Hinton也是如此。

有这个想法，语言模型可以做任何事情，它们可以做到这种涌现的符号和推理，我们可以训练它们到极致。我们现在开始看到，像AlphaGeometry和AlphaProof这样的东西。所以这些是混合系统，它们，它们也普遍存在，我认为我们业务的方式是构建特定的架构来做特定的事情。好吧，我认为拥有这些完全通用的白板式的东西效果非常，非常差。但是你是否也看到了这种趋势？

是的，绝对的。我们许多人一直在争论神经符号方法有一段时间了。但是，我越来越觉得这个术语是不必要的，因为在我看来，神经符号方法实际上越来越普遍。你提到了AlphaProof，这是一个很好的例子。

但我认为，即使是那些使用语言模型生成一些代码，然后执行代码，然后获取反馈，然后用它来做进一步决策的代理，它们实际上也在做一些神经符号的工作，对吧？因为你实际上是在使用Python解释器，它是一种符号工具。话虽如此，对我来说，更有趣的问题是，再一次，不是方法本身，而是这些类型的组合将采取的精确形式。

我们已经看到了一些例子，例如，在AlphaProof中，我们有一个机器学习模型，一个神经模型，它正在从Lean解释器或Lean证明器那里获得反馈，对吧，这为它提供了一种非常可靠的基础。嗯，所以我认为我们也将在更广泛的环境中看到这种趋势的其他形式。我不认为它必须非常特定于领域。在一个世界里，你可以想象代码执行和形式证明基本上可以告知世界上的各种决策，而纯粹的神经模型充当在人类语言和这种推理机制之间传递的层。

推理能否在没有公理的情况下存在？

这是一个很好的问题。嗯，我认为，再一次，这取决于我们对推理的含义。当我们谈论数学推理时，整个目标是，你从某些公理出发，得出某些结论。

所以，我们理解的数学推理，如果没有公理，就真的没有意义，那么物理推理呢？所以，我们认为是物理推理的一切，它都取决于我们处于某个特定的地方，并遵循某些物理定律。所以对我来说，嗯，你知道，你可以想象在一个定律不同的世界中发生推理。但即使那样，你也有公理。只是你的公理不同。

我们可以将推理系统组合在一起吗？

绝对可以。事实上，我们一直都在这样做，我们将数学推理系统与，例如，你知道，人们在自然科学中一直使用的实验经验推理方法结合起来，当我们进行任何类型的科学发现时，对吧？我可以想象，将来我们可以拥有许多不同的推理系统，它们具有不同类型的功能，并且它们都汇聚成一个比其各部分之和更大的东西。

对于零来说。或者你认为那是推理吗？

我认为，它，它绝对是一个强大的系统，在传统上被认为是推理的任务上取得了高度非凡的进展。所以对我来说，你知道，这是一种行为或定义，对吧？如果它看起来像一个推理系统，它在推理任务上做得很好，那么它就是在进行某种推理。

好的，如果它看起来像鸭子，叫起来像鸭子。什么是神经符号编程？

神经符号编程是一种人工智能方法，你使用神经网络和经典符号代码的混合来表示模型。

呃，所以你可以想象，例如，你知道一个程序，其中你有一些神经模型正在对感知做出决策，比如说，某种物体是否出现在场景中，然后你有一些向量从那里出来，然后你有一些符号方法来处理这些向量。很多时候，如果你对模型应该是什么样子有预先的知识，这很有意义。呃，那么你可以想象使用符号代码来基本上编码一些这些参与者。

你也可以想象，呃，神经符号模型在解释假设时被使用。例如，你正在试图理解某个生物过程。现在你可能会得到这个完美的黑盒神经预测器，除了科学家们无法真正理解它并用它来指导实验，但是如果你有一个更机械的模型，它以科学家传统上使用的符号表示形式表示，对我来说，所有这些都只是你知道程序，物理情况和动态系统的定义等等，这些都只是各种形式的程序。所以如果你有一个模型，你知道它像那样以机械的方式表示为一种程序，但是某些神经部分不容易用符号表示，那么这将是另一种潜在的应用。

这似乎是一个相当模糊的术语。但是例如，法国谈论的是离散程序搜索，一个神经网络来指导程序的生成，例如在你的工作中，你可以用它来表示函数，甚至某种事后验证类型过程。确保事情在上帝的玫瑰中，并且还有许多，许多更多的具体实例。所以我想这相当模糊。

呃，它是，当我们定义神经符号编程这个术语时，我们希望非常精确，是的，但是“神经符号”这个词，正如我们前面讨论的那样，它被用在许多不同的形式中，以至于我认为它也失去了意义，是的。

但是当我们谈论神经符号编程时，我们的意思是：我有一个编程语言，我可以用它来表示这些混合模型。我有符号代码和神经网络的组合，然后我们有一些方法被用来发现这些程序。这些方法可能是部分神经的，部分符号的。通常情况下，它们是混合的。

所以，呃，节目的许多粉丝都熟悉凯文·艾利森和他的合作者的DreamCoder论文，据我正确回忆，有一个特定于领域的语言，它有你知道的唤醒阶段，它们有这种神经引导搜索，它们有抽象睡眠等等。所以它与那个相关。

绝对的想法。是的。所以，呃，我想说在过去几年中，在这个领域出现了几类方法。

一个很大的挑战是库学习，你不仅仅是在使用一种固定的编程语言并试图在该语言中找到程序，而是在进行显式抽象。你试图发现新的原语，然后将其添加到编程语言中。DreamCoder就属于这一类。

在DreamCoder中，你从一种极其低级的语言——λ演算开始，然后逐步发现越来越大的模块，这些模块实际上是抽象的，你正在这些非常低级的程序中看到模式，然后你将它们抽象成这些模块，然后你正在使用它们。呃，他们在那里的编程语言纯粹是符号的，但是很容易将其泛化。事实上，最近有一些工作已经完成了。

呃，所以你可以想象这些程序是神经网络和λ演算项的混合，对吧？然后他们用来发现这些库函数以及你知道的程序合成的方法，这些都是神经的。人们可以想象，你知道，将它们现代化，它足够新，但是你知道几年前，你可以想象将它们带到2024年，通过使用大型语言模型来搜索程序和抽象来适应2024年的深度学习。

有趣。所以，呃，DreamCoder没有使用语言模型，并且有一个硬编码的DSL。让我感兴趣的一件事是原语是什么。例如，我们可以搜索图灵机的空间。

我们可以使用λ演算，我认为只是图灵机作为认知心理学的大粉丝，那就是我们有这些认知的原生基本原语。因此，我们应该搜索这些原语。并且据推测，它被训练来执行特定任务。

你可以用它来训练ARC挑战。那么它所做的是说，好吧，在我的DSL中这些固有原语的组合是什么，并产生熟练的程序，你知道这些程序对这个特定的事情有效？所以，就像有一个关于从哪里开始的问题，以及你训练它的任务在多大程度上影响你学习的库。

对吧？所以对我来说，呃，先前的问题是开放的。我认为人类可能确实有一套认知原语，但我们不一定知道它们是什么。然而，真实的是，原语的存在使你解决程序合成问题或库学习问题的能力大大提高。

呃，我的意思是，如果你已经有一套合理的原语作为你的新编程语言，你就不用从头开始发现所有东西。也就是说，我可以想象一个世界，你从一种极其低级的语言开始，没有任何原语。你只是拥有这些基本的运算，比如组合和λ，然后你只是在发现整个宇宙，编程的数学，物理学，等等。这重要吗？

如果我们可以理解生成的程序。这将是本次讨论中的一个主题，因为当然，你的工作也在改进，同时也谈论了数学家如何不再自己做这些事情。我们依靠计算机来搜索这个巨大的空间。但是仅仅通过这种程度的程序搜索，呃，我们可能会创建仍然有很多抽象和许多有趣效率的程序，但是它们看起来非常难以置信。

没错。所以我认为我们应该区分解释问题和能力问题。对我来说，在解释能力方面肯定存在潜在的价值，尤其是在某些应用领域，如科学发现。我们确实关心解释，呃，也存在潜在的安全和保障方面的风险，我们稍后会讨论。但我认为将这种担忧与以下担忧区分开来是有用的。

仅仅是，你会采取什么措施来构建真正强大、稳定和有能力的模型？所以我认为存在一个宇宙，你再次拥有极其低级的语言，一种汇编语言。我认为λ演算就是这样。

然后你让机器随着时间的推移弄清楚哪些抽象是有用的。对我来说，这可能具有很大的价值，因为你可以发现人类从未想象过的事情，对吧？这可能会使你能够进行新的数学、新的物理学、新的学问。

所以我根本不排除这种可能性。呃，我认为这种抽象的想法即使在这种情况下也是有价值的，因为这意味着你将要，你知道，发现这些更高级别的构建块。是的，你知道，还没有人弄清楚这一点，但是这个AI已经弄清楚了。

但是然后你使用这个构建块来构建简洁的程序、模型，呃，可以做令人惊奇的事情。然后你只是在引导和构建全新的数学宇宙，竞争，对吧？呃，我可以想象这样一个世界。

那么你能告诉我们你在这个领域的工作吗？所以，所以你创建了这种架构，它使用元素并进行类型导向的搜索和学习搜索。

那么你能告诉我们吗？所以，我在这个领域有一系列的努力。呃，我过去做了很多关于程序合成中符号方法的工作，呃，设置是这样的：你有一个编程语言，你有一个由领导者定义的编程任务，当时它要么是逻辑约束，要么是一组示例，然后你定义一个搜索问题，找到一个适合任务规范的程序。符号方法有一些可扩展性挑战。

然后当深度学习出现时，你知道，我们都朝着那个方向前进，这种神经引导的程序搜索，这成为了一种非常强大的方法。呃，现在，呃，那里的一些方法结合了这些较旧的符号思想和深度学习思想。例如，我们在类型导向的神经程序合成方面取得了这些成果，你使用强类型语言生成程序，并且语言的类型系统充当修剪机制以及指导机制。

所以它排除了显然不合理的程序。呃，也帮助我们专注于某些类型的子目标。现在如果你想想在证明改进领域发生的事情，它实际上与之非常相关。

呃，Lean实际上是一种具有非常强大的类型系统的函数式编程语言，呃，所以当你例如使用来自证明改进的反馈来排除你数学证明搜索中的某些类型的步骤时，呃，你实际上是在使用这个想法的一个版本，对吧，呃，但是我们一直在考虑这个问题，对于更广泛的程序合成，这个社区来自程序语言，他们一直在考虑这个问题。好的，所以，呃，这仍然是在上下文中。你有一个固定的编程语言，你正在寻找该语言上的程序。现在，呃，还有其他相关的方法。

所以我们有，例如，呃，关于使用神经松弛的这些结果。有一篇我们领导的论文，由我、阿姆·沙阿和我的长期合作者伊斯·宋以及詹妮弗·孙，呃，我的前学生法尔玛，呃，这是关于使用程序的神经松弛作为启发式方法来搜索程序。这个想法是这样的，假设你正在搜索程序，并且你正在逐步填充这些不完整的程序。

所以你从没有任何东西开始，只是一个带有很大一部分呃，很大一部分空洞的代码，然后你逐步添加越来越多的代码。所以这里的一个挑战是，因为你总是使用这些不完整的程序，你怎么知道某个决策是否有价值，对吧？然后你知道，我应该保留某个不完整的程序在池中还是应该将其丢弃？这个想法是，你知道，在这个空洞中，你将要，呃，所以有一个可能的完成该程序的方式的空间。

所以有很多符号离散项可以插入到那个空洞中。但是，你所做的不是那样，而是将一个神经网络放在那里，并且存在这种子集关系。所以，因为这些神经网络比你编程语言中的任何符号程序都更具表达性，呃，你将具有这样的属性，呃，如果你对神经网络进行足够的训练，你将获得比使用任何符号程序所能获得的更好的损失。

这导致了一个论点，即你可以基本上使用在你将这个神经网络插入到那个空洞之后获得的损失，呃，你可以将其用作成本下限。这是从那时起使用符号程序所能做的最好的事情。这反过来可以用来指导启发式搜索，你知道，像A*和分支定界加上你知道的迭代加深搜索等等，所以这些算法来自回溯搜索，对吧？现在你想象一下使用这些神经松弛来加速这些类型的算法。

呃，这种想法一直存在。所以总的来说，我们已经对这个问题进行了很多研究，你知道，我可以使用神经网络作为松弛，作为离散程序的某种连续逼近，以及你可以报告这种松弛的程度。我们已经研究了几个版本的这个，以及其他最近的努力。所以我们有一篇关于符号回归中库学习的最新论文，与迪利普一起。

我们在这里做很多相同的事情，呃，你知道，搜索程序，呃，做抽象，但这次使用alembic，嗯，特别是elm，这是一种非常好的方法，嗯，即使你正在做这种传统的程序搜索，例如使用遗传Albertha，更多的是使用某种类型导向的动画。你仍然可以想象，你知道，一个LLM作为指导这种搜索的神经网络。但除此之外，你还可以想象使用一个l作为一种抽象工具，就像我们刚才讨论过的那样。

例如，你知道，在dream quarter中，抽象发生的方式是，你，呃，你知道，查看一组表现良好的程序，然后你找到在这些程序中反复出现的合成子结构，对吧？然后你会说，好吧，这是一个我可以重用的模块，然后它就成为我库的一部分。问题是，这个过程很困难，因为在一个大型程序池中识别这些常见的子结构非常具有挑战性。

有一些为此目的而产生的符号方法。但是你可以想象一下，不这样做，而是只使用一个alm。那会是什么样子呢？好吧，你应该阅读这篇论文，它是由ara gari和一个服务器单一嗯，并且与miles crime crime先生和omar cus呃，出现在今年的欧洲。

但基本思想是，你将使用一个元素作为抽象器，所以你将奥斯卡，什么是这些程序中出现的一些常见模式，你将使用它的自然语言推理，理解它很多时候，但它的能力至少是，你知道，在语法中找到模式，在语法程序中。呃，你正在，并且用自然语言解释它，你将使用这种能力来进行抽象，对吧？这就是你学习概念的方式。

我非常喜欢鼠标，一个罪犯，几年前他写了一篇关于符号回归的具有里程碑意义的论文。我认为这是另一种新的符号编程形式，而且我还听说人们谈论过符号的语言模型组合。所以这个想法是，你知道，你从这种粘土块开始。你做棺材梯度下降，然后我们我们从它的迷人之处中提取某种符号结构。

所以，呃，先回答你的第一个问题，呃，符号回归我认为是一种形式程序综合。是的，你真正想做的是，你得到一个数据集。你试图找到呃，表达式对，适合数据集。但表达式只是一种特殊的程序。

所以，我们讨论过的一些方法，例如，这种在符号回归设置中完成的神经可接受启发式方法，你试图找到一个适合数据集的程序，对吧？但是现在可以想象，你知道，超越遗传编程方法，或者，呃，这些蒸馏方法，首先训练神经网络，然后蒸馏成一个符号程序，呃，你可以超越这些策略，你可以使用一个LM呃，非常努力地做到这一点，来解决符号回归问题。嗯，对。

那么，它可以用来做什么呢？一个角度是，你可以使用一个elem来基本上搜索程序或指导程序，特别是表达式的搜索。这些让我们谈论进化研究。

所以你可以想象使用一个LM来进行程序的交叉或程序的变异，它们在你的池中。你也可以使用一个alem来进行抽象，也就是说，你可以要求LM提出一些在超形成程序中出现的概念，对吧？然后这些概念成为AA条件，它们基本上在这种情况下调节程序的搜索。

我最近和sba row combat谈过，他有一个LM模块架构，你知道吗？所以他说，lms。

非常有创意。所以现在我们可以遍历这个空间，然后在最后加上一个验证。所以我们实际上可以挑选他们何时真正得到IT正确。

我有点不同意他，因为当然，当我们让联盟找到有创意的东西时，当我们正在做，比如说，LLM引导的搜索，当我们让elms进行抽象时，我觉得它们仍然有点寄生在它们训练的数据上，这意味着存在一种创造力差距。我们似乎可以访问更丰富的创造力来源。然后就是我们建立这个库的事情，在某些时候，库的重量会影响我们的创造力吗？

这是一个很棒的问题。呃，我想补充一点，在符号回归之类的设置中，你有一个优势，那就是你得到了数据提供的基础。归根结底，你想要做的是，你已经看到了一些经验性的，你做了一些经验性的观察，你试图找到符合这些观察的表达式，对吧？

所以，现在当你有一个由elem创造性地构建的新候选者时，你可以想象实际上在你的数据集上评估它，看看它的效果如何，对吧？所以，这可以防止它完全偏离轨道。现在，关于先验知识问题，是的，我绝对是从他们已经看到的东西中吸取教训。

如果你以纯粹的黑盒方式使用alams，那么，呃，你将只受到alam之前所见内容的限制。现在我想补充一点，这仍然是一个，这仍然具有非平凡的价值，因为当你进行新的标志时，你通常是在建立在其他人之前所做的科学之上。而L。

M.大概以各种科学论文、数学问题等等的形式看到了这一点。但就是这样。你知道，你不必局限于零样本黑盒模型。

你可以想象一个循环，你用另一个房间创造性地提出候选者，你经验性地疏散这些候选者，然后你使用经验来基本上进一步微调模型。你甚至可以想象一个宇宙，你从一个完全空白的幻灯片开始的大象。也许它对语言有一些基本的了解，但没有更多的科学。

然后你只是逐步地用各种科学课题来建立它。它正在观察，你知道，各种假设是如何执行的。它正在从现实世界中获得反馈，以实验的形式。也许它甚至可以继续进行新的实验，对因果关系进行推理，并确定一些新的实验来尝试，然后根据这些实验的结果获得反馈，然后用它来呃，我们可以使用这些信息来进一步微调，对吧，所以比仅仅使用LLM，然后呃，作为一个黑盒，然后在最后有一个非常火嗯，更多可能。

我同意这一点。关于创造力总是有这样的讨论。我的意思是，dems一直由demis谈论创造力的后者，发明者是最高的优势。当然，你知道，我们可以。我们可以想象独角兽。

我们可以想象我们在现实世界中没有看到的东西，因为它们仍然是由我们理解的事物复杂整体中的基元组成的，但在程序生成的环境中。所以语言模型，它们有如此多的自由度，并且拥有自然语言、虚构语言和编程语言。所以，然后我们可以做一些事情，比如生成代码，我们可以使用dcs。

即使那样，如果如果我们执行一堆这些程序，它们可能不会停止，或者它们可能无效。所以似乎还有另一个步骤。我们需要实际检查这些程序是否良好才能运行。

没错。顺便说一句，你可以获得比这个程序是否在一些测试中正确运行更多的反馈形式，你也可以对程序进行更严格的分析。但最后，嗯，所以你正在从这些外部工具中获得所有这些额外的反馈形式。

然后问题是你用它做什么，对吧？所以你可以用它来决定是否保留这个程序。呃，但你可以做得更多。也许你可以回到elem，并使用这些信息来基本上进一步训练它并指导程序的编写方式。

如果你想到人类程序员，这就是它的发生方式，对吧？所以你编写代码，然后你尝试各种事情，然后你会看到某些类型的程序有效，而某些类型无效。你从你的编译器、你的类型跟踪器、你的解释器那里得到反馈，对吧？然后你用它来改进你的调用方式。

是的，即使是停机问题，我的意思是，我我脑子里有一些想法，这是我不知道它是一个量子算法，它有上千个数据点。它在90秒后仍在运行，可能这里有什么问题，控制海，回到大约。

是的，你知道，在解决停机问题方面，有大量的研究工作，即使原则上这是一个不可判定的问题。在实践中，关于证明程序终止的文献，它的工作方式是，它认识到证明程序终止实际上是提出一个归纳论证。

所以你所展示的是某种表达式的值在每次执行程序的一个步骤时都会严格下降。所以如果你想到一个循环，对吧？所以你写了一个循环，它说当I小于an时，你知道，某些东西，某些东西，然后I被实现，你知道这个程序将在一个，你知道，尽管艾伦·图灵。

原因是发生的事情非常简单。循环的每个步骤，你都在增加这个I，你只能增加这么多，对吧？所以有一个值，即n减去AI，它在每一步都严格下降。

它只能下降这么多。它不能下降到零以下，因为零或主体是下界，你已经说过，因为你的程序的结构方式。所以你在这里做的这种推理，对吧，这是一个归纳证明的例子，呃，除了应用于程序。并且有很多工作是关于自动发现这些类型的归纳证明，它们实际上是非常简单的符号表达式，对吧？你可以想象使用LM或其他类型的机器学习技术来搜索这些类型的论证。

关于这一点，几点说明。也许你应该引入图灵的著名证明，因为他用反证法证明了，不知道停机问题，但如果我理解正确的话，你指的是你可以用归纳法证明程序将如何工作的特定实例，你还会期望仍然存在程序的空间，这些程序。

你做不到吗？嗯，我没有说任何关于自动发现这些归纳证明的事情，对吧？所以，我的意思是，对于大量的实用程序，事实上，人们编写的绝大多数循环或人们编写的绝大多数递归，这些程序将终止的论证非常简单，你可以使用各种方法搜索这些证明，甚至只是基本的动画也能很好地工作。

但是你可以想象，你知道，使用更现代的机器学习技术来解决这个问题。但是你不可能有一种方法是自动化的，它会呃，它会总是终止它，并且它会适用于所有程序。不。

但问题是，你知道，对于现实的程序，呃，烟雾会产生吗？我们有充分的证据表明，对于人们编写的现实程序，呃，你可以做这些事情中的一种，你可以尝试这些策略来证明终止。如果这不起作用，你就说，好吧，这里有问题。去修复它，对吧？也许有一些原因导致程序仍然有效，但无论如何，你知道，你可以忽略该程序并找到不同的。

解决问题的方法。所以我的合著者，他非常感兴趣图灵机，他说，你知道，语言模型在那里，我们不是在谈论LLM系统，我们只是一个语言模型。他说它们是最终状态自动机，而图灵机仍然是什么，它有一个最终状态自动机作为这些的控制器？他说，你知道，在FSA类中有一组算法。

他实际上会称这些为图灵机算法，即使它们是最终状态自动机，由于停机问题，也不能用棺材梯度索引搜索或发现。我认为你指的是在这个领域已经完成的最早的一些有趣的研究。我的意思是，他会对此着迷，对吧？对吧？

是的。嗯，所以有很多工作是关于使用梯度下降来解决程序强调的问题。对我来说，在图灵机中搜索，它只是一个形式程序综合，它只是编程语言极其低级，它是……每个程序都知道可以访问这个一个计数器啊，这个磁带，然后嗯，然后还有一个控制器，它是一个有限状态机，对吧？所以对我来说，这是一种非常简单的编程语言。

嗯，它在竞争理论的数学证明中很有用，因为它很简单，对吧？但我认为从编程的角度来看，图灵机没有什么特别之处，对吧？任何关于图灵机的推理，你也可以对其他更广泛的程序类别进行同样的论证。

现在，已经有很多关于使用梯度下降来寻找程序的先前工作，而且由于你提到的原因，这些工作并不成功，是的，这就是为什么人们历史上一直想使用神经网络作为一种指导作用，你仍然会进行某种直接搜索。然后你会……你会使用神经网络以各种方式指导搜索过程。我会说神经网络在 DreamCoder 中的使用就是一个例子，但使用 LLM 来编写程序或指导程序搜索也是例子。

这很有趣。所以，嗯，图灵机有这种惊人的能力来扩展它们的内存。所以我们不需要从头开始训练它。我们可以说，我需要更多数据。我需要更多数据来扩展我的内存。

人们说，嗯，你使用一个语言模型，你可以训练它来进行推理，甚至在它的训练过程中，它可能实际上是从数据库中检索信息，或者你可以训练它来执行代码，然后你可以说，我们基本上不是在搜索图灵空间吗？因为我可以，我可以说，生成一个计算π的n位数的程序，这是一个任意n时间的问题，然后我可以运行它，然后我可以把它传回去。但对我来说，感觉这是一种本质上的区别，对吧？但区别是什么？在这样做和真正拥有一个本地处理图灵空间的机器之间有什么区别？好的？

我试图理解，所以你可以想象将图灵机程序的定义作为ADS，对吧？你可以定义一种编程语言，其中每个程序都是一个图灵机，对吧？所以对我来说，这就是你打开一本计算理论教科书时会做的事情，如果你去看图灵机的定义，它只是一种编程语言，对吧？有一个语法，有一个语义。

那么，在训练 LLM 生成这种语言的程序和 LLM 已经做的任何其他类型的程序综合之间有什么区别呢？对吧？我认为在图灵机生成和 Python 代码生成之间没有根本的区别。现在我认为你描述的是一些稍微不同的事情，那就是用于这种生成的流程，你知道，这个流程是一个有限状态流程，还是这个流程更像一个图灵机？我认为这是一个非常有趣的问题，对吧？所以你真正说的是，与其拥有一个语言模型，它只是以这种特殊的方式运行，只是预测下一个标记，并且，也许我可以检索有限数量的信息，也许，与其拥有一个大规模的 LLM，一个大规模的或更大的瓶颈，你可以拥有一个大规模的图灵机，它正在进行各种生成，对吧？我认为这是一个非常令人兴奋的想法。

啊，是的，完全正确。我花了一段时间才弄明白的是，图灵机中的控制器是一个有限自动机，所以存在语言模型中的一组权重，可以允许……你知道……使用某种推送自动机或类似的东西来扩展其内存。所以我们只是无法用随机梯度下降找到它，嗯，另一件事是，是的，我完全同意，原则上我们可以想象我们有一个互联网规模的巨大数据集的图灵机和描述，因为我认为描述很重要，因为拥有一个我们无法以任何方式编程的图灵机语言模型有什么意义呢？需要某种可以理解的映射到我们可以用来指导的东西。

对吧？所以同样，我会区分生成的内容和生成它的方式。所以有两种不同的可能性。一种是使用语言模型，无论是图灵机语言模型还是……一个……一个语言模型法，你知道，一个转换器语言模型，你正在使用某种语言模型来生成图灵机语言中的程序。所以这是第一种情况。

版本二是，你特别指出这个语言模型本身就是一个图灵机，它能够……你知道……访问这个无限的内存，它会去……你知道……从这个无限的磁带上查找东西，这个无限的内存。这是一个非常有趣的命题。我唯一犹豫的是，我们发现架构可能并不那么重要。

嗯，真正重要的是规模。所以所有这些关于……你知道……状态空间模型和高度扩展的 RNN 的新结果。我们看到，许多这些转换器似乎特别擅长的任务也正在由这些极度扩展的 RNN 完成，对吧？

所以我认为……你知道……这种图灵机架构可能需要……你知道……惊人的新能力。但我可能会……看到更多证据。但这绝对是一个非常有趣的想法。

去探索，总有这样的反对意见，嗯，实际上，这并不重要，因为我们可以扩展模型，我过一会儿会很兴奋地谈论状态空间模型和内存，所有这些东西，因为它们可以让我们可能调整模型大小。然后总是有这样的问题，嗯，在某些时候，模型将足够大，可以完成我们想要做的所有合理的计算类型。但反驳是，你知道，我们有时会花很多时间思考问题，你知道，Linux 操作系统，它总是给我们举个例子，我们必须设计和看到非常复杂的工件才能达到我们现在拥有的技术复杂性和成熟度水平。这似乎超出了这些模型的能力。

即使我们扩大它们。没错，没错，是的。所以我认为……嗯，我非常相信拥有超越自回归语言模型范式的算法。这就是为什么我们讨论这些方法，你拥有这些外部工具，比如你知道代码解释器或……或你知道一个 Lean 证明器……或图灵证明器，比如 Lean，并使用它们的反馈来做一些……比我们用其他自回归模型所能做的更多的事情。

但对我来说，这些方法的强大之处不在于语言模型的内部架构，而在于这些不同类型的推理机制如何与神经网络一起工作的高级架构。对吧？我认为……这……这可能是……不同神经网络实现的元素会给你带来截然不同的结果。

我可能有点怀疑，这是我想看到更多证据的事情。但对我来说非常清楚的是，如果你有这些高级架构，你将各种类型的……无论什么想法的神经网络与这些类型的……符号基础机制结合起来……在现实世界中执行，人类反馈……所有这些东西……你将获得比我们今天拥有的更好的东西。对我来说，挑战是如何将这些各种基础机制的反馈传递回神经网络？好的，也许当你这样做的时候，某些类型的神经网络架构会……会更好。但我对此仍然有点犹豫。

我非常同意你的观点，我的意思是，我注意到的一件事是，现在，当然是在构建现实世界的应用程序，克服这种复杂性诅咒的方法是通过架构和流程。这是唯一的方法来……使这些东西多样化。可能唯一的权衡是，你投入到问题中的工程和架构越多，你就越适合这个问题，但你也以某种方式削弱了它在其他问题上的通用性，对吧？

这就是为什么我理想情况下希望看到一些非常简单的东西……一种非常简单且领域通用的架构，但在我看来，有一些这样的例子，所以你知道，让我们以数学为例，对我来说，数学是……一个非常有用的模型，用于解决许多不同类型的问题。

嗯，例如，如果你在做物理学，如果你在做生物学，如果你在做编程，数学都是有用的，即使是对于日常逻辑推理，数学也是有用的。所以我可以想象，一个工具可以给你关于你对世界的模型的数学合理性的严格反馈，对我来说，这是很有意义的。

所以我可能不会认为这是对……对你可以应用你的方法的领域类型的限制。同样，代码执行对我来说，也是一种非常通用的……模型，一种表示世界模型的方式。对我来说，程序总是具有语义。

所以能够执行程序并分析它们，并以某种方式推理四种情况的行为，这也是我认为不会造成巨大限制的事情。所以对我来说，这个想法是你会有这些相当通用的基础机制，然后你会有一个灵活的方式将它们组合在一起。嗯，你不会强加……你知道……你不会硬编码很多东西。

嗯，当你将这些方法部署到特定应用程序中时，你可能会硬编码，但框架应该完全通用，你可以编写……你知道……新的复杂组合，例如，兰证明器和代码执行以及神经预测，也许还有一些自然语言处理和视觉。为什么不呢？对吧？所以你会允许所有这些不同类型的模块的组合形成新的模型，然后你可能会……一个 AI 系统会去尝试找到正确的组合。

你能告诉我们关于 LASER 架构吗？

当然，LASER 方法。这种方法的目标是……嗯……使用 LLM 来驱动程序搜索，并提出解释超高性能程序中正在发生什么的抽象。这是在符号回归的背景下完成的，在这种情况下，你有一个……你有一个数据集，你有一种程序或表达式的语言，你试图找到一个超高性能的表达式。

现在，以前的方法在这里使用了进化搜索，也有一些工作使用……LLM 来基本上指导搜索过程的某些部分。但我们真正探索的是，能否使用 LLM 来提出解释超高性能程序中出现的一些常见主题的高级解释或高级概念。所以你可以想象一个过程，进化搜索会产生一组候选者，你实际上正在使用你拥有的数据来评估这些候选者。

所以这充当了一种基础机制。现在你留下了一堆超高性能的候选者。现在你使用 LLM 来解释在这些超高性能程序中出现的一些共同主题是什么。然后你记住这些主题，这些概念，然后也使用它们来驱动搜索。对吧？

所以像这样的方法，一个很大的吸引力是，即使你没有使用所有……你知道……LLM 拥有的科学先验知识，LLM 将文本片段抽象成高级概念的能力仍然非常有帮助。所以……我们在……寻找重新发现一堆标准方程的问题中部署了这种方法。具体来说，是费曼物理学讲义中所有方程中的方程。这是 Max Tegmark 和其他人在这篇 AI 发现论文中提出的。此外，我们还在一些合成基准上评估了该系统，我们还用它来新发现一个实际的 LLM 缩放定律。

哦，告诉我们。

是的，当然。嗯，所以，嗯，在这里我们想超越 Chinchilla 定律。我们想提出一个新的定律……只使用关于 LLM 的数据。

因此，您知道，例如，关于参数数量、数据集的大小以及在训练中使用了多少次样本的信息，因此您拥有一堆这样的参数，然后您还拥有数据集特征，然后您拥有性能，所以现在您可以提出这样的问题，我能否提出一个能够解释这种异常行为的符号定律？我们发现，我们得到了这个定律，它与仓鼠定律略有不同，这绝对是客观的，我们想要找到一些不同的东西，但仍然具有解释性。是的，更多细节请参阅论文。

但除此之外，我们还在完全合成的任务上评估了该系统。他们还发现，这种概念学习的想法有所不同。因此，即使您忽略了大型语言模型对问题领域的先前理解，这也不是我想要争论的事情，因为归根结底，在现实世界的应用中，您都拥有预先存在的知识。但即使您忽略这一点，您仍然有另一种使用大型语言模型的方法，那就是将其作为一种工具来提出抽象概念。

是的，我也受到梅洛尼·梅特的启发。她在这一领域做了一些工作。迭代抽象似乎有一些非常有趣的东西，也就是说，几乎存在一些固定的外循环，你不断向上，不断向上，不断向上。这似乎告诉我一些关于这方面的信息。

这与我们目前在 LASER 中所做的事情非常吻合，只是 LASER 目前还不太复杂。我们的抽象只是用自然语言描述的，但您可以想象一个世界，在这个世界中，这些抽象可以用更具象征意义的、程序化的形式来表示。随着时间的推移，您的抽象，您故意设计这些抽象，使其达到越来越高的层次。我们还没有做到这一点，但我认为这在 DreamCoder 中是存在的，因为在 DreamCoder 中，一旦您发现了一些库模块，您就可以使用这些库模块编写新程序，然后您可以进一步抽象它们，对吧？因此，这个抽象过程自然地朝着发现越来越高级的模块的方向发展。

您能否也快速评论一下，对我来说，这太令人兴奋了。它目前并没有出现在任何 DreamCoder 示例中，也不是最先进的挑战，但我有一种强烈的预感，我认为这是正确的方向。不幸的是，由于 SOTA 的追逐等等，人们并没有给予这项真正具有创新性的工作足够的关注。

我认为 SOTA 的追逐是一种非常不幸的趋势。我认为，这也是资源的错误配置。有些公司非常适合追逐 SOTA，因为现在您既需要探索也需要利用，而追逐 SOTA 就是利用，对吧？您有一个明确的方法，现在您正在扩展它。

您正在解决以前无法解决的新问题，这很好。但我认为探索方向也很重要。

不幸的是，SOTA 的追逐正在损害这一点。但与此同时，我想说的是，很多人正在提出新的有趣算法。也许需要发生的事情是，从探索本身到利用的转变更加频繁。

换句话说，假设您有 DreamCoder 这样的算法。您如何将其扩展？好的。因此，我们的 LASER 方法是一种通过使用大型语言模型来稍微扩展它的方法。但也许还有其他方法。

还有一个问题是，如何将其连接起来，以便在非常大量的计算资源上运行它，然后，我们能否看看会发生什么？这目前我们还没有做过，但这是我们非常感兴趣的方向。我们正在与各个研究合作伙伴进行沟通，看看是否有任何方法可以扩展它，并且一旦我们做到这一点，我们将非常兴奋地了解会发生什么。

您在数学发现方面做了大量工作，我认为您在您的论文中评论说，您认为到 2026 年我们可能会拥有一个 AI 协同驾驶员。是什么让您这样认为？

那实际上是塔伦·塔沃提出的观点。

哦，对不起。

我非常尊敬他，而且我实际上同意他的观点。我认为我们正处于数学领域一个极其令人兴奋的时期。我可以想象，让 AI 成为一个重要的贡献者，虽然不是，你知道，灵魂的作者，你知道，一篇数学论文，甚至是一篇具有重要数学成分的计算机科学论文，在不远的将来应该是可能的。

好的，那么我们到底是什么意思呢？如果您考虑数学的完成方式，甚至实际上在理论计算机科学中发生的事情，您会发现这些定义非常严格，但最终，并且您有证明，但最终，其目的是说服人类审稿人和读者，对吧？这意味着您可以犯错误。您可以忘记一些极端情况，而您的证明可能会因此而被破坏。

因此，这是当今数学完成方式的一种可能的风险。另一件事是扩展，对吧，即使您不认为当今数学的完成方式有任何根本性的错误，也有机会使用计算工具来扩展数学。直到现在，这都是不可能的。

我的意思是，如果您考虑一个非常大的软件系统，如果您考虑 Linux 内核或 Google 云基础设施，这些都是极其复杂的系统，任何个人都无法完全理解。人们在抽象的高层次上理解这些系统，也许他们不了解特定组件的所有底层细节。但我认为实际上很少有人对整个系统的详细情况有全面的了解。

现在，如果您考虑数学证明，历史上，数学一直非常注重个体贡献者。因此，当您想到一位数学家时，他是一个，你知道，他们会产生一个证明，并且他们知道证明的所有细节，对吧？他们自己制作的，或者至少他们理解了这些细节。但想象一下一个世界，在这个世界中，存在极其复杂的数学问题，也许没有个人能够理解所有细节，但您仍然可以保证整个证明可以分解成对人类来说更容易管理的片段，对吧？就像我们编写代码一样。

我们能否为数学做到这一点？那会是什么样子？我认为 Lean 等系统提供了巨大的机会。

现在，AI 自然而然地参与进来，就像 AI 协同驾驶员使编写代码变得容易得多一样。您可以想象有一个协同驾驶员来编写数学证明。如果所有这些都是可能的。

因此，我们可能会拥有新型的数学，人类之间新的协作模式。这是特里托里广泛讨论过的事情。然后，AI 驱动这个过程，使我们的效率提高十倍。我会说这会导致带有 AI 贡献者的论文吗？我会说，是的，不，你知道，也许不会。这并不一定，因为就像我们不会列出我们的计算器或计算机作为作者一样，我们可能会接受，好吧，这里有一个工具，它做了一堆事情，但仍然存在高级别的人类创造力，而这些将成为视频的作者。但我认为 AI 肯定会做很多事情，而今天数学系的学生必须去做。

很有趣。因此，我们看到，我想，很多人认为数学理论是相当分散的单元，由一位或几位数学家研究和理解。我们，我想直到最近，才考虑大规模扩展会是什么样子。是的，我们需要说服审稿人，而您说，即使审稿人越来越难以理解，因为规模太大，如果证明是由计算机发现的，审稿人会更倾向于相信它。因此，我甚至会质疑为什么需要审稿人来理解证明的每一个细节，对吧？也许审稿人只需要理解证明的高级组件。

然后，只需确保证明的较低部分是正确的，就像您阅读代码时一样，您不必考虑，好吧，这是这段代码进行的系统调用，这个系统调用在汇编级别是否正确实现。您不会考虑这一点，您假设 Linux 内核的实现者已经正确地解决了这个问题，对吧？因此，同样，人们可以想象在证明中，证明处于抽象的高层次。

然后有一些较低级别的构建块，您认为是理所当然的。现在，人们也可以想象，就像您在软件中构建大型系统时一样，您将系统分解成多个部分，您将这些责任分配给不同的人。并且有一个接口。

在这些方面应该得到验证，只要它们确实如此，并且在单元级别和端到端级别都有通过的测试，您就会接受这个系统是可以的，对吧？同样，对于数学证明，我们也应该具有相同类型的组合，您将拥有一个大型复杂的证明。假设我们正在谈论费马大定理，这需要一个人类很长时间才能证明，对吧？

但也许现在您将提出组合，您将拥有一支由一千名数学家组成的团队来研究这些部分。然后，有一种方法可以确保，假设这些部分是正确的，每个人都履行其本地义务。证明费马大定理的全局目标将是正确的。

因此，我对将更大的整体分解成这些局部义务的想法很着迷。让我们看看 Linux 操作系统。您认为在本地级别拥有这些对人类来说可理解的接口模块是否会引入某种瓶颈？我的意思是，我可以想象未来语言模型如此强大，它们可以随时重新生成整个代码。

但这将成为签入代码的噩梦，因为它，你知道，约翰·琼斯刚刚破坏了他的组件，而那里的模式接口已经改变了。因此，您认为这是否总是会存在一种有趣的权衡，为了拥有一个一致的接口，我们几乎需要增加局部模块的复杂性，对吧？

我认为这回到了可解释性和能力的讨论。我认为原则上，可以创建一个完全用汇编代码编写的 Linux 内核。它不是模块化的。它没有这些对人类来说可理解的接口，对吧？但它仍然是功能安全的。

我的意思是，您有一些高级目标，一些人类已经写下了这些目标，关于 Linux 内核需要满足的属性，然后，你知道，您的 AI 会生成一大块汇编语言代码。然后还有一个正式的证明，证明该代码实际上正在做正确的事情，对吧？那么，我们为什么会有任何异议呢？

对我来说，问题是，首先，这种说法目前还只是幻想。我们实际上没有任何 AI 能够在没有任何人类干预的情况下生成大量高度可靠的代码，除了在最顶层进行一些规范，以及随着时间的推移，需求将会发生变化，并且您可能希望有一条途径，让人类能够参与到这个 Linux 的维护中。

您的内核，我认为同样的论点也适用于数学证明，存在一个世界，所有数学都是通过按下按钮来完成的，然后数学就完成了。因此，数学家提出了这个理论，他们陈述了这个理论，然后他们按下按钮，然后您的 AI 就会在尽可能低的级别上生成证明，而无需任何人类解释。但是有一个证明检查器，即 Lean 证明检查器，它已经为您检查了证明，对吧？所以我认为这在原则上是可能的。

实际上，我们离那还差得很远。所以至少在短期内，我们希望得到的证明至少在解释上缺乏模块边界，这样人类就可以参与到高级过程的设计中，而机器则负责低级的细节。但我可以想象一个世界，在这个世界里，人类越来越少，越来越少。尽管你会对数学的意义提出一些疑问。你知道，数学的部分原因在于它很有趣，它教会我们一些关于世界的知识。但是，你知道，如果数学的意义仅仅是一种工具性的思考，认为你在做数学是为了预测某种化学反应是否会发生，那么也许这是你可以允许人工智能去做的事情，就像今天一样，使用数学或或或mah实验室来进行大量的模拟。

那么，在这个领域有哪些进展呢？我知道你在这个领域做了很多工作，人们都在关注什么。

对吧？所以有几个不同的方向。目前研究得最透彻的方向仍在改进。所以这里有几个版本。

一个版本是，你从一个理论的形式化陈述开始，比如lean语言，然后你搜索这个理论的证明，m所以像lean这样的足够框架，一个证明只不过是……它就像代码一样，是一系列指令，在这种情况下，被称为策略，所以你正在寻找一系列策略，这些策略将导致目标被证明，这实际上就像找到一个程序来实现某个规范。这方面有很多工作。最有效的方法。

它们结合了神经网络的使用和在um lan peronne中的执行，你正在得到一些反馈，关于你是否知道你应用的决定是否做事情，然后你会使用这个反馈来做更多的生成。所以这就是那里发生的事情。也有一部分工作是关于非正式的泪流改进，你是否有自然语言问题陈述，并且你经常使用纯粹的非正式方法，比如，你知道，这种基因思想的变体来进行数学推理。

但有时你也会结合这两种方法。Shan Wallop和他的合作者有一篇不错的论文，是关于使用自然语言模型来提出高级证明草图，然后使用这个证明草图来驱动农民证明者。那篇论文的名字是什么？草图证明，是的，所以这是一个方向。

如果你正在改进正式的泪流改进和非正式的泪流改进，还有许多其他有趣的问题尚未得到探索。一个非常吸引人的方向是开放式的探索。如果你想想数学真正需要什么，我能贡献什么？一个重要的机会在于提出更好的猜想，创造性地提出更好的目标，你想证明的不仅仅是证明本身，而是……也是主题的陈述。

我认为这是一个极其重要的方向。但不幸的是，到目前为止，这方面的工作还不多。但也有一些研究小组对这个问题非常感兴趣。

而且，例如，有一些努力，你知道，你有一个……一个好的人最近发表了一篇非常好的论文，是关于使用内在动机来驱动AA证明者。那里的想法是，你有这两个代理。你有一个代理正在提出新的主张，你还有一个不同的代理正在试图证明它们。所以实际上，你知道，你在猜想过程和证明过程之间有这种相互作用，这正是数学中发生的事情，如果你考虑它的话。

昨晚我读了你的corpora论文，非常有趣，我的意思是，你已经用高级术语谈到了lean，但也许你可以更详细地谈谈，但……它基本上是一种算法，……你知道，你有一个恐惧……然后你有一系列义务，然后算法将使用语言模型来解决这些限制，然后它将递归地冷却自身，直到它用完义务。我想启发式部分是使用语言模型从这个柠檬数据库中找到一个合适的柠檬，这是一个迷人的架构。你能告诉我们关于这个吗？

当然。所以……一件事是……与所有其他lean泪流改进或正式泪流改进的努力一样，那就是……有一个正式证明的整体结构。

那里的想法是，你有一个你从顶级时期开始的目标，然后你逐步应用这些策略，这些策略将这个目标简化为主题，对吧？过了一会儿，假设你选择了一系列好的策略，你没有更多目标需要证明，然后你就完成了。你的团队已经被证明了。

QV，D，对吧？所以这就是lean。这与AI无关。现在的问题是如何以一种聪明的方式使用AI来选择策略？而珊瑚论文做出了几点贡献。其中一点是，你只是使用大型语言模型，没有任何微调。你只是提示它猜测策略，这与烟火不同，在烟火中，人们使用在证明数据、正式证明数据上明确微调的模型。

现在，对我们来说有点令人惊讶的是，即使是一个黑盒模型也能预测这种形式化证明的合理策略，即使语言相当新颖，但一个重要的点是，仅仅查询语言模型是不够的。你还必须做这个LM模块的事情，你得到LM预测的策略，然后你用它来实际改变你的执行策略在底层的lean框架中。然后你得到一个新的状态，一组新的义务需要证明。

然后你继续前进，对吧？而l实际上可以看到当前的义务是什么，而且实际上有一些……它有一些来自h的记忆……来自过去。所有这些都被插入到一个更大的搜索中，对吧？搜索过程正在回溯，正在记录什么失败了，什么不起作用或什么起作用和什么失败了。

所有这些信息都被用来指导elem的生成过程。所以这是一个想法。另一个想法是你在进行检索。现在，直觉是……当你做数学时，你通常会使用其他项目中的定义……你使用其他项目中的拉马斯，而使用这些外部知识库的想法，最初是在ku Young的reproval LED模型中引入的，他现在在meta，正在为数学研究做AI，而这个reproval模型是经过微调的。

但在这里，我们想探索的是，我们能否只以一种简短的方式使用大型语言瓶子来做同样的事情。我们发现，是的，它能够从外部数据库中检索知识。所以这真正表明的是，上下文学习可以走很远，即使是在做正式……的这种非常奇特的环境中。

直到改进。是的，你尝试在GPT三、五turbo和GPT四上这样做。你会注意到GPT四有显著的改进。

你消融了检索，检索帮助很大。我认为你将其限制在大约60步。但如果时间更长，它可能会更好。而且……回溯可能有一些概念，我现在处于糟糕的状态，我要回去，这是如何工作的？

所以，像lean这样的正式框架的好处是，你正在获得关于什么是……什么状态是糟糕的信息，对吧？所以如果你……如果你处于证明的某个……状态，你有一组需要证明的义务。现在你采取一个没有帮助的策略……或者实际上是当前状态下根本不适用的策略，那么你将获得反馈。

或者例如，如果你发现你正在循环回到你已经……你已经看到的状态。所以你基本上会在状态空间中陷入无限循环。那么这也是你应该避免的事情，对吧？而这种信息可以通过将elm明确地嵌入到更广泛的搜索过程中来获得。

我认为，再次，……主要发现是，上下文学习在……环境中可能很有趣。现在我们将其限制在60个，因为我们使用的是学术计算预算，而且当时GPT四相当昂贵。但我认为，随着模型变得越来越便宜，看看这种LLM加……搜索，加上通过lean或其他类型的框架进行外部基础，这种方法能走多远，这将非常有趣。我认为你实际上可以走很远，特别是如果你愿意进行导出，也就是说你收集数据，然后用它来为模型寻找，然后你继续这样做几件事。

所以我对这个可达性概念很感兴趣。所以你有一堆策略在……数据库中。然后有一些概念，我们一直在指出的关于策略的复杂整体给你一些可达空间。所以……所以……也许我们应该谈谈这个复杂的整体，但大概会有这样的例子，主题有一个目标状态，而这个目标状态是无法用这些策略达到的。我的意思是。

你能解释一下吗？对吧？所以有一些低级策略可以让你真正找到任何东西。只是可能存在一系列策略可以让你到达那个……目标状态，但它可能太长太复杂，你的AI可能找不到它，而这种情况一直都在发生。有很多陈述是我们无法证明的。

现在我认为一个有趣的问题是，如果你能够将这些低级策略抽象成高级策略，你是否期望AI做得更好？我认为答案是肯定的，对吧？如果你想想数学学生的进步过程，你从非常基本的代数开始……或者甚至在那之前，你从算术开始。

然后你……你进入代数，然后突然你有了这个巨大的飞跃，然后你进入微积分，你知道你……你学习概率，然后你可以变得更抽象。你进入复数。所以有一个人类学生学习数学时经历的指令等级结构。

而这些吸引力的目的是，你能够更强大。你能够处理越来越多的问题。所以你将许多点解统一成一般解。我可以想象，即使在AI用于数学的这种情况下，这种方法也是有价值的，你将从一些低级的策略开始。但也许在这种梦想引述的方式中，你将发现更抽象的策略，然后你将使用它们……来做更多成功的证明，然后事情会在某个时候爆炸，你会发现新的数学。

分辨率是如何影响泄漏的？M，我当然是在想物理学的例子，新的托尼力学和相对论。那么你是否通过依赖高级抽象来引入泄漏呢？

在这个正式证明的环境中不是这样。原因在于框架likely nor rather their rather once as well um这些框架的架构方式。你必须始终保持确定性，否则你的证明将不会被接受。

所以，即使你处于高级抽象状态，你也会有高级原语的实现，这些实现是基于实际有效的低级原语。话虽如此，你当然可以想象这种方法的版本，在这种版本中情况并非如此。例如，你可以想象AI用于数学的一部分，其中有一些低级或一些证明义务只是……经验性的，对吧？

想象一下，我正在做一个陈述，……我不知道，也许这不是宇宙……数学定律，但也许它是某个地方和时间的属性，对吧？所以也许你……你有一个预测，你只是在评估经验性的东西。现在你可以赋予它数学意义，通过将其变成概率预测。但你不知道你选择的分布是否正确，对吧？所以在这种情况下，会发生什么情况是，你的分辨率越高，或者分辨率的进程越长，不确定性就越大。但如果你使用……你知道，上述级别的形式化数学，你仍然会对所做的主张有一定的把握。

所以，这与你在自然科学中使用数学的情况并没有太大不同，你会进行一些经验观察，其中存在噪声，对吧？但你最终会将它们纳入一个更清晰的数学模型中，你所做的所有推论都基于该模型，它们以你的假设为条件，你的模型是正确的，对吧？我认为这与使用粗略的屏幕模型的情况并没有太大不同，你会对你的结论有更多的不确定性，对吧？它不是非黑即白的，它不必完全确定或完全不确定。

我最近与 David Blei 谈过话，他在应用类别理论方面非常有名，他有点说我们整个推理框架几乎源于我们提出的问题，我想知道当我们谈论定理及其效用以及人类在创造这些定理中的作用时，是否也是类似的情况。嗯，一定有一些原因让我们提出这些问题，比如这些问题从何而来？

我认为对于许多数学来说，它都受到解决现实世界问题的目标的启发。如果你想想人们为什么提出几何学，人们为什么提出微积分，我认为有一个非常实际的目标，那就是你想了解世界是如何运作的，然后你想应用它来做新的事情，以解决现实世界的工程挑战。所以我认为这是起点。但当然，你知道，也有优雅的动机，以及好奇心，你想拥有优雅的、统一的解决方案，而不是仅仅被检查过的点解决方案。嗯，你也会好奇，好吧，我在这个定义中做出了这些假设。如果我以这种方式改变这些定义，会发生什么？我觉得如果你把这些想法结合起来，嗯，对我们日常生活中可见的现象进行建模的想法，并将其与好奇心的动机结合起来，你会问，好吧，如果我修改了这个，会发生什么，以及将点解决方案统一成更抽象的东西，我认为你会得到很多数学方法。

你能稍微解释一下吗？那么，如果你能打破这个呢？是什么构成了一个真正好的数学理论？

我不是专业的数学家，所以我可能不是问这个问题的最佳人选。也许我可以谈谈计算机科学，我可以尝试回答这个问题，比如说，对于重要的计算机科学论文，因为我来自那个社区。所以在那里，我会说，嗯，一个问题是，呃，是否……有一个有趣性的问题。是的，是的。那么什么是有趣的呢？嗯，我认为它应该是你试图解决的清晰的问题。

呃，它应该是简洁的陈述，它不应该是这样的，我提出了这个奇怪的定义，有不同的呃情况，然后嗯，我想证明关于它的某个定理，对吧？所以，它应该是相对简洁优雅的东西，然后嗯，它应该是新颖的，所以如果感觉我以前见过这个版本的定理，我可以取其中一个先前模型的证明，稍微调整一下，然后证明就出来了，那就不值得追求了。所以我认为新颖性、简洁性和优雅性是重要的标准。然后我会说，尤其是在计算机科学中，效用也是一个考虑因素。

计算机科学家经常关心某些类型的理论的原因是，它们对现实世界的计算过程建模。所以人们对在线算法感兴趣，因为你知道，有很多实际的计算机系统需要在线处理数据。人们对算法博弈论感兴趣，因为互联网出现了。

然后突然间，我们开始偏离对竞争世界的传统集中式观点。相反，互联网是一个巨大的计算机。你拥有所有这些由自身目标驱动的代理，但它们正在使用这个进行协调。

这是一个成人或呃，任何其他类型的在线协调。梅根的短信，对吧。这导致了所有关于算法博弈论的有趣工作，在那里，它是我们，那个。好吧，所以让……所以我有这些不同的代理，它们到达任何俱乐部，嗯，对吧，这是一个市场，对吧，嗯，它们可能是市场的买家。

但是嗯，我想现在问的是，与传统的博弈论相比，我能在多项式时间内达到均衡吗？对吧？这个均衡不仅是可以达到的，而且在计算上也是易于达到的，所以正如我所说，许多有趣的计算机科学理论是通过采用这些独立的原则和数学以及先前的计算机科学，然后将它们应用于这些新的环境、新的模型，这些环境和模型都受到地面上实际问题的启发，在……在……嗯……计算机系统中。

博弈论是一个很好的例子，绝对是。我的意思是，我对代理感兴趣，这是一个很好的例子。它只是自然界中的一种现象，它很好地描绘了某些行为动态等等。

然后我们创造了这个博弈论的东西，它也使用了代理的概念。它具有这种不可思议的有效性。所以对许多嗯，你知道，复杂的系统进行建模，即使我们选择以不同的规模对代理进行建模，甚至在模型内部混合不同的规模。

但是回到你对真正好的理论的定义。虽然你说简洁，我认为你指的是帕累托最优，但你知道，斯基说 LLM 没有语言理论，因为它们没有那种清晰的界限。它们没有……它没有界定他认为是语言的东西与其他任何东西，比如不可能的语言或其他什么东西之间的区别。所以这是关于这个界限的某些东西吗？

我认为 LLM 嗯，会产生训练集中存在的东西，对吧？以及一定程度的组合，因此。所以我认为，如果一个 LLM 主要是在优美的定理和优美的文献上进行训练的，我认为你会在生成器生成的文本中看到某些方面的体现。

然而，我认为这种简洁性、这种优雅性也是微妙的。它不仅仅是遵循某些高级动机，比如美，而且还关乎嗯，一致性。所以很多时候，例如，当我使用 LLM 写作时，我发现，好吧，这段写得很好，很好，但是下一段有点不同。

它可能是你知道的，单独来看很好，但是当我把两者放在一起时，它就变成了有点混乱的东西，对吧？我认为这种优雅的想法是一种全局的概念，它不仅仅是你知道理论的小片段被清晰地陈述，因此整体也被清晰地陈述了。嗯，所以我认为对我来说，这是一个非常开放的问题，LLM 能否提出优雅的陈述。我不知道答案是否定的或肯定的。

并且为了结束这个话题，因为你在你的消融研究中概述了，一直到零样本，在一个空白的 GPT 中，它不是 GPT-4，我认为如果我没记错的话，我得到了大约 2.3% 的结果，然后它通过所有这些协作算法和检索以及回溯，大约达到了 30%。嗯，问题是，我们心中总有一种挥之不去的感觉，那就是测试集污染。做了一点工作，你能谈谈吗？是的。

所以这是一个非常困难的，基于 LLM 的方法的问题。总有一种担忧，那就是你看到的结果是由于污染造成的。

现在我们尽我们所能来解决这个问题，呃，这表明……所以首先，我们证明了，如果你去除所有添加的额外部分，我们只是要求 LLM 去生成证明，嗯，并且它最终没有成功，它得到了大约 2% 的结果，正如你提到的那样，我们还查看了许多生成的证明，我们非常努力地寻找互联网上的类似例子，嗯，我们根本没有找到任何类似的例子。所以这是另一个迹象表明，我们看到的证明并不是污染的产物。话虽如此，污染可能间接地起作用了，也许 LLM 以前见过类似的问题，而我们只是找不到。呃，这绝对有可能。但我感觉，在这个历史阶段的人工智能研究中，我们只需要知道，要非常清楚地意识到这种风险，但仍然继续嗯，使用 LLM，是的，汗水。

当我与 Subhro 谈话时，他说当他解决积木世界中的规划问题时，他制作了一个神秘的积木世界版本，他只是打乱了所有的标记，显然这确实导致了性能的显著下降。但它非常微妙，不是吗？它非常非常困难。

是的，是的，在标准基准测试中，我认为这是一个很大的风险。现在我认为人们可以想象使用合成基准测试。呃，我们在 COPRA 论文中采用的方法，我认为它并不适合完全任意的合成基准测试，因为重点是 LLM 内部的先验知识有助于找到新的策略。

但是我们最近参与的另一篇论文，呃，它涉及使用 LLM 在符号回归的背景下进行概念学习，在那里我们也在搜索框架中使用了 LLM，这是一个进化搜索过程，在这种情况下，呃，我之前在我们的谈话中提到过这篇论文，你实际上正在使用 LLM 进行概念抽象，并且你正在使用这些抽象概念来指导搜索过程。现在在这种情况下，我们确实对合成呃问题进行了实验，我们发现 LLM 在那里也有帮助。原因是，即使你没有使用任何先验知识，LLM 的抽象能力，即根据一些文本例子提出你知道的高级概念，这是有帮助的，但这并不是 COPRA 方法的一部分。因此，没有理由相信，如果你只是提出一个完全合成的问题，COPRA 能够做到这一点。好吧。

太棒了。在我们结束之前，人们在哪里可以了解更多关于你的信息？

只需搜索我的名字，然后你就会进入我的网站，我的所有论文都链接在那里，嗯，我还有一个推特账号，呃，只是 Swarat，但是如果你真的想讨论一些技术性的东西，请给我发消息，我很乐意。

检查更多精彩内容，我们将把论文放在屏幕上，这是一次精彩的对话，非常感谢你的加入。很高兴能有我。

我也喜欢你。