Shownotes Transcript
大家好,这里是海外独角兽开源 AI 研究平台海外独角兽的同名声音栏目我们主张用开源的研究和讨论精神链接全球 AI 从业者行业瞬息万变我们在这里拉起认知,抹平鸿沟欢迎来到新一期海外独角兽我是主持人 Penny
最近 AI 领域有一篇讨论度很高的文章是强化学习之父 Richard Sutton 和 DMAT 科学家 David Silver 共同发表的《欢迎来到经验时代》这篇文章指出如果要实现 AGI 构建能完成复杂任务的通用 agent 必须借助经验这一媒介
这里的经验就是指强化学习过程中模型和 agent 积累的人类数据集中不存在的高质量数据强化学习是 AGI 的关键解法从 OpenIO1 到 DeepSync R1 我们不断在看到强化学习的潜力这篇文章中 DeepMind AlphaProof 被认为是经验时代出路端倪的一个例子
作为第一个在 IMO 获奖的 AIAlphaProof 借助强化学习算法自行做题并积累经验最终在定理证明环境中自我探索自主生成了上亿条新的形式化证明数据 AlphaProof 的案例表明在像数学这样人类高水平知识接近极限的领域强化学习通过互动试错可以突破瓶颈取得超人类的成果
以 AlphaProof 为开端整个数学证明领域也在最近半年迎来了 AI 突破的密集期除了 AlphaProofOpenAI 的 O1 模型在数学推理上也展现出了惊人的表现 DeepSync 推出的 DeepSync Prover v1.5 也在形式化数学证明上创造了新记录为什么 AI 研究中要特别关注数学证明能力一方面 AGI 的目标之一就是 AI 自主研发新知识
因此 AI 在数学领域的突破是模型能力提升最直接的表现另一方面因为数学证明和代码类任务有着严格的规则和格式要求并且要求推理过程中每一步符合逻辑规则因此这类任务的逻辑性可验证性也为模型推理能力的提升提供了很好的强化学习环境
这期内容我们请到了 DeepSickProver 系列核心作者辛华健邀请华健和我们讲解数学和 ACI 之间的关系华健本科毕业于中山大学逻辑学现在是爱丁堡大学人工智能方向的博士他目前专注于大模型在数学定理证明中的创新应用最后一个友情提示
这期内容同时涉及 AI 和数学领域的硬核干货大家可以配合收诺的部分注视来收听本期内容也欢迎在评论区留下你的疑问和建议首先特别感谢华健来到我们海外读教授要么先请华健可以先向大家介绍一下自己吧
好的好的谢谢 Pedro 大家好我是新华健现在是爱立马大学的一年级博士生之前是在 DeepSync 做 DeepSync Prover 系列模型然后现在是在 Z 跳动的 Seed 团队继续做定义证明方面的研究然后我是从最早 2022 年开始做这方面的工作然后最开始是在是在华为诺亚做然后后来 DeepSync 想要在这方面进行一些进一步的探索然后我就进一步参与到了这个工作当中来
然后 DVC Prover 其实在这个领域算一个比较典型的工作从名字上可以判断出来就从 DVC Prover 之前的话几乎每一个工作都它独特的名字但从这之后几乎所有的模型都会叫什么 Prover 比如说 Gode ProverKibana Prover 基本上我们就把这样一个领域作为一种研究范式给固定下来的我觉得这个还是比较
对我个人来说是比较开心的事情然后接下来的话我也会在这方面进行进一步的探讨然后包括从单一定理的证明推广到定理库的实现包括我们想要对一个完整的数学的库来进行一个形式化也都是我们的未来的研究范围
华健是在 DeepSick 也实习过然后现在在这个字节实习并且也在爱宁宝念 PhD 嘛在这种不同的世界一流的这个组织里面去做 research 有没有什么不一样的感受
这个和大家想象其实是比较类似的比如说 DeepSick 作为一个非常非常年轻的团队他从 23 年开始组建到我工作的时间就 24 年初上半年的这样一个时间的话他仍然是一个非常年轻的团队这个年轻一方面体现在他的历史不是那么长无论是在 infra 上还是在组织上还是在工作方式上都是一个不断演进的过程
然后同时也包括年龄上就是 DeepSick 喜欢招应届生无论是硕士应届生还是博士应届生大家在整体年龄画像上都是比较低的大家会把很多更多的学校里面的工作方式和生活的
积分带到公司里来这会和一般的创业公司甚至一般的大公司有一个表大的差别但是自己的话是一个相对来说在体系架构上更加成熟的企业我觉得这方面还是各有所长的就是当是一个
完全新的领域的话对于初状公司来说的话可能是更快的有针对性的调整人力和技术上的投入但是当一些问题的复杂度无论是在工程上还是在人员组织上都是已经到了一个比较大的规模的话自己的话这样会有一个比较对于任何这样的困难问题有一个比较成熟明确的打法我觉得也是一个需要认真看待的一个选手
我个人是这么觉得的而对于学校来说的话现在大家的观点就是在比如说大剥陷研究的话学校和业界已经慢慢有一点点脱节许多大的实验很难在学校的计算机群上进行这种算力上的硬性限制很大程度上影响或决定了研究上的风格往往局限于在具体的细节上雕花可能会陷入见目不见灵的误区
这一问题在强调规模效应的大模型研究中更加严重,因为往往具体的技术可能只在小模型上效果明显,但这种效果上的收益会随着模型规模的增大而被逐渐淡化。如果学界的团队只能在小规模的实验上进行验证,那就无法确认同样的方法推广到更大规模时是否还能奏效,也就无法对于智能边界的扩张提供有效的指导。
这就是为什么一流的研究范式总是在头部的企业中提出不仅仅是好的想法无法通过最好的实验证明的而且是无法进行最好的实验决定了难以提出好的想法所以说我觉得 IDMO 主要是给我提供了一种在知识上互相交流的机会但是在实践上我仍然主要是在企业里面做
确实这是过去几年 IM 出现之后的一个特别的一个现象吧比较优秀的人才可能都在企业里面才能拿到更多的 GPU 资源和这个做实验的资源那听起来 DeepSick 和字节都是挺适合这个 AI 人才去的这个组织是的每个人对 AGI 的这个定义可能不太一样
如果说从你的对 AGI 的理解的角度来看现在你做的研究主线在实现整个 AGI 的道路上你觉得可能会起到什么作用 AGI 的话它其实包含很多层面上的意义语言模型多模态和机器人等不同领域对这个问题也会给出不同回答一方面比如说对知识层面的话
他会希望能够理解所有的人类的知识然后以一种正确的方法像人类一样能够成功的运用
而另外一方面它还涉及到它能够像人一样主动的生产和积累知识而这方面的话是我们之前的尝试的话都不太能覆盖到的我们只是通过一些具体的问题和回答的这种二元结构的任务来进行评测比如说让它能够进行一次代码编写进行一个知识问答
我们认为这样的形式能够和人类进行一个能力的 mesh 的话就认为它是 AGA 了但是我们到现在 2025 年的话我们的理解对它的需求是相当于更高的我们实际上是向更 agent 的方式来对它提出了一些需求也就是说我们不仅认为它是一个知识的使用者而能够像人一样是一个知识的发现者知识的整理者而不仅是知识的使用者
这会带来很多额外的挑战这方面其实也就反映在我们在做数学当中的一些具体的问题比如说在数学上我们也需要无论是在解决单一问题当中想要以更好的方式对一个复杂问题来进行一个拆解还是说想要提出一些引理和假设来指导我们往哪个方向来进行思考
还是说我们想要对整个人类数学已有的知识来进行一个整理和编排找到能够更加好的概括很多互相孤立的数学结论之间的一个统一的结构
来对已有的数学知识有更好的整合还是说我们希望解决一些开放的问题这些开放的问题可能会引导我们不断主动的想要对已有的数学的知识结构来进行一个调整和扩充才能够满足这样一些问题还是说我们甚至这些开放的问题都是能够让模型来自己的提出来的就像人类提出大定理之后我们发现这个不仅仅是一个出能出路的问题还需要很多很多高等的知识才能够解决
这个如何提出更好的问题的话实际上对于一般的科学研究来说是一个比较重要的方面而实际上我们也希望我们的模型我们的 agent 能够像人类一样满足人类活动的这样对知识生产的一个完整的流程而不是仅仅一个验证的流程这方面的 AGA 我们认为才是一个真正符合我们需求的 AGA
而有这样能力 AGI 的话才能够真正的在各个流程环节上能够至少能够人机写作解决一些复杂的问题而不只是我们把问题已经整理好了之后再喂给他能够解决一些我们已经非常好的约定和限制好的干净的问题才能够解决那这肯定不是一个
general 的符合人类水平的一个智能体的体系总而言之的话所有这些的对 AGI 的刻画和理想实际上和现在的大家对 ATI 的追求已经非常的相近了
所以说我个人会经常认为我们对 AGI 的如果说不讨论其他模态和对世界进行交互的话我们的 AGI 就是 agent 的 AGI 那在我们就是比较深入的去讨论 Prover 之前可能前面还需要跟大家做一点这个科普
因为你的这个研究领域是 LM 加形式化数学嘛可能很多听众对形式化数学还不是特别熟悉能不能先跟大家解释一下形式化数学以及形式化是什么跟我们大家平时熟悉的比如说用纸笔去演算或者用自然语言去表示的这个数学有没有什么不一样
好的我觉得这个也是一个非常关键的问题比如说大家实际上在日常做 LM 的过程中其实不太会使用到形式化方法这样的设计包括形式化方法其实在自然机科学当中也是一个一直以来是一个不是那么主流的方法非常简单的问题就在于比如说大家怎样对一段代码来进行测试来判断它这个正确性
我们基本的方法就是编写一些单元测试写一些测试样例然后判断输出的结果是否符合我们的需求但是形容的方法作为一个传统的话比如说从 70 年代开始大家尝试一种更加严格的方法来对系统进行建模比如说我们想要对每一个函数它的行为来进行一个性质的描述我们用证明的方法来描述它
会采取怎样的行为不会采取怎样的行为而不是像简单的 testing 一样而只是判断它不会有意外的输出就可以了总而言之它是希望一种符号的方法来对整个系统来进行建模实际上这种方法并不局限于比如说使用特殊的形容化语言来进行系统的描述
实际上我们可以用一种更宽泛的方式来理解这样一种想法比如说我们为什么要讨论逻辑规则逻辑规则实际上就是对于推理的建模就像比如说不同的推理不同的内容但是很多正确的推理都有它稳定的形式而这种形式是超出于具体的实力支配的一般的模式我们对它来进行建模就是逻辑学
比如说我们想要对算法来进行建模比如说我们想要具体的落实每一个算法到底对哪一个变量或者是实体来进行怎样操作实际上我们进行代码实现也是对于这样一种抽象的算法来进行建模
所以这些建模的想法其实都是一种更加宽泛的形式化方法而我们想要把它应用在大圆模型中其实就是为了想要用这种符号的推理工具来约束和引导这种概率模型的行为比如说现在的圆模型可以是
生成大量的不可控的内容但我们可以以这种方式来进行内容的筛选从中抽出正确的内容来作为综合回答这也是目前比如说 Metal Generation 一些比较常用的方法在形式化方面的一些具体应用一个引入形式化数学的典型动机是论文评审
为了聚焦主线,数学论文往往只会将最核心的思路写到论文里,但一些具体的推理细节很多时候依赖于作者表达和读者理解之间的默契,作者只要展示结论,在原则上可以用更严格更具体的推演即可。但现在数学中往往有几百页长的一个大定理证明,对于人工评审来说是一个非常具有挑战性的事情。
要将每一个这样的细节尝试手工地进行实际的补全来确认它的正确性意味着非常巨大的工作量但对于计算机来说它可以很低的成本快速的执行大量繁琐的证明搜索的任务可以为严格的证明检查提供彻底的解决方案唯一的问题在于计算机程序无法直接处理模糊笼统的自然语言描述因此我们要首先对数学进行形式化以一种更加严格的符号方法来对它进行描述
进行完善全面的形式化建模才能发挥算法的力量这也是当前陶志轩在推广形式化数学这种范式的关键动机另一个例子是程序验证为了测试一段代码的正确性目前主要的方法就是编写单元测试看输入输出是否符合预期但是测试的问题在于它至多能够证明一个系统在一组有限的输入下会出现错误的行为却无法证明一个系统在任何输入下都将会正确表现
而形式化会方法希望能用更严格的方法来对系统进行完善的建模在数学上证明每一个函数在任意输入下会做什么不会做什么从而提供全面彻底的系统描述总的来说形式化方法能够用符号化的方式对整个系统进行建模和验证而形式化数学就是使用形式化方法来对数学推理进行建模和验证例如我们可以精确地将数学推理归结为利用公理系统和推理规则进行的活动
数学推理的正确性就是判断结论是否可以通过推理规则正确的从前提中得出而这种活动我们可以用形式化方法在程序语言中建模从而将数学推理的正确性归结为代码编译的正确性听起来其实在 coding 这个方面大家对于形式化
已经比较了解了如果说在数学这个方面我们是不是也可以理解成形式化主要所做的事情是把数学建模或者翻译成一个比较确定的然后计算机可以去理解大元模型也可以去理解的这么一种语言
对 是的 一个非常典型的案例就是比如大家在写数学论文的时候基本上就是把主要的推理过程写在论文里面去至于内容过程之间的推理的具体的想法实际上是在作者和读者之间建立一种默契的也就是说数学家希望他的这个文本能够足够的简洁以至于大家能够仅仅通过自己的理解和想象就可以从每一部当中进行一个严谨的推导
而这些方面实际上是不会体现在纸笔层面的而对于计算机来说它需要对每一个方面都有非常明确和严格的确认和理解这就需要我们以一种更加严格的符号方法来对它来进行个描述这样的好处在于我们可以用计算机来检查所有的具体的情况具体的边界条件使得它能够以更加超过人类的这样一种
对于严格性的把握来对一个大规模数学证明来进行一个检查和验证这会导致比如说很多时候我们在
现代的数学当中有几百页长的一个大令你证明这个对于人工评审来说是一个非常非常挑战的事情而现在我们能够做到绝对把握的正确性的方法实际上就是形式化方法你就是说我们把它全部完整的翻译到形式化语言当中去然后用计算机的方法来对每一个具体步骤进行大规模甚至比如说对
几十万个不等是一一在进行检查到这样一种规模的状况实际上就不得不依赖于计算机或者说定义证明工具的辅助了这个是当前比如说陶哲轩在推广形式化数学这样一种范式或者工作方法的时候一种基本的 motivation
也就是说现在有了形式化这个语言,才能让这个当代的数学能够工程化,然后去解决更复杂的问题,然后如果没有这个语言的话,是不是可以理解成就是我们现在想要证明的一些复杂定理,或者我们想让数学再往前更走一步,其实是遇到了挺多挑战的,
对对这个其实这样的挑战比较类似于大家在讨论分布式系统的时候的一些关键的问题就比如说现在的我们有 10 万个 GPU 而让他们进行一个统一的运算和执行实际上是非常困难的这个主要来自于通信的问题
每个 GPU 它能够计算一部分的内容而它需要把所有这些内容来进行一个聚合再把这些聚合的结果来进行分发而这个对于通信的要求是很高的这会导致通讯的这样一种 budget 实际上是最大的程度上限制了我们能够使用分布式系统来进行大规模计算的这样一种设置而对于数学家来说也是一样的比如说现在
现在大家的困惑不仅在于我们对于前沿数学的理解不够到位而是在于比如说某些前沿数学家确实有了这样的思考和成果但他这些成果要对其他数学家来进行理解的话
实际上是需要花很多的通讯和讨论的时间的这会导致将人类数学研究作为一个整体活动的话会带来一种工程的瓶颈也就是说大家花太多的时间来互相传达对于
关于前沿数学的理解和掌握这会导致我们整体的数学进展变慢了这种变慢并不是因为我们不够聪明而是因为我们进行团队写作来说会面临像人越神话这样的工程化的挑战
而计算机的话形状提供了一种中心化的一种 oracle 就是它能够判断哪些是对哪些是错的我们只要相信它的判断就可以继续往前前进了而且它这些形式化之后的结果也会成为一种统一的知识库我们可以中心化的向其中来进行贡献和进行信息的提取我们可以用更加统一更加连贯的方式来进行整体化的数学研究这个是这样一个形状数学的一个终极的梦想
很有意思,也就是说其实形式化语言让计算机能够作为一个中心处理器去沟通不同的参与者或者研究者在数学证明或者研究过程中的工作。那我们其实看到在 AlphaProof 还有刚刚提到 DeepSync 的 Prover 系列的论文当中,其实都选择 Lean 作为训练语言的标准。
在所有的这些形式化语言当中为什么会定义成为一个最广泛采用的语言呢它有什么优势呢这个问题其实也是另一方面就是为什么我们用形式化可以对很多方面来进行建模而现在偏偏选择数学这个方向
选择 Lin 就是因为 Lin 对于当代的前沿数学的支持最高大家对它的参与最活跃以至于它的社区不断地有新的成员引入然后它的所覆盖的范围也快速地增长选择数学的原因就在于数学系是对于更加复杂的思维推理的一种系统化的设计的一个比较好的练兵场也就是说在数学当中我们是处理一些
非常高阶的抽象比如说对于具体演算实力的抽象以及对于这些抽象之上的抽象这种高阶的抽象如果说我们能够对这方面也进行一种非常精确而严格的形式化建模的话那么这对于一般的具体实际问题而言可能就不在话下这个是我们将数学作为一个科学皇冠来进行专门的研究然后来进行形式化建模的一个基本 motivation
然后至于选择令就是因为令对于数学支持是比较好的以及它的比如说开发环境比较现代很多问题可以达到迅速的解决这是一些工程化的想法而归根结底的话我觉得还是建基于为了数学这样一个基本的想法
这里华健其实刚好提到一个后面我们想问的问题就是选择数学作为一个研究对象它对其他的这个更抽象或者其他的领域有什么好处我们都知道这个数学和代码其实在 LM 训练当中包括 RL 当中是一个可以比较适合去做验证的领域嘛那
选择数学作为研究对象之后反过来说它对其他任务的泛化或者说更广泛的这个 IM 的推理能力啊还有抽象能力会有什么样的影响呢
从具体的使用案例来说的话比如说对于形式化方法我们可以把它继对数学定理来进行建模也可以对代码来进行建模比如说我们来对一个复杂的软件来进行形式化的建模可以判断出它是否会面临一些比如说内随泄露并发竞争之类的问题
而我们一旦能够实现用语言模型来做数学的图理的话那把它幻化到代码上面去做形容化建模也是类似的而从问题的结构来说的话数学的难题
难点在于它的抽象程度比较高而它的规模一般不会像代码那么大而代码的话它的主要的问题在于它的规模复杂性比较大比如说它甚至有比如说有十万行几十万行代码在一个复杂一些的软件工程项目上面都是比较常见的但这个在数学上是不是那么常见的
而我们需要以非常好的方式来在规模上来进行一个泛化虽然它在每个功能每个方法的这种抽象层级上可能不那么高可能是非常符合人类知觉的也就是说我们接下来想要把这套方法推广到代码验证的话需要在规模上有一个进一步的推广但是无论如何的话我们都认为除了将大圆波形应用在使用形态系统来进行建模之外可能还有一些其他的好处就比如说
我们希望对更一般的场景来进行一些形容化的支持比如说无论我们想要做怎样的一般推理比如说知识问答的推理比如说法律的推理 医疗的推理很多这样的推理也是一种演绎推理的系统凡是这样演绎推理的系统往往就可以用形容方法来做比如说从法律上的话实际上在逻辑学方面也有专门的法律逻辑这样一个专门的学科也就是说我们想要对法律进行一个专门的形式化
然后我们也可以以这种方式我们在用大圆模型来进行法律推移的时候也可以以同样的方式来进行相当的建模和验证来保证对法律条文的理解和运用是符合正确的规则的
总而言之的话我会倾向于认为形状化方法其实不仅会局限于代码和数学两个方面对于一般的领域的话也会有它的贡献而将生成能力的大圆模型和具有业证能力的形状系统进行结合我觉得可能是下一步的范式这个可能是从超过当前简单的单轮工具调用和简单的 deep research 进行检索之外
能对自己的生产能力来进行一个约束和控制我觉得这个是下一步的主要的看点嗯
这里我想补充一个小的问题就是我们其实聊到了很多数学这个领域的研究对其他领域的影响前面其实也提到数学领域其实率先出现了类似 test time scaling 还有 online training 这样的信号就是在这个形式化数学领域里面它有没有一些具体的这个技术或者说 tricks 作为这个案例
大家会把它相当于是先从形成化数学里面知道然后再去衍生到其他的研究领域我觉得目前来说最典型的就是自动形式化的想法我们是从自然语言数学把它翻译到形成化的数学从而弥补数据不充分的领域的数据构造的问题
然后事实上这方面的研究其实在其他领域上也有比较好的对应比如说在 Lama3 里面我们会看到它的技术报告里面有从更加常见的比如说像 Python 的这样的编程语言的数据代码把它翻译到更加不常见的编程语言的代码当中去来进行一个数据合成的工作
这方面数据合成也像我们在 Prover 里面做的一样它是一个从数据更加充分的领域推广到数据不充分领域但是在知识内容和逻辑结构上有一个继承作用的方法我觉得这个可能算是一个在 Prover 里面用的非常的核心非常的典型而且在其他领域上有一个比较好的对应的一个想法
华健也提到 DeepSync 发了 Prover 系列的 paper 之后其实就一直用 Prover 作为这个系列的名字没有再改过了能不能跟大家解释一下 Prover 是什么意思 Prover 就是定理证明器的意思它是和一般的比如说像 DeepSync Maths 这样的数学解题模型有一个非常好的对照就是比如说大家在做 DeepSync Maths 这样的数学模型的时候
往往是应用在一些问答题或者说填空题也就是说我们想要通过一些数学推理来拿到一个具体的答案通过这个答案的对照来判断这个题目的数学推理是否正确
但对于 prover 来说我们想要得到的是对于一个数学命题它是一个封闭形式的数学定理我们希望给它提供一个正确的数学证明每个数学推理的步骤都是以合理的方式从前提或者公理当中严格的推出来的而它最终不会到达一个确定的结果而
它的实现目标就是每一个证明步骤本身都是符合逻辑符合数学直觉的也就是说它是天然的一个过程监督的任务而不像一般的数学体系来语言是一个结果监督的任务它在任务形式上和以前的模型是有一个本质的差别所以说我们把它单独的作为一个 prover 这样一个名字那我们再回到
数学领域里面比较重要的几个 work 上面因为其实你也是 DeepSick Prover 2 的重要参与者从 2024 年 AlphaProof 发布到 DeepSick Prover 1.5 再到今年的 Prover 2 你感觉在数学这个领域 AI 和它的结合取得了怎么样的一些重要的进展其实从 Prover V1 V1.5 和 V2 相比最大的差别在于 V2 它在
Scaling 上有一个比较好的结果 DeepSeqProver V1 的主要贡献在于验证了在合成数据上做 scaling 会有很明显的效果
DeepSeq Prover V1.5 验证了,利用自然语言推理引导形式化代码编写是有益的。而 VR 则将更多精力放在了更高层次、更抽象的内容上,比如对一个复杂问题进行拆解和规划。这种高层次的抽象推理任务更能发挥大模型、参数量多、通用推理能力强的优势。DeepSeq Prover VR 验证了在模型规模上做 scaling 能够实现高层次的数学推理和规划,
将复杂的证明任务分解为具体可实现的目标是我从三年前就开始尝试探索的技术路线在 DeepSeek Prover VR 上我们成功地在 671B 的规模上实现了非常有效的证明分解和实现策略最终充分验证了这个路线的有效性
这个是 VR 相比之前的工作一个比较大的差别而这个其实我个人会觉得也是和之前的传统的 IL Agent 的工作一个比较大的差别就比如说我们传统的工作比如说围棋虽然我们说它的这个状态空间非常大但它的动作空间其实上是比较固定的也就是说就是这棋盘格这么大我们之多可以在其中的某一个点上落下一个子但是在数学上其实是不一样的数学上我们可以
理论上可以无限的提出任意复杂度的一些猜想定义中间的引力而这些是不会像围棋那样有一个非常明确的有限有界的一个动作空间的设定的这就是为什么在过去的简单的
直觉性或者说立即映射的一种 IL agent 难以做得好而现在具有通用推理能力的大元模型能够做得更好的一个根本的差别具有推理能力的大元模型在中国经过 IL 的进一步训练之后确实会做到以前所难以做到的更加难以控制难以进行规划的更加 general setting 比如说像代码比如说像数学这也是目前为什么能取得和之前相比那么大差别的一个
进展的一个主要原因在 DeepSeekProver 三部曲的发展过程中我们也看到使用大模型进行自动定理证明的研究领域也开始越来越活跃在测试基准上的表现不断取得新的突破这都证明了这个领域的长期前景
对确实在 AlphaGo 和 AlphaFold 发布的时候其实 LM 还没有出现他们仅靠 RL 就取得了比较好的效果但是真的涉及到人类的皇冠就是数学这个问题其实是在 LM 出现之后才
取得了进展的所以这里面可能有华健刚刚提到的一个原因就是搜索空间的不同我不知道这里面还有没有其他的什么原因能不能给大家讲一下就是比如说在 AlphaProof 包括这个 Prover 系列里面 IM 可能分别扮演了什么样的一些角色
我觉得另外一个比较大的差别就在于比如说对思维链的使用上实际上比如说我们有一些理论的工作证明了我们在回答之前先进行长连号推理的话实际上是相当于对一个模型的规模进行一个扩大比如说对于模型的
宽度进行的一个增广使得我们可以对于不同的问题采取不同的一些计算 budget 的设定这个在理论上是有保证的就会导致比如说我们对于更复杂的问题可以等效的把模型放大然后让它以更加充裕的时间来进行思考和判断这包括更加复杂的思维流程包括长颖条的推理包括对于具体大的
目标的一些分解和化解以及和以往支持的一些回忆所有这些作为复杂思维过程的话在于之前的工作当中它因为它是一个及时的输入输出它需要把所有的这些计算和推的步骤都在简单的神经元的全部当中就已经进行
这个会导致在之前的话对于复杂的任务的训练实际上是非常困难的事情但现在我们掌握了指涌思维链来进行一个扩展的阶段的话这些
更加复杂的情形和生存目标都可以慢慢的通过在自卫链的大的框架之下来进行一个更加充分的计算 budget 的使用我觉得也是另外一方面现在的我们做退任务的情形和之前做的不一样的问题这也是为什么比如说从 O1 到 O3 它能够在花更大的推理的 budget 下能够在
推理的结果上有一个持续的可靠的提升这个就表明了我们解决推理的问题的话 test time scaling 其实是一个比较可靠的长期发展路线这个是比较震撼的事情也就是说 IAM 在数学的研究当中其实不仅扮演了拆解任务这么一个角色更重要的是它其实让思维链就是 COT 的过程
这个能力的增强起到了很大的作用在数学领域里面的这个思维链和我们平时使用语言模态的时候解决普通问题的时候的这个思维链你们观察到有什么不一样吗
数学的话其实我们所处于的数学有多种层面比如说在简单的层面的话之前都会测的比如说 Math 数据集的话它往往是一些偏重于计算和简单推理的问题它的困难在于它的对于数学技巧的使用上就比如它会对一些比较微妙的数学结构来进行一个专门的 guidance 以及和以往的策略来进行一个简单的对应
这个是在比如说高中进化水平的数学上一个比较突出的特性而比如说在研究水平的数学上的话它会花大量时间来对一个抽象概念来进行深入的理解和迁移就比如说我们在理解很多抽象概念的时候实际上是需要将它在一个更大的语境之下来进行理解的甚至比如说会举很多具体的结构的例子辅助我们来对它进行一些更好的推理
而这会导致我们花大量的时间在定义和定义之间的联系以及从简单的推理的这种模式推广或者类比到其他的模式之间的问题这些和通用的推理的差别在于它会在更加抽象的领域上有一个更加复杂的表现我们日常的
推理的话比如说我们想要做一个路线形成规划比如说 Manus 现在能够为大家做点事情这些方面其实更多是对一些信息的处理和综合就比如说我们现在调用了很多工具拿到了很多不同来源不同内容以及不同形式的数据我们想要把它整合在一起这方面推理是大家在日常生活中比较常见的
也就是说对于数学来说更多的推理内容是放在了对于抽象的理解和运用上而对于日常生活来说的话这样的推理往往是应用在对于杂多信息的整合和分析上虽然同样是使用推理这个概念但是具体的使用步骤当中其实是不一样模式的一种比较典型的例子
其实我还观察到在这几个数学论文里面有一个比较有意思的点是 IM 有的时候还承担了一个产生数据的这么一个作用在 prover 里面 IM 其实产生了一些用来做 SFT 的这个冷启动的数据
在那个 AlphaProof 里面它的训练过程好像也是先收集了 100 万道自然语言的数学问题然后把它用神经网络转化成了一亿道这个形式化数学的问题然后再去不断地用强化学习的方法去
证明这些数学题我看到它从 100 万题扩展到 1 亿道题这个增量其实还是挺大的我不知道这在数学的研究里面是一个比较常见的做法吗因为其他领域里面这个合成数据都是一个比较大的问题不知道这是不是表明在数学领域里面合成数据的问题已经解决了呢实际上我们在 Prover 这个范式下为什么会这么密集的使用合成数据以及我们为什么做的这么早
这个实际上是一种不得已而为之的一种决定就是因为实际上使用形人化数学来进行模型训练的话它的自然数据是非常非常少的
这是因为比如说使用另一种的语言来进行编码的人类专家的数量本身就很少而且它需要同时在数学和代码和逻辑方面都有非常专精的理解才能贡献出能够满足机器验证的一些有意义的代码这个数据产生是非常非常难的这会导致我们想要训练一个专门的这样的大模型实际上在预训练阶段是远远没有这样的数据的
这就导致 prover 相对于一般的代码和数学来说它是一个非常非常特殊的领域它给我们提出的问题在于当我们没有人类产生的大规模的自然数据的话我们怎么来进行复杂的推理环境的理解和掌握
实际上我们是花了大量时间来做这样一个事情然后我们所提出的一个基本的想法是叫做自动形式化也就是说我们想要从一些数据相对来说更加充足的领域把它进行一个知识和内容的迁移把它翻译到相对来说数据量比较小的领域就是形式化的领域
也就是说我们把非常多的自然语言数学的内容这些内容可能是人类的习题人类的论文人类的教科书这样的自然方式来进行产生的数据把它翻译或者整合到一种特殊的形式也就是形状数学的形式
这个是一个我们来进行数据合成的比较好的一个出发点这是因为我们有足够好的一些虽然在形式上不同但是在内容上基本上是一致的数据来源我们只是进行一个翻译的工作而不是进行一个从零开始 from scratch 的一个
构造的工作这会导致我们虽然是合成数据但是相对于从零开始的合成数据来说要更加简单一些代码的领域上大家做合成数据的话是需要源模型自己的独立来提出问题然后根据这个问题来编写相应的代码和相应的测试样例并且用这样的测试样例来衡量代码的质量这会导致大家用源模型的时候是一个
从零开始空手套白狼的这样一个想法这会导致实际上是同样是合成数据但是这样的方式从零开始构建的模式的话它的难度是会更高的所以说其实我觉得是不太能够同日而语的而另一个问题比如说像刚刚潘莉提到的从 100 万道题扩展到 1 亿道题这个增量是怎么实现的这个实际上很多方面的来源比如说 AlphaProof 团队他提出了
一方面是同样一个资源语言数学问题它可能会翻译成不同的形式化的形式这比如说大家同样对于一个问题来进行数学建模有不同的方法和策略一样这个是一种非常直观的想法而另一方面的话实际上 apaproof 团队它是花了很谈大的精力来做一种叫 test time training 的工作实际上这个工作是他们在去年 7 月就已经提出来的甚至比 OE 这种 test time scaling 的方式还要更加早一些
这个的基本想法就是说我们想现在想要解决一个极端困难的问题而比如说一道 IMO 的问题我们把它进行一些变形或者拆解比如说我们对条件来进行一些具体化或者说进行一些放松
然后对在这样一种更加简单一些的形式上尝试用模型来进行证明如果说他能够把这样一个问题能够证明出来的话就认为他在一种比如说子环境或者子任务上取得了突破 Afterproof 团队会把它进一步加入训练数据当中去然后使得模型能够在聚焦于解决同样问题的过程当中不断地增加对这道问题的理解和对之前尝试的记忆
它的能力不断上升的话就可以解决更多的困难的责任的拆解以至最后把主要的问题核心问题也能够来进行一个解决这个想法其实已经相当接近于现在大家讨论的这种 online training 的 setting
我们怎么样解决一个问题如何在线的和来进行交互如何能够通过拆解和规划的方式一步一步的探索解决这个问题的结构和形式我觉得这些其实都是对于其他领域来说有非常有好的借鉴意义的一些方法
这个很有意思,包括我们其实也经常会想 AGI 或者甚至说 ASI 有没有可能先在一些领域里面实现比如说先在代码领域里面或者先在数学里面实现包括刚刚华健提到的这个 test time training 甚至 online learning 好像都是我们认为的 LM 的下一个范式但是
你觉得它有没有可能就是说可能不一定在所有的领域实现但是先在数学这个领域里面或者代码这个领域里面探索出来对我个人是倾向于认同这个观点的实际上这个一个想法和比如说大家在逻辑学里面来探讨问题的做研究的方法是一致的比如说大家是怎么样发展出现在逻辑学的这样一种逻辑系统的在一开始的话也是在尝试对数学来进行一个推理的建模
因为数学是一个比较干净整洁的领域它不需要和物理世界来进行昂贵有危险的交互我们只需要在纯粹的思维世界里面进行实验就可以了在思维的空间里面我们已经可以得到某些想法是对的某些想法是错的仅仅根据这些想法和比如说公理前提之间的矛盾来进行判断的这其实就为我们带来一种非常好的实验的场景
实际上这个想法比如说和机器人里面大家是做在虚拟环境里面做 simulation 的数据采样和训练而不是直接从一开始就是拿一个真实的机器人来进行抓碗之类的操作这样的想法是不谋而合的
也就是说我们先在一些形式和内容上比较整洁可以进行更好的建模和方法的探索的场景下能进行一个成本比较低可以进行大规模探索的方式的方法探索之后
再把不论是方法上还是对于模型还是在那样的场景协下训练的模型来进行流域之间的泛化上都可以以这种方式先在这些领域上做了工作然后再推广到一般的更加困难更加接近于日常生活更加靠近物理世界的更加复杂的场景我觉得这个应该会是接下来一个大致的方向
这个点很有意思,也就是说把这个形式化数学或者数学代码这样的领域当成是其他更复杂的,然后更工业化落地这些领域的一个 simulationsimulation 的问题解决之后可能再去解决更物理世界或者更现实世界的一些问题
是的因为我们刚刚讨论的是这个 AlphaProof 的工作不过它毕竟好像不是一个开源的工作相比起来好像 DeepSeek 的这个 Prover 系列其实是这个领域里面目前第一个开源的重要里程碑式的这个工作除了我们说的这个用这个 IM 去做这个任务拆解之外华健能不能再分享一下觉得在这个 work 当中有哪些是你觉得比较具有亮点的比较具有创新意义的
还有一些有意思的比如说同样是聚焦于任务拆解实际上它是一种比较接近于 multi agent 或者说对于把同一个任务让不同的模型来进行代理的想法比如说我们在训练数据的构造当中是同时使用了 DVC v3 和之前的 DVC v1.5 来进行数据的构造的
对于同样一个大的任务我们使用大的模型来进行任务拆解和规划然后用小的模型来进行一些细致的具体的征服目标的形成化的补全而这样一种方法的话我们既可以在宏观领域在整体思想上利用大模型的推理能力也可以
在非常小的需要和环境进行高度快速交互的这样一种场景之下利用小模型的这样一种快速推理低延成本以及可扩展的一些好处这个带来的比较有意思的一点在于我们接下来比如说想要在其他的场景下在复杂推理的任务当中去使用这样一大圆模型的话
我们是否还要像现在一样使用单一的大模型来完成所有的任务还是说我们可以把用一种更加 agent workflow 的方式来对一个任务来进行一个组任务的执行方式来进行一个组织对于一个复杂的 IM 的任务或者其他的图形推移的任务或者说语言推移的任务我们也可以以这种方式来进行模型之间的合作现在大家
虽然在 test time scalability 上我们确实发现在上面不断的增加 training budget 下我们可以拿到更好的 tweet 的效果但是这对于我们的 tweet 的 infra 其实带来了非常大的挑战这就是为什么现在很多厂家正在研究怎么样来控制对于同一个问题的我们的 test time scalability 或者说 long cot 的 token budget 的控制比如说小问题的话我们就不要做过度的思考
而让模型主动的来用非常及时问答的方式来进行一个讨论
对大问题的话再进行常理条的推理也就是说我们需要模型对于任务难度甚至不仅是模型对于这一整个推理系统可能包括不同的模型不同的工具这样一个大的可以适应的 workflow 能够对于任务的难度来进行感知和这样的感知会导致我们可以对于不同任务设置不同的算力的需求来进行推理的实践
而以这种方式虽然一方面对于我们比如说 Tescan 的对于算力推理的使用来说会是一个更加复杂的调度问题但是另一方面的话其实也是一种我们能够以更加可学的方式来使用模型来进行复杂任务而不对推理系统的算力需求一个无限增长的扩充的
一个比较好的一个解决方案总而言之就是说我希望能够实现一种比较模型之间混合模型和工具之间混合的这样一种更加灵活虽然更加复杂的这种 agent workflow 可以来解决一些不同难度不同领域不同方法的这个推理任务这个不仅局限于使用比如说现在的专家模型 MOE 模型来进行这样一个并行的训练我觉得混合系统也是可以一个比较好的机会
华晋说的这个观点其实跟陶哲轩说过的有一个观点有点类似数学尤其是复杂的这个数学证明问题就是它可能比我们大部分人想的更像一个复杂系统然后如果说有这个计算机和形式化数学的帮助的时候它甚至可以让几百个甚至上千个人一起去合作每个合作者只需要负责去做自己的部分
然后这个听起来其实很像一个天然适合 agent 或者 multi agent 的思路去做的一个工作
对 是的 甚至比如说现在的我们的用形容数学的一个基本方式是把一个复杂任务来进行一个蓝图的拆解把这个蓝图中的每一个具体任务交给不同的人来做然后不同的人的这种结果只要他能通过计算机的验证的话就认为他是可靠的正确的我们把它聚合在一起实际上就已经得到了对于一个完整的任务框架的全面的实现
其实可以非常方便快捷的把它变成一种 multi agent 的想法甚至一种人机协作的想法就比如说我们同样是对一个任务进行拆解如果这个任务是足够简单的我们完全可以让模型来进行独立的探索和解答的尝试而只对于复杂的问题来说采用人工来进行参与这会导致一种更加自动化的做数学的方式可以为我们所接受
而这样一种人机协作的模式的话理论上的话也可以推广到其他的形式比如说代码的方式让人和 code agent 来进行协作以及限制其他的领域上去我觉得总体来说是一个非常好的非常值得期待的场景
那关于这个复杂的系统不知道华健能不能再展开讲讲因为我记得你在有一个分享当中其实提到过一个观点现在的这个形式化工具需要从静态的 theory improver 转向具备自我规划自我修复还有自我知识积累的能力的这个 proof engineering agent
这里提到的自我规划自我修复还有自我知识积累这几个能力听起来好像都是我们对未来 agent 的一个想象是的这也是为什么我会认为行业数学是我们发展和探索 agent 的一个比较好的场景以及为什么我会在这个方面专门会做一个这样的 benchmark
这样一个想法就是即使将软件工程当中的一些 agent 探索的模式迁移到了数学当中来如果说我们也想要再像代码一样对数千个文件来进行一些修改上的处理从里面抽取出关键的内容并且对其中的某些文本来进行修改的话我们在数学上应该怎么做这个我们在
形容数学上当中的话有一个相应的概念叫做 proof engineering 它的意思就是说我们所掌握的这样一套软件不仅是一个通常意义上的软件工程的项目而是一个证明的项目而证明的项目就意味着它带有两方面的内容一方面的内容是证明的内容就是说它在尝试解决一些怎样的数学问题它尝试对哪些定理来进行证明
而另一方面的话它涉及到这些数学的意义和计算机验证工具的一些交互就比如说我们需要以简单方式把它转化成一种机器可以理解的语言表达方式才能够更高效的为这种机械的检查所接受无论是哪些方面的话这个整个都会是一个非常大的规模就比如说现在
对于之前所讨论比如说 300 页的开播的猜想的一个形式化的话它实际上是需要几万行代码甚至数十万行代码这样一个规模这会导致我们同样也是需要用软件工程的方式来进行大规模的长文本的推理和修改而
而另一方面的话不仅我们希望对它进行一个单元性的修改比如说像简单的往里贡献新的 feature 修改出一些已进入的 bug 或者说提升整个系统的效能我们是希望能够在这基础上来进行一些更加大规模的重构而这个重构和软件工程的重构的话
在一些方面上有些差别就比如说它不仅仅是在代码形式上能够更加满足人类的需求以及在编码的结构上能够更加高效更加满足计算要求
它还涉及到一种更加高层次的数学的理解,就是说我们怎么样能够提出一些在数学上更加强大的抽象,能够统领和聚合各方面的问题的理解,能够让具体的问题能够在这个框架当中有一个通用的解释,这个是 Proven Engineering,钻对于 Software Engineering 来说一些额外的内容,我觉得这个方面的话会导致这样一个问题,
是一个更加有深度有更多抽象层次结构的一个问题可能对于我们探索 agent 的话也是一个不错的环境
而另一方面的话一旦这样的场景能够有一个非常好 agent 的解决方案的话它对于我们人类数学想要走向一种形成化的一种跨越来说也是一个非常好的契机而这是因为现在大家形成化数学的话仍然局限于一些比较实验室比较学术性的领域的探索而没有真正走向
全体数学家的一个日常工作的问题主要是在于形式化本身是一个比较困难的任务它需要专家的长期的努力才能够把一些复杂的数学推理进行一个形式化的翻译和整理的工作
这会导致比如说像 Lint 的数学库 Mathlab 这样的软件工程项目它的扩展实际上是非常缓慢的它实际上是远远无法达到我们所期望的能对人类数学的全体知识来进行一个编码和整理的这样一个梦想
而一旦这样的 agent 能够实现的话它对于这样一个梦想会是一个非常快速的加速的过程如果说这样的 agent 实现的话接下来十年我们做数学方式可能会完全不一样我们可能不再做一些非常简单的直笔推演而是直接我们使用自然语言和一个具有形式化能力的 agent 来进行交互我们告诉他我们想要处理的是什么样的数学问题我们希望得到什么样的结果
而他会自动的把这样一些任务的目标和一些基础的数学概念把它翻译到形式化的领域当中去在形式化的领域当中来进行一个推理思考以及验证并且把这种验证通过的完整的解答能够再翻译回自然元素当中去作为一个人类可以理解和接受的一种回复而这样一种完整 workflow 的实现的话
可能会对我们的数学研究会有比较大的影响就比如说当数学家想要确定一些比较简单的具体的实例或者具体的猜想的正确性的话我们就完全不需要把这样的任务再包给比如说人类研究生来做而是可能像大圆模型的 agent 来做
它无论是在成本上 在规模上 在速度上都会有简单人力这种手工的方式来进行工作有一个非常大的提升可能接下来大家做数学的速度会越来越快因为我们很快的可以判断一些猜想的正确和错误能够达到相信它的正确性并且它在结构上可以更好的理解的一些证明
更进一步来讲的话如果说我们在数学上的使用能够到一这样一种非常便利的程度我们就可以在更多的领域来使用数学的结论比如说我们想要在一些软件工程的项目上来推测一些得有程序和代码的比如说
时空复杂度或者说对于一些运筹优化的问题想要做一些计算上的一些优化和整理我们也可以用这种方式来用一种这种非常好的可靠的数学 agent 来做总体来说的话用这样一种形式你这样一种 agent 来实现这样一种梦想的话可能对很多具体现实的领域的应用来说都会有非常大的改变作用
这里华健其实提到两个点一个是这种计算机的或者说形式化语言在实际的数学家和研究者当中使用还不是特别的普遍因为它还有大量的人类现存的数学题没有被翻译过去对吧对
不知道有没有一个概念就是现在已经被形式化的这个数据大概占人类的这个总的高质量数学数据的百分之多少现在在数学专业本科一二年级及以下的数学知识的话已经有一个非常好的表示而对于前沿的数学比如说研究生级别博士级别是研究者级别的数学领域的话只有一些非常零散的形式化的结果
那如果我们想要推进这些研究生以上的更难的数学问题的解答或者说更难的证明不知道华健能不能举一两个比如说特别难解决的问题作为例子来说明一下就是可能当 AI 和 agent 的发展到什么情况下我们能取得这样一些比如说超出人类最顶级数学家这样的突破
这个问题其实说有两个层面第一个层面是我们现在想要做的是很多问题人类数学家已经有了非常好的结果已经有了具体的证明我们希望让形式化的数学能够覆盖这方面的内容
而另一方面是我们想要让具有形式化推理的大元模型 agent 可以开拓新的数学教育比如说解决一些人类提出的开问题或者说甚至提出一些新的数学的想法这个是第二层面甚至更高层面的一些追求
而具体来说到第一层面的话比如说现在在帝国理工大学有一个专门的项目是想要形式化费马大定理它是需要把之前的很多的大规模的文章来进行一个数年的时间用很多人的精力来进行一个形式化事实上这方面的话我们立刻有的机会就是可以在这样一个长期的大项目当中融入我们的 agent 的无论是发展还是应用也就是说我们能够帮助
数学家能够更快的来进行形式化的努力这方面的结果的话目前的技术来说已经一定程度上可以帮助到他们了比如说
我们可以让原模型来进行从基础的数学库当中抽取核心在想解决问题相关的一些引力和定义这方面是非常好的可以解决用 E-Binding 就可以做而另一方面比如说对于现在做了一些需要具体补全形式化步骤的真空目标的话也可以用比如说像 DeepSickTrover 这样的模型来进行一些补全它也能够理解上下文当中已经更新过的内容以及新
拿到的这样的一个结果但是下一步的内容的话比如说我们想要
对一个人类编码的一个比较正在暂时执行的一个文件来进行一个梳理和扩展的话这方面就需要 Proof of Engineering 能力的 agent 来做这方面的话就是我们现在正在尝试翻转的一套能力更下一步的话我们需要对整个项目来进行各个高层层的理解比如说同样是一个问题有一些学生的话的策略是好的
无论是对于当前语言还是对于代码上的翻译来说的话都是不那么方便那我们就应该去排除我们希望让这样的 agent 能够独立的像人类一样不断的提出形式化策略的 candidate 然后自主的来进行实验从中筛选出足够好的来作为简单来辅助人类来进行这方面工作的自动化这个又是下一方面而这方面的话就是下一阶段工作了
而虽然说提出猜想并应应着猜想一些尝试在目前工作当中也有做过我们在 2023 年提出的 Nagelprover 工作以及现在斯坦福大学一些比如说 STPprover 这样的工作也是不断的在这方面来进行探索但具体能够主动的提出足够好的猜想来解决足短的问题的话仍然有一定的距离
对于我们做大圆模型 agent 来说提出了一些具体的挑战而对于第二阶段的话我们需要让圆模型主动的开拓数学疆域发现一些新的猜想证明一些等待解决的开问题的话这就需要更加复杂的推理和对数学理解能力
我们这方面是寄希望于将自然语言数学的比如说现在的常链条推理能力和形式化的结果来进行一个结合也就是说我们能够通过像 O3 甚至 O4 这样的足够强大的推理模型通过常链条的推理来发现一些可能有用的数学结构数学抽象那么将它落实为具体的数学推理过程
然后我们能够起到的作用是将这些数学的中间的产物把它翻译到形式化的领域当中去去验证它的正确性能够帮助这种探索起到一种非常好的监督和引导的信号
我觉得比如说第二个大阶段的话可以这种方式来将现在主流发展的自然语言数学和我们所努力的形状数学的这种 agent 验证的框架来进行一个结合这方面的话可能再快的话接下来两三年时间也会有一个不错的工作现在的这个模型的能力已经可以部分实现你说的第一阶段的工作
而第二阶段就是开辟新的领域或者说让模型提出新的更高阶的数学问题其实现在的模型能力还做不到如果做不到的话它现在主要欠缺的能力是什么呢我会认为的话这样的欠缺仍然需要在自然语言上有一个更好的解决就像比如说大家仍然需要在 OE style 的模型上来这些更好的努力比如说无论是在
预训练阶段有更高数学推理能力更高数学推理复杂度的这种数据的合成和筛选以及在 post-training 阶段对 RL 能够在不断的在一些从简单到困难的具体的环境和任务上有一个不断增强的预训练的步骤这方面其实是和现在主流的比如说推理模型的训练的详细的问题是一脉相承的
那在这个训练的用强化学习训练的这个过程当中有几个组件可能是特别重要的一个是前面也提到的环境然后一个是可验证然后还有一个可能是我们这个 RL 的这个算法就如果分别说一下介绍一下这几个组件在数学里面它是一个什么样子或者说我们能不能去把数学和代码进行一个对比
这两个领域里面它所需要的强化学习的环境和 verification 还有算法有什么相同和不同对现在无论是在数学和代码上大家能够有一个能 work 的 RL 的一个算法的话最关键的在于 valuation 或者 verification 的设定对比如说大家在之前为什么 RE still 能够 work 很大程度上是因为它能够基于一些非常好的
rural base 的一些 variation 的设计这样的一种反馈机制的设计能够更不容易被 hack 而且能够提供更加精确和可靠的
一种反馈的结果而只要我们模型足够大然后 Io 的算法足够好我们就可以不断的和这样的结果来进行一个匹配和交互这样模型的能力就会有一个比较 promising 的增长的结果这个问题也就引申出来了如果说在某些场景下我们没有直接 on-shelf 上手可用的 evaluation 的话该怎么办这个其实就呼应了比如说姚顺宇在提出比如 AI 下半场这种
这样一种论断里面提出 evaluation 相比 train 更重要这是因为比如说我们现在模型是一个很好的锤子但是我们现在已经没有足够好的钉子了现在 IL 需要跟环境进行交互而这种交互是一种任务中心型的交互
也就是说我们往往是为了解决一些在模型能力范围之内有足够的奖励信号而且又稍稍比他能力要稍微高一点点的环境下的话才会对他的训练结果有一个比较好的提升这个意思就是说如果说我们的模型一直在做一些非常简单他只要简单的 simpling 就可以
非常稳定的解决了一些任务的话那他就不会得到本质的断裂而如果太难的任务的话他又不会拿到任何的正的奖励信号他也不会有明确的优化的方向这就意味着我们怎么样来提出更好的 evaluation 的 benchmark 实际上是一个比较关键的任务
这个需要比如说在数学上的话我们需要在无论在难度上在设计的领域上甚至更具体来说同样是比如说是聚焦于
高中水平的竞赛知识的话我们需要在他使用的具体的技巧上以及解析的策略上都有足够完备足够充分的测试和执行的任务和环境之下我们才能够用已经有的这种 IL 的算法能够来更好的训练模型这就是为什么我们又说 Evaluation 相比 Training 更重要我们要使我们的 Benchmark 的设计或者说 IL 训练当中 Prompting 的设计
更加符合我们对它的实际应用的需求也就是说我们的 Evaluation 的这种环境更加全面可靠准确的覆盖了我们下游做测试的时候的推理需求的时候我们才能够用这种 R 的 setting 把它 work 起来我觉得这个无论是对于代码还是对于数学来说都是一个比较核心的一个
一个场景和任务这个很有意思就是这个 verification 或者说 benchmark 既不能太简单也不能太难就是既不能太容易被 hack 然后也不能让它没有任何的这个正反馈对 是的华健最近其实你也发了一个新的这个工作叫 ApeBench 这个 benchmark 的设计思路还有它里面比较有意思的一些地方是什么样的
这个其实就非常接近于刚才我们所说的那种 proof engineering 的想法希望对大规模的文本无论是自然元文本还是代码文本来进行一个修改并且这种修改是可以和验证和执行的系统来进行交互来判断它的正确性的
也就是说我们希望把这样一个想法应用在数学当中去使得我们的模型 agent 可以更好地完善一个大规模的数学库而不仅仅是完善一个孤立的任务也就是说我们希望在行刷数学方面也能够实现一个从比如说 human evil 到 sweep bench 的这样一个跨越我们希望从孤立的定理证明也就是从
只会解析的模型发展到一种可以主动的对一个非常大规模的已经有一定积累的知识库来进行一个扩充维护和整理的这样一种工作我们希望模型不仅能够孤立的完成一些具体的任务而且能够从这些任务当中获得一些收获和思考
这些思考能够通过形容的方式能够通过对已有的数学库来进行扩充的方式来进行一个沉淀沉淀到我们的统一的知识库当中去在后续的其他的任务当中的话我们可以利用这样一些能力从已有的知识当中抽取出已有更好的经验来用经验来
帮助模型更好地解决更复杂的问题也就是说我们会认为无论是对于长文本问题大规模定理库的解决还是说对于知识的积累这个本师都是他想要能够对模型来进行评测以及引导模型进一步发展的一个基本的 motivation
这个 benchmark 它所主要体现的核心思想我们了解了有没有更加具体的例子或者更简单的方式能让大家直观的理解一下这个 benchmark 它考量的任务和考量的这个方式是什么样子的
好的,我们这个 BatchMap 的话现在的设置还是在第一阶段第一阶段是想要对单文件来进行一个修改工作也就是说我们单文件的话一般就是聚焦于一个特定的数学领域我们想要在这样一个数学的分支当中更好的把一些人类数学结果来进行一个形式化的融入
模型需要一方面理解现在我们的形式化框架实际上的风格和结构来进行一个编码的以及我们如何把自然语言的数学的结果和这样一种编码的方式来进行一个结合
以及另一方面的话还涉及到一些重构的工作也就是说我们现在希望对一个复杂的定理它有一个非常冗长的证明希望把它进行一些合理的拆解来进行一些模块化的使用这方面的 idea 的话就已经非常接近于软离工程里面的一些设计思想了比如说我们现在想要在一个代数的基础上想要加入一个新的代数结构
它是对于一些已有的结构的一些进一步的具体加了一些更强的功力或者说对一些方面来进行一个放松我们想要将它和已有的定义和结构来进行一些结合
使得我们在具体使用当中的话我们可以在这种更加具体的结构和更加一般的结构之间来进行跳跃来方便来进行一些证明一些目标灵活的一些场景这个是我们这个 benchmark 想要解决的一些具体问题也就是说如果说我们想要在这个 benchmark 上有一个更加好的评测结果的话
我们实际上是需要对形式化数学的这样一种对代码的理解对数学的理解以及它们之间相互互动的理解都有一个更好的掌握之后才能够取得更好的 score 然后我们也希望这样的 score 能够帮助大家能够知道研究然后来判断我们的模型是否已经比较接近于人类使用者的使用需求了这些都是这个本身一些比较细节上的一些使用方法
也就是说之前的 benchmark 可能更侧重于看这个模型的解题能力但现在这个新的 benchmark 更侧重于看它不光是解题还有使用代码使用工具甚至可能涉及到多步骤多文件去解决一个复杂问题的能力
对,是的,这个其实上就是我们想要想象的一个在数学上的一个 agent 想要达到的能力基本上都有什么我们进行的一个列举分析以及对于弱势到具体奔驰慢离中努力
那会不会有这么一个情况现在虽然我们分别去看有专门做数学的模型有 coding 很强的模型同时他们基做的都是 LM 最后会有一个融合的模型它可能在数学代码还有其他的一些领域上都做到很强以后可能不会再有单独的代表顶级数学家的模型出现
对我觉得理想情况下一定是这样的就比如说形容数学就提供了一种一个例子就是说在这个领域下我们既要有代码能力也需要有数学能力这个例子其实并不是
单独的很多情况下我们都是需要在两方面都有足够好的能力才能够解决一些问题即使在数学研究的话很多时候我们也是需要进行一些仿真建模的方法用一些专门的资源基带处工具来进行结构验证的方法而这些的话实际上都是需要代码来进行融合的也就是说我们想要让模型在数学上做得好
其实很多时候随着他做的任务越来越难他的代码能力其实是不断的增长的这其实反映在很多比如说像金融数学这样领域的话很多论文它实际上是基于一种非常大非常复杂的代码库的实现才能够完成一些结论的仿真和模拟以及计算的
而对于代码的话比如说很多时候我们需要对于一个常用的程序尤其是涉及到自传密集型的程序对它的复杂度对它的自传效率来进行一个估计很多时候也是需要一些比如说离散数学的工具来做的
如果说代码模型不仅想要让他能够生成代码而且能够分析代码根据这种分析的结果来进一步优化代码的话数学能力可能也是必要的这个只是数学和代码界的互动而对于一般的科学的互动来说的话这个会更加常见很多领域比如像物理领域他会用很多的数学工具比如像其他的领域的话他也会用一些很多信息计算的方法
也就是说我们即使在一般的科学的美术目标的 Agent 之下我们也是需要对各个领域都有一个触类旁通的一个模型才能够有一个对具体的场景有一个比较好的应用的结果我个人也是倾向于认为最后我们应该是有一个全材模型而不是现在有一个专材模型现在专材模型的这样一个设计只是因为它是一个时代的特殊产物
我们无法在比如说像在 post-training 阶段兼顾各个领域之间的长处和特性因为比如说在 SFT 阶段的话不同的领域之间数据的混合会出现翘翘板的现象就比如说这方面优化好了另一方面可能就会遗忘而这些基础能够解决的话我相信以后有一个全面都做得很好的通财模型一定是会出现的而且这方面也是大家的共同需求
这个点很有意思确实我们之前也听到很多 researcher 会提多模态数据的加入可能会影响语言模态的这个智能但是其实大家都在寻找一个方法并且可能未来也会有进展就是让这个多模态数据的融入不仅不会影响 IM 甚至还会提升智能所以就是不同领域的这个数据融合可能未来也会有这么一个趋势
嗯 是的 是的华健在分享中提到的一个观点就是形式化验证还有这种动态的或者就是自主的这个学习机制的结合可能会催生出一个新的 AI 你给它取了个名字叫 certified AI
这个概念不知道它的背后的思想是什么样的能不能给大家解释一下这样一个 Celifat 的 AI 其实它的提出是和 Generate AI 相对就是说现在的国型它在生成上有一个非常好的能力比如它能够很快速地生成
数万行甚至数十万行看起来非常好高质量的代码它非常符合人类的编码习惯我们人类进行审查的话一下子也看不出来什么问题但它在长期的部署和运用当中的话可能会暴露出来很多问题无论是在安全性上在使用效率上还是对于
可维护向上都会有很多不那么符合人类需求的方面而 certified AI 的话就是我们不仅需要生成而且需要我们对它的生成质量有一个比较好的控制就比如说对于数学来说的话
就是我们不仅需要模型能够生成出来一个篇幅非常长涉及到的数学的推理非常复杂总体来说大概满足我们的需求而且需要它的每一个推理步骤都是正确的它能够全面的满足大家对于数学工作的所有要求
这需要它对于自己的生成结果有一个比较好的验证或者说一个检测就是 certification 的概念比如说在我们这里的话就是用形式化方法就比如说我们想要用形式化建模的方式来对它进行一个翻译在翻译到形式化数据的一个结果之后我们可以来通过计算机辅助的方法来对它的结果来进行一个验证
而一旦这样的验证通过的话我们就认为这样一个生成结果它是通过我们的检测或者说一个质量认证的结果的而这样的模型我们称之为 certified AI 一个模型不仅需要有生成的能力而且还需要对它的生成的结果有质量控制和检测的能力
而他只有通过这样的外部工具的调用完全确认了他的这套生成的方法是满足所有需求之后才将其返回给人类使用者人类使用者一种方式可以完全可靠的相信他一种生成结果的话我们认为这对于当前的只管生成不管这样的 AI 来说是一个比较好的补充和革新
这个想法的提出主要是在于对于数学的研究还是说可能它也会泛化到其他的领域
这个就像刚才讨论的一样,比如说在数学上我们有形容方法,在代码上我们有类似的程序验证的方法而在一般的场景下的话,我们有很多工具的调用,比如说我们可以在完成一些文本论述之后我们可以再根据这些文本当中提到的具体事实来调用比如说 De-research 这样的工具,来对每一个事实细节来进行检查
而这方面的话你可以根据这种检查结果来进行进一步的修正和反思以及最后进行多人迭代之后一个最终完全可靠的结果再反馈给人类用户所以我认为只要是能够使用外部工具来对模型的一种
生成的结果来进行一个纠正和修改的话都算是一种这样的 certified AI 的一种理念的贯彻所以说我觉得它其实是一个比较通的想法
确实下面我们可以讨论一些就是数学它对于其他领域还有对于 LM 其他研究的一些启发因为我们觉得数学是 LM 应用的一个研究的分支那如果反过来看数学还有强化学习的这个突破它会对 LM 本身起到什么样的作用数学能力的这个提升有没有带来比较明显的泛化的迹象
这个我觉得还是要看具体的分析很多的这样的结果其实都是在预训练厂家里面大家通过不断的实验数据配比数据筛选的这种 Rule based 筛选的机制的探索才慢慢的能够得到的一些比较早期的例子比如 GB3.5 它的这样推的能力有比较好的提升的话很多时候是因为它在
代码的数据的预料的配比上有一个更加高的比例但他以此方面就认为代码方面的数据是对于一般的推理能力来说会有一个比较好的放话能力的但是我个人会倾向于认为具体场景还是要具体分析很多时候同样是代码数据它包含是怎样的代码数据它是怎样的形式来进行提供的
它是单纯的代码 还说代码之中也有相应的解释的配套可能对于模型的学习来说都有不同的结果所以说我觉得这个其实是模型虽然也没有一个工程的问题
一般的来说这样的泛化的话往往它是建基于不同的领域之间它所使用的共同的推理的模式能够在不同的语料当中有一个文本互建的作用才可以出现的也就是说我们还是要通过语料的控制的方式来促成这样的泛化
那如果我们从这个学科研究的角度来看其实现在数学领域里面 AI 已经帮他取得了很好的成绩比如说已经获得了 IMO 的银牌然后也能比如说部分帮助顶级的数学家证明这个复杂的数学定理了
这种对于科学研究的突破是否能够借鉴到其他的学科有没有可能比如说在化学物理生物医疗等等这些领域它也可以借鉴这个数学领域的方式或者这种形式化的方式取得一些新的突破呢
就形式化本身而言的话现在很多的尝试也在把它推广到一些同样使用数理结构同样使用演绎推理方法来进行工作的理论比如说像理论物理这样的场景甚至还有对一些
在例里面也有对化学来进行一个形式化的尝试这些尝试都表明了这方面的形式化的这样一种领域不仅局限于像数学这样的纯粹思维领域还可以对其他的领域有一个知识整理和综合的作用但是对于一般的领域来说的话大家往往涉及到的问题在于实验也就是说我们是需要具体的实验而不是仅仅通过思维的推理来对
世界有一个更好的把握的这就涉及到另外一个问题但即使这样说的话数学方面的成果可能一定程度上也可以推广到其他的学科就比如说在数学里面我们是非常强的会依赖于先提出假设并且对假设来进行验证然后将验证成功的结果来加入到我们的知识体系当中来
而事实上对于所有的学科来说的话往往都会有这样一种自卑的模式一旦我们有这样的自主提出猜想自主验证猜想然后将猜想的正确的结果来进行知识积累的模型能够有一个比较好的方法上探索的话我相信它是可以很快的应用到其他的学科领域当中去的话
虽然可能在实验上需要在比如说机器和物理进行实际交互的方面有一个更进一步的补充其实华晶前面说到有一个点我觉得非常有意思就是在数学的证明的过程当中其实对代码能力的提升会有很大的提升因为尤其是涉及到一些复杂的定理证明的时候它所需要的好像是更像一个复杂的代码库
有的时候我们也看到有说法是好像解决一个复杂的数学问题就像是写一个 Linux 的系统一样我不知道对这个有没有更多的看法对于复杂的数学和复杂的代码户它两个之间的联系是的我觉得这两个方面其实是非常接近的比如说我们现在想要一个
在一个非常长的数学的论证的文章编写当中去修改一些具体的问题对一些具体的条件进行放松或者说引入一些新的抽象来对它进行一有来进行一个总和这些其实都已经非常接近于大家在代码软件工程里面进行实践的一些基本的策略
所以说我觉得大家在一旦这个问题上升到对于大规模的知识来进行一个完善和补充的话实际上无论是代码还是数学还是其他领域都是一个非常
有共通之处的研究场景了也就是说大家的主要困难已经不在于对于数学概念的理解对于代码的执行逻辑的理解了而是在于对于规模的理解对于大规模工程的理解而这种工程的话实际上是在领域之间是共通的那接下来 AI 和 LM 如果要进一步发展你感觉可能需要突破的一些瓶颈会是什么
事实上我们比如说如何提出一个更好的问题以及如何对一个已经有的生成的回答有一个比较好的 evaluation 的话仍然有一些非常现实具体的困难非常典型的例子就是比如说我们想要训练一个足够好的
IIM as judge 的模型有一个比较好的 reward model 怎么样让训练这样的模型能够让他比如说对一个复杂的问题他模型的解答能够完成的怎么样有一个比较好的判断的话实际上是一个比较困难的任务很多时候比如说模型确实像一个
代码库当中提出了一些补丁的设计它对一些内容进行的编辑而且它通过了所有的单元测试但是我们仍然需要对它确实是否能够满足我们的需求它无论是在代码风格上在使用规范上但在安全性上有一个更加好的理解的话我们往往不得不
最终诉诸于一种生成式的或者说一种用原模型来进行软性的判断也就是说我们没有继续使用 Rule-based 的方法来进行简单判断的场景下如何训练一个模型能够作为一个比较可靠的教师或者说一个观察员这方面的探索实际上我觉得是 2025 年大家一个核心的方面这方面比如说 DeepSync 之前也提出了一个 Generative 的
AI 的设计也希望在更加通用的场景上有一个训练一个比较好的 reward model 而在我们的这个任务当中比如说像 if bench 这样一个 benchmark 当中的话
它也是一方面需要通过编译来对语法层面来进行一个判断而另一方面的话也需要使用语言模型来对它是否正确的遵循自然语言指令来进行一个笼统的判断第二方面的话我们现在是直接使用了 Clausonnet 来进行一个简单的推理
但是事实上这个问题是比较复杂的我们比如说像人类的 code reviewer 也是面对一个具体的 commit 或者一个 pool request 的时候也是需要通过对已有的代码来进行一个比较审查来甚至对一些代码进行更加新颖的测试之后才能判断它的正确性也就是说甚至我们对于一个生成结果的审查本身
就是一个 agent 的任务了也就是说我们不仅需要一个生成式的 reward model 甚至需要一个 reward agent 我们需要
让模型自主的收集更多的信息利用这些信息来判断模型自己的生成是否是正确的以及可能也需要一些外部的工具要用来判断一些具体难以识别的细节就是说我们为了训练更好的 agent 我们需要训练另一个 agent 来对它进行一个判断
这样一个整个训练的 workflow 可能是一种非常复杂的场景我们该怎样提出一些具体的方法来解决这样一种复杂性的控制我觉得都是一些开的问题也就是说这个 reward 不再是一个提前固定好写好的一个 model 它是一个动态的 agent 这个 agent 自己还要去学习我怎么能更好的去判断怎么能更好的去给这个奖励信号
对是的因为比如说如果说我们是用固定的数据去练出一个一次性判断的一个 reward model 的话
它的效果的很大程度上是局限于我们的数据设计的也就是说一旦它模型自己的生成超出了我们所为训练 reward model 所提供的数据的话它就会到一种 out of the domain 的一种场景下模型的这样一种判断能力可能会剧烈的下降
而对于 agent 的设定下的话我们模型可以当它部属性领域出现的时候它可以主动的来获得更多的信息和知识来判断它所部属性的这样一些情况
这会对于这样一个 reward function 的设计来说的话使用更加 Lubon 更加不容易被 hack 的更加有准确性可靠性的方法以这种方法再来训练 RL 的话可能会对于当前的 RL 的话是一个比较好的补充和甚至彻底的提升的作用有意思
除了这个 reward agent 之外我们平时可能还会觉得或者说大家提到比较多的重要的这个模型需要提升的能力可能还包括这个 long context 或者说 long horizon reasoning 还有就是未来可能能实现 online learning
对于这两个,一个是 long context,一个是 online learning,不知道华健有没有什么看法?我认为 long context 的话已经基本上是一个工程问题了,也就是说我们要怎么样通过更好的数据工程收集到质量很好的无论是输入还是输出的长文本的推理的数据,还是说我们现在有一个比较好的多轮交互的这样一种过程。
无论是人类使用者的参与体现出人类对于上一个阶段的偏好以及模型需要在下一阶段进行相应的修正应该怎样来做还是说模型在自主的进行 agent 的执行过程中不断的和工具交互来进行长链条的执行和规划的过程这方面的数据的构造和筛选的话我觉得一定是会慢慢成熟的
而这方面的往往可能并不一定有那么多的概念性或者技术性的 inside 或者说 interest 可言很多时候往往是一个工程化的努力而至于 online earning 的话这方面很多工作其实是我个人会认为它是和 agent 的想法是非常接近的
现在 Agent 的话他主要的想法是不断的积累上下文通过新获得的信息将到上下文当中去能够辅助下一轮的决策和执行这个是现在主流的 Agent Workflow 的一个主要的设计但是 Online Learning 的想法在于我们希望能够
使用新的信息新的尝试对模型进行一个训练利用训练之后的结果再来对下一轮的或者说对同一轮的任务来进行一个更好的执行这方面的话我觉得我个人认为仍然是一个工程问题
它的主要瓶颈在于我们的 infra 支持怎么样能更好的平衡推理和训练方面的抑制性的需求也就是说我们需要在哪些环节上打断推理然后开始训练以及这样的推理和训练有异步的执行之后怎样来对模型的变化来进行一个控制
这方面种种问题其实都是对于训练的方法技术和对于推理和训练 infra 的整个系统来说是一个很大的挑战我觉得这方面的话
一定是会慢慢的取得进展的我觉得也是一个非常好的机会如果说在这方面的已经有比较好的厂家能够实现的话 Online Learning 应该是一个比较好而且足够 Promising 它在取用结果上可能取得意想不到的收获的一种样用方式
我们刚刚其实也讨论了几个技术的关键词华健觉得如果我们更 general 来说你认为下一个像 GBT4 级别的智能技术的跨越最可能会出现在什么方向这方面的跨越的话我个人其实和刚才讨论是一致的我觉得一旦我们能够
实现一个具有自主规划执行和反思能力的 agent 这种 agent 能够有上下文的能力有长链条的思考的能力有 online learning 的能力的话这样一套系统的一旦能够把它进行商业化的部署的话我觉得就已经足够是一个非常非常震撼的结果了就比如说大家在具体的用户的使用过程当中人类需要让模型能够不断的解决一些复杂的问题
我们能够感受到它的能力是在它探索过程中不断优化的话本身我觉得就是一个非常好的商业产品我觉得对于现在的产品来说已经获取一个差异性的打击的态势了华健对 AGI 的定义是什么在这个定义之下你觉得全球范围内可能第一家会实现 AGI 的公司会是哪家
第一家公司这个我觉得可能很难说因为现在实际上我们对每家公司的了解其实非常有限大家往往会有很多的压箱级的技术突然的爆出来但是我总体来说的话我认为有足够充分的模型训练经验有大规模的 infra 支持有足够稳定的大模型商业产品出现的公司我觉得往往会是下一个赢家也就是说不会是
新的医疗之外的赢家而是现在赢家之间进行内部绝对的结果也就是像北美的比如像 Google 像 OpenAI 像 Antopik 像国内 DeepSeek 都可能是这样一个结果的贡献者而
而这个又意味着现在已经我个人认为已经慢慢到了一个垄断和赢家通吃的结果就是说大家为了进行下一步的探索和增长需要在第一阶段上已经有比较好的努力而新入局的成员的话他需要补全太多太多的无论是在技术上在 infra 上在人才上还是在研究上
都有长期的积累之后才能够在这样一个技术密集其实同时也工程密集的环境下去的突破我觉得会是更加困难的结果所以说我个人认为 Big Name 仍然会成为 Big Name 这个很有道理要技术密集而且工程密集目前来看是现有的玩家会更有优势其实有些观点可能会觉得在
Pretrain 遇到一定的瓶颈然后 Oscillate 这个模型出来之后未来的半年到一年有可能会出现一个技术发展的真空期有些观点会觉得对未来一段时间有技术突破这件事情写的比较悲观不知道华健对这个未来可能半年到一年或者一两年的这个技术发展或者新的范式的出现会是什么态度呢
我觉得比如说从 GBT-3 到 GBT-3.5 和 GBT-4 的这样一个跨越在历史上一定会是一个比较罕见的事件也就是说我们不能一直指望这样的事件不断的涌现我们很多时候也是必须要接受我们有一些技术快速发展的阶段然后有一些技术慢慢积累的阶段然后再等待下一个快速突破的阶段
我认为现在我们已经慢慢到了一个有一定程度上的新东西的不断涌现但它不会有那么 exciting 的一个阶段了虽然说 OEE style 的模型能够给大家在推理上带来足够的震撼但是大家从个人的日常使用来说的话
可能并不一定对于已有的方法来说有一个彻底的革新或者代替作用比如说现在仍然大多数人仍然在密切的使用 4o 这样的老模型 4o 这样的老模型仍然是在推移时代之前的模型而推移时代之后的模型的话
核四欧往往是一个互补的态势而不仅仅是一个代替或者说代际跨越的态势这也反映了我们现在在处在一个简单状况之下至于下一阶段 Pretrain 的话我个人认为
其实这个问题我们需要更加仔细的探讨就是我们认为 pre-train 撞墙的是什么意思 pre-train 撞墙可能是因为我们只在 pre-train 阶段上进行 scaling 已经不足以支撑支撑下一步的大规模的跨越了但这可能并不意味着 pre-train 本身是不重要的比如说 agentworkflow 的能力的扩展对工具的调用的扩展的这种
过程当中去的话呃拿到的新的数据拿到的新的训练方法呃
难道新的数据组织方法可能还是要在 pre-train 当中进行一个融合的也就是说现在大家谈论 pre-train 不再那么重要是因为它不会带来完全新的技术革新了而并不意味着我们可以完全不做 pre-train 完全可以在一个完全 stable 的一个模型上继续工作就能够足以完成新的技术进展了我觉得这个可能
没有那么的乐观我们仍然需要在比较技术密集在资源密集的这样一种 pre-trained 的阶段不断地往里栽新的东西然后才能在下一阶段的话有一个比较稳定的技术突破这个话题
这个很同意,pre-training 其实仍然是非常重要的我们所说的这个 post-training 很多时候也是在激发 pre-training 的能力是的那如果从这个时间线上来看不知道华健怎么看这个 AGI 实现的这个 timeline 你会觉得它是比如说三年后到 27 年就能实现还是需要一个更长的时间我觉得我个人来说也不会有很好的判断但是
在 27 年之前的话应该会有一个在以上所讨论的这些方面都有一个比较好的进展但我们会不会发现一些新的问题发现他们有了具有这样的能力的模型仍然不能满足我们对于 AGI 的想象的话可能是另外一个问题了就意味着实际上我们对 AGI 的理解也是不断的看到新的东西我们才知道我们想要的是什么我们想要的是还是不是这个所以说呃
从一个稳定的 AGI 的时间表来对接下来进行预测的话我个人会觉得可能不是那么好说那从你个人的角度
接下来一段时间可能你的这个研究重点和研究兴趣会像一个什么样的方式去进化然后什么时候可能你会像前面所说的从这个数学这个分支领域转到一个多学科融合或者说更 general 的 IM 的这个方向上的研究
我个人会认为数学方面的话一直会是一个比较好的研究的案例也就是说我们可以不断的在这样一个
钉子上是新的锤子也就是说我们不断的把通用都可以借鉴的方法在这个领域上进行探索和实验把实验的结果总结成为新的方法然后供大家来进行推广所以说我个人的话接下来几年时间应该还是会在形式化数学上有一个更加深入的研究但是我在这方面的研究的话我也是希望这方面的方法不是非常 accurate 不是太
只能应用于这样一个具体的场景的而且希望它能够在不同的领域之间能够互相推广的但这些推广的话我个人会认为它是比如说我的工作和其他研究者的工作是一个共同相互借鉴的一个状况我个人的话还是会聚焦于形化数学在 AGI 的需求上能够更加满足我们的不同的使用的场景需求和能力的要求
各方面的态势呢华健你作为一个特别年轻的 researcher 在学术领域里面有没有你特别欣赏的 role model 很多 researcher 可能都觉得伊利亚是特别厉害的一个人不知道你心里有没有这样的类似这样的 role model 我的 role model 其实也是伊利亚本人就是我会认为
他能够敏锐的感觉到 Scalen Law 本身对于推广智能的边界来说是一个无论是在技术上可以实现在观念上是有非常充足的支撑还是在工程上已经达到了现在的这样一种
技术的阶段的话我觉得都是一个非常典型的榜样他能够非常敏锐的感受到我们这个时代已经在哪个方面有非常明确的机会是可以立刻进行工程化进行商业化我觉得这个是非常可贵的一件事情这样的人出现这样的事情出现也是一个很难判断的事情比如说我们现在已经慢慢从一些非常小的主要的想法比如说
pre training 可以做 scalding 而推广到一些非常具体的非常细小的工程上的一些 trick 和一些优化的贡献那这这种时候已经到了一个不再是那么个人英雄就可以发挥大的场景的阶段了那大家会成为一个无数平凡的
研究者最终会去成为一个大灯塔的这样一个态势那我觉得也是实事造英雄的一种态势最好情况下也可以尝试捕捉这样的时代脉骨但很多时候我个人会认为
大家只要做好自己的事情就是自己的这个 model 也就是说你觉得现在这个环境下其实很难再出现下一个伊利亚对对他很多时候不仅是他个人的原因你要考虑到比如说英伟达 Liebderling 的算法比如说像英伟达的芯片的算力的支持才能够让他这个梦想能够得以实现而这样的历史时机这样的重合的机会并不太多
好的,我们今天也聊了非常多关于形式化数学,还有关于 AGI 的话题,特别感谢华健跟我们做这样的分享,特别感谢华健今天的时间。谢谢,谢谢 Penny。