AI实话实说

今年 1 月 13 号，在 arxiv 出现了一篇论文（2601.07222），它证明了代数几何里的一个新定理，特别的是，这篇文章中的一个重要证明是由谷歌的 Gemini 模型生成的。文章作者之一，美国数学学会主席 Ravi Vakil 教授评价道，Gemini 的证明严格、正确，优雅，并不是已有文献的重组。教授表示，如果这个证明是他本人做出来的，他也会因此觉得自豪。类似的新闻我们最近听到得越来越多，就比如说，菲尔兹奖得主陶哲轩是 AI 数学的忠实用户和倡导者，自己也参与了用 AI 加上形式化验证来解决数学问题的工作。本期嘉宾 Alex Gu 就是陶哲轩在 AI 数学上的合作者之一，他所在的 8 人创业公司 Math, Inc 邀请了陶与他们合作，共同开发他们的 AI 形式化数学 Agent 高斯，并在 1月 16 号刚刚完成了对超椭圆曲线的黎曼猜想及其证明的形式化。本期 AI 实话实说，我们想和他深入聊聊：AI 做数学，到底能代替数学家吗？Alex 是 MIT PhD on leave，之前的主要研究兴趣是 AI for code 和 AI for math。大家耳熟能详的 LiveCodeBench 评测就是他的作品。相关术语：formal math - 形式化数学，在我们的语境下指用 lean 等计算机语言书写，利用编译器检验正确性的数学informal math - 非形式化数学，在我们的语境下指人类目前更常用的由人类审稿人来检验正确性的数学快速跳转：0:00:55 引入0:02:27 嘉宾经历介绍0:11:24 什么是形式化数学？0:15:40 为什么大家用 lean 来做形式化数学？0:17:00 形式化证明的例子0:20:43 在 AI 出现以前，大家做形式化数学的动机是？0:22:59 AI 出现以前形式化数学为什么没有大规模使用？0:26:15 形式化费马大定理，需要数学家还是 AI 人？0:28:39 为什么大家应该用 AI 做形式化数学，而不是 informal math？0:33:38 形式化和非形式化的数学对数学家有什么用？0:34:56 什么叫自动形式化？为什么它对于 AI 数学重要？0:40:00 到底哪些人在做 AI for formal math？0:42:37 不同的动机做 AI 数学，会产生什么样的不同行为？0:48:02 formal math 天生不适合人类数学家阅读吗？0:51:10 创业公司为什么要做 AI for math？0:53:58 AI math 创业公司有哪些？讲的是什么故事？1:01:59 AI 数学将来可以应用到软件的形式化验证？1:07:09 AI 数学还有哪些可能的应用场景？1:13:47 数学家群体怎么看待 AI 数学？为什么有些数学家不喜欢 AI 数学？1:18:16 “手工”数学家和拒绝工业化的手工铁锅匠人有区别吗？1:20:15 数学家未来会拥抱 AI 吗？1:22:12 Math Inc 如何团队合作？1:24:57 Math Inc 如何和数学家合作？1:26:40 陶哲轩如何和 Math Inc 合作1:29:34 为什么陶哲轩喜欢 AI 数学？1:33:18 你们会如何改变数学博士的就业市场？1:36:18 对于现在要开始学数学的人有什么建议？1:38:21 AI 不擅长提出新猜想和新问题吗？1:46:14 为什么加入创业公司，而不是大厂？嘉宾主页：minimario.github.io相关论文：Formal Mathematical Reasoning: A New Frontier in AI感谢 Peiyang Song 对本期节目的贡献。

大家熟悉的语言模型，比如 chatgpt ，采取的是自回归（autoregressive，AR）的生成方式，一句话从第一个字开始，一个字一个字地生成，一直到最后一个字。Diffusion 语言模型，扩散语言模型，则没有严格的顺序，也没有一次生成字数的限制，每一次可以在句子的各个位置生成任意数量的文字。所以它被叫做非自回归（non autoregressive）。扩散语言模型正在受到学术界和工业界的极大关注。本期 AI 实话实说，我们邀请了龚珊三，姚锦炜两位参与过 diffusion LM 研究和开发工作的同学，共同探讨扩散语言模型的过去、现在和将来。珊三是港大博士生，从 22 年起深耕 diffusion LM，发表了早期有代表性的 diffusion LM Diffuseq，提出了将自回归语言模型转化为 diffusion LM 的方法，还在 Apple 训练了 7B 用于代码生成的 DiffuCoder。锦炜是UIUC 硕士生，研究大模型的并行生成，同时是 SGLang diffusion LLM team的核心成员。他在和蚂蚁集团的团队合作，将蚂蚁近期发布的第二代 LLaDA，参数量达到 1000 亿的目前最大的 diffusion LM 整合进了 SGLang 框架，让开源社区得以高效部署这一模型。欢迎关注节目同名小红书 “AI实话实说” 加入群组，关注同名微信公众号获取文字内容。嘉宾小红书：Sansa (496274944)快速跳转精彩内容：00:01:00 扩散语言模型简介00:02:24 龚珊三自我介绍00:04:18 姚锦炜自我介绍00:07:49 哪些要素是 diffusion LM 必要的？00:10:56 diffusion LM 三要素00:12:39 包含自回归要素的 diffusion LM 是修正主义吗？00:15:21 以前名字千奇百怪，现在为啥都叫 diffusion LM 了？00:20:11 现在哪些学校或者公司做 diffusion LM？为什么？00:25:10 OpenAI 在做 diffusion LM 吗？00:26:41 为什么 OpenAI 很多人是 Diffusion 黑子？00:31:18 大家不愿意做 diffusion，是因为还没看到它的前景吗？00:33:42 蚂蚁集团为什么要做 diffusion LM？00:36:40 为什么大家从连续 diffusion LM 转向离散的？00:39:23 把 LM 做成非自回归，把图像生成自回归，这是没活硬整吗？00:44:21 从哲学上为什么说非自回归比自回归更有未来？00:46:44 锦炜为什么不在乎 diffusion LM 赢不赢？00:52:40 diffusion 对于语言数据天然有局限性吗？00:59:40 自回归为语言数据规定了  生成顺序，是不是违背了 the bitter lesson？01:09:43 陈立杰老师分析 diffusion 理论上限，有何意义？01:16:43 自回归语言模型的巨大成就是否限制了 diffusion LM 研究的空间？01:24:29 如何公平比较自回归 LM 和 diffusion LM？ 01:29:23 如何看待除了 diffusion 以外的并行生成方式？01:35:24 diffusion LM 目前适合用在哪里？01:45:23 diffusion LM 最大的问题是什么？01:48:46 ChatGPT 对你们的科研产生了什么影响？01:54:30 diffusion LM 如果未来没成功，你怎么办？01:59:17 AGI 会把我们都干掉吗？术语对照表：NAT - non-autoregressive translation - 非自回归翻译AR - autoregressive - 自回归Diffusion LM - diffusion language model - 扩散语言模型两位嘉宾的个人主页：summmeer.github.iokivi-yao.github.io讨论到的论文和资料：珊三对于 diffusion LM 的总结锦炜参与的 SGLang Diffusion LM 引擎非自回归翻译从生成顺序看 diffusion 模型的局限性diffusion 的学习效率比自回归更高diffusion LM 的理论上限分析parallel generation calls are not isolated-- they have sharing pattern to acceleratesequential prefill can be parallelizedmultiverse--parallel generations for better test time scalingdLLMm for drafting:  tidarlm.github.io and z-lab.ai/projects/dflash/dLLM caching from NVIDIA:  github.com/NVlabs/Fast-dLLM

这是 AI 实话实说的第一期节目，我们请到了赵晨阳。晨阳本科毕业于清华大学，目前是 UCLA PhD on leave。他从 2024 年 7 月份开始参与主流 LLM 推理引擎 SGLang 的开发，是 SGLang 的核心贡献者和 RL lead，现在也和 SGLang 的许多开发者一起在 RadixArk AI 创业，继续做开源 AI Infra，开发开源 RL 框架 Miles。嘉宾主页：zhaochenyang20.github.io/Chayenne嘉宾小红书：我，吉他，猫，LLM。欢迎关注节目同名小红书 AI 实话实说 加入群组参与互动，关注同名微信公众号获取文字内容。跳转精彩内容00:01:34 嘉宾自我介绍00:02:20 为什么从做算法变成做 Infra？00:10:00 做 infra 是为了最大化 impact？00:12:30 存在 bug 的 infra 能做出可靠的算法研究吗？00:14:45 某 Frontier Lab 的 MOE 模型训不出来背后的原因竟然是？00:18:44 为什么要做 RL 的训推一致？00:21:35 假设 infra 是完美的，算法研究会发生什么？00:27:23 RL 的下一步是 Serverless RL？RadixArk 要做 OpenTinker？00:33:08 为什么 OpenRLHF 的设计理念很先进？00:35:44 SGLang 的产品经理要做什么？00:39:42 如何平衡来自不同贡献者的开源贡献？00:43:56 vibe coding 对开源社区的影响？你如何用 vibe coding？00:49:11 如何避免垃圾代码毁掉开源项目？00:52:31 开源项目和企业的关系？00:53:47 SGLang 贡献者为什么要加入 RadixArk AI？00:56:26 为什么你觉得 AI 学术圈完蛋了？00:59:51 RadixArk 做什么？怎么赚钱？01:02:02 RadxArk 如何平衡开源和商业？01:08:13 如何加入 RadixArk？01:11:40 Infra Engineer 会被 AI 代替吗？01:14:39 RadixArk 的 RL 框架 Miles 好在哪？01:20:03 谈谈博士生 on leave01:28:28 谈谈 AGI01:30:18 为什么你用 gemini 以及看好谷歌？01:37:31 AI 会让我们失业吗？怎么办？本期提到的论文：Zhao et al., SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning, COLM 2024Viswanathan et al., Prompt2Model: Generating Deployable Models from Natural Language Instructions, EMNLP Demo 2023.本期提到的开源项目：sgl-project/sglangTHUDM/slimeradixark/milesOpenRLHF/OpenRLHFNovaSky-AI/SkyRLInternLM/XTunerByteDance-Seed/VeOmni本期提到的人物：slime 的代码神：github.com/zhuzilinSGLang 的代码神：lmzheng.netkivi-yao.github.io