传说巴别塔倒塌之后，人类开始说不同的语言，从此再也无法轻易理解彼此。 千年后，我们造出了精通所有语言的 AI，她能写诗、编程、聊天、抚慰陌生人的心灵。但一个诡异的问题随之出现——当机器学会了语言，是否意味着她理解了我们的世界呢？ LLM出生于文字，她读过无数次的“猫”，却没有摸过任何一只猫; 她知道什么叫“前后左右”，却从未真正站在房间内转过身；她可以描述悲伤，却从未真正体验过失去。 这正是Grounding（符号接地）所追问的问题：语言的意义，究竟来自语言内部，还是必须最终落回到真实世界？ 本期《AI实话实说》，我们和 Freda Shi 教授从语言学聊到认知科学，从维特根斯坦聊到AI写诗，Freda本人也像这个问题的映射：做着精确的符号研究，却深爱历史诗歌和那些无法完全形式化的东西。 也许通向 AGI 的最后那一步，不是让AI再读万亿 token，而是让语言——终于落到地上。 欢迎关注同名小红书“AI实话实说”，加入群组和嘉宾、主持人互动！ 嘉宾介绍 Freda Shi（石昊悦），滑铁卢大学计算机科学教授，Vector Institute Faculty Member，并担任 Canada CIFAR AI Chair。研究方向横跨自然语言处理、计算语言学、Grounding、多模态模型、模型认知与程序语言。 她于 2024 年加入滑铁卢大学，此前在 Toyota Technological Institute at Chicago 获得计算机科学博士学位，她本科就读于北京大学 EECS，后进入自然语言处理与计算语言学研究领域，曾在 Google DeepMind、Meta 等机构从事研究。 Freda 是一个很难用单一学科装下的研究者。她做 NLP，也读语言学；写代码，也爱历史、文学和维特根斯坦。她尤其关注那些主流 benchmark 不容易照到的角落。 相关术语 Grounding / 符号接地 把语言中的符号与意义、感知或外部世界建立联系。模型是否真正尊重语言背后的 semantics，而不只是统计上生成了合理的文本。 Symbol Grounding Problem / 符号接地问题 认知科学和人工智能中的经典问题：如果一个系统中的符号只是通过其他符号来定义，那么这些符号最终如何获得真实意义？这一问题通常被追溯至 Stevan Harnad 对符号系统意义来源的讨论。 Stochastic Parrot / 随机鹦鹉 Emily Bender 等人提出的著名比喻：语言模型可能非常擅长复现语言形式，却并不真正理解这些语言对应的意义。 Inductive Bias / 归纳偏置 学习系统在看到数据之前就具有的结构性假设。例如卷积神经网络偏向利用局部空间结构，而循环神经网络偏向顺序处理信息。归纳偏置可以提高样本效率，但也可能限制模型能够学习到的模式。 Bitter Lesson Rich Sutton 提出的机器学习观点：长期来看，依赖大规模计算和通用学习机制的方法，往往会超过高度依赖人工设计知识和领域先验的方法。它常被用于解释深度学习和大规模模型的发展路径。 Emergence / 涌现 指模型在规模扩大后表现出的、在较小模型中不明显的新能力。研究界对于部分“涌现”现象是否真正是突然发生，还是由评价指标离散化造成的表象，仍存在持续讨论。 Mechanistic Interpretability 试图从模型内部结构出发，解释神经网络如何实现某种计算或行为。研究对象通常包括神经元、注意力头、特征表示、计算回路以及不同层之间的信息流。 Sparse Autoencoder（SAE）/ 稀疏自编码器 一种用于分析神经网络内部表示的方法，通过将密集的 activation 分解成较稀疏的特征，希望获得更容易分析和命名的内部表示。近年来被广泛应用于大语言模型可解释性研究。 Actionable Interpretability 一种更务实的可解释性观点：解释模型不是为了“看起来解释了”，而是要能帮助 improve the model、better understand the model，或者更安全地与模型互动。 快速跳转 02:58 Freda 还是昊悦？一个英文名字如何变成另一种语言里的身份 05:12 兴趣与天赋并不匹配：爱文学和历史，为什么最后还是选择了计算机？ 14:37 从维特根斯坦到 NLP：为什么语言最终成为她研究世界的入口？ 20:28 当 AI 让所有人说同一种“语言”，人类会不会失去认知的多样性？ 29:02 什么是 Grounding？为什么一个会说话的模型，不等于一个理解意义的模型？ 36:05 Grounding 是手段还是目的？如果机器人不知道自己在做什么，我们敢让它进入现实世界吗？ 45:50 从 Coding 到 Grounding：为什么代码验证与外部世界反馈必须同时存在？ 56:58 Scaling 能解决 Grounding 吗？能力是突然涌现，还是一点点长出来的？ 1:00:02 有意思，还是有意义？一个研究者到底该追求什么？ 1:07:27 能不能像研究人脑一样研究 LLM？Behavioral Science 与 Mechanistic Interpretability 的边界 1:17:58 如何带学生：研究品味、自由，以及“有意思”和“有意义”的双向选择 1:20:10 AI 会写诗吗？艺术究竟发生在创作者手里，还是发生在读者心里？ 1:29:34 AI Slop、论文评价体系与 Reward Hacking：学术发表体系还能撑多久？ 1:36:02 未来三年的一个判断：论文发表体系会崩，具身智能会继续向前

2010年那会儿，付杰在人人网上第一次听说“深度学习”。第二年他投了一篇用深度学习做图像匹配的论文，被拒了，审稿人说这东西“太经验主义”。他没纠结，转头就去做 kernel machine。两年后，ImageNet 比赛里，AlexNet 杀出来，深度学习的这十年，就这么开了头。 到了2020年，朋友拉他一起搞语言模型，他想了很久，还是决定继续留在 Mila 做博后。同一年，GPT3 发布，大语言模型从此一路狂飙。 说起来，两次都站在风口边上，两次都没进去。付杰后来也承认，心里一直有个念头，就是想证明“我比大家更早看到”，只是当时没有懂得如何利用好工业界scaling的优势。所以现在，他戒糖、断食，想方设法“延缓衰老”，想把错过的时间，在下一个路口抢回来。他觉得目前对于safe AI来说，梯度下降最陡的一个方向是如何让“验证”变得便宜且可靠。 这次聊天里，他特别想聊清楚一个事：measure 和 verify，看着差不多，其实是两码事。他也慢慢放下了“什么东西都得形式化”的执念。至于机制可解释性到底能不能兑现当初那些承诺，他还在摸索。说到底，这就是一个AI研究者跟自己较劲、跟时间赛跑的十五年。 欢迎关注同名小红书“AI实话实说”，加入群组和嘉宾、主持人互动！ 相关术语 Verification：验证。判断一个系统的结果是否真正满足人类的目标、约束和安全要求，而不只是某个分数是否更高。 Verification Cost：验证成本。确认结果正确、安全和符合真实意图所需要的时间、算力、实验与人力成本。 Formal Verification：形式化验证。把要求写成严格的形式语言，再通过程序或证明系统验证软件、算法或行为是否满足这些要求。 Autoformalization：自动形式化。将自然语言中的问题、规则和需求自动转换成 Lean、Dafny 等形式语言中的严格命题。 Verifier：验证器。检查 AI 的答案、计划或行为是否满足规范的系统。在理想情况下，它需要与被监督的 AI 同样强，甚至更强。 Mechanistic Interpretability：机制可解释性。研究模型内部的神经元、回路与状态如何产生具体能力和行为。 Swiss Cheese Model：瑞士奶酪模型。任何单一安全机制都有漏洞，因此需要多层防御，让不同层的漏洞尽量不在同一位置重合。 Recursive Self-improvement：递归式自我改进。AI 参与改进自身或下一代 AI 的过程。其关键瓶颈之一，是能否获得持续、可靠且低成本的验证信号。 快速跳转 02:02 IQuest 付杰登场：轻断食、延缓衰老，以及为什么每天都在怀疑自己 04:21 前沿研究为什么越来越难获得反馈？ Verification 的稀缺 10:51 Verifier、World Model 与 Safety Specification 如何共同构成安全防线？ 17:21 “AI also means 爱”：如果无法控制更强的 AI，人类能否让它学会爱与共情？ 21:42 Verification 一定比 Generation 容易吗？计算复杂度与不可约性 28:40 穿越四次 AI 浪潮：为什么他一次次提前看到，又一次次错过？ 35:20 从“证明我看得早”到 “Scaling What Works”：对过去研究路径的反思 40:05 降低 Verification Cost：为什么安全既是防御工具，也可能加速 AI 进化？ 46:03 从机制可解释性到形式化验证：如何让黑盒模型变得更透明、更可靠？ 1:06:58 形式化验证与自动形式化：如何把自然语言问题放进一个每一步都可检查的形式世界？ 1:18:35 从软件到 Agent，再到 AI for Science：哪些行为能够被验证，如何防止模型钻规则的漏洞？ 1:30:35 理想的验证系统、AI 取代焦虑与最后的结论：Verification is the GOAT

江湖传言，南京大学蒋炎岩老师，要在人生巅峰“金盆洗手”。 蒋老师江湖诨号“绿导师”，是南大操作系统课的掌门人，软工圈的奇人，知乎、小红书和B站常驻的“锐评宗师”。讲课有名、出题有名、骂人更有名。之前一篇《给天命人的劝退信》，劝得无数准备读博的“天命人”站在山门前开始怀疑人生。 这一次，绿导师来到《AI 实话实说》，不是讲课，不是说论文，而是预言一整个 AI 时代的江湖浩劫。 在他眼里，AI 带来的不只是“程序员失业”或“论文被替代”，而是整个人类智力活动被推上审判台。翻译、编程、科研、大学和导师制度，都将被重新改写。但绿导师谈“末日”的态度，不是悲凉，而是看破红尘的快意。那也许不是末日，而是一种“恩赐的解脱”：博士生不必再痛苦挣扎，老师也不必再被论文、经费和职称反复消耗。 他究竟是金盆洗手、退出软工江湖的“风清扬”，还是不忘初心、对抗科研体制的“真大圣”？ 这一期，绿导师开坛讲法。 欢迎关注节目同名小红书“AI 实话实说”加入群组参与互动。 本节目音频版在小宇宙、Apple Podcast 同步更新，视频版在 bilibili 不定期更新。 嘉宾介绍： 蒋炎岩，南京大学博士生导师，曾在 SOSP、ASE、EuroSys、ICSE 等操作系统和软件工程的顶会斩获 best paper。 他在南大开发的操作系统课程广受好评，在 bilibili 观看量超过五百万，并在学生投票中被评为“我最喜爱的老师”。 他在网上行走的名号是 “绿导师原谅你了”。他讲操作系统，讲软件工程，也讲他对于考研、论文、经费、职称的锐评，出言如剑，专拆学术江湖里的 reward hacking。 相关术语： 绿导师：蒋炎岩老师的网络称号。既是教学江湖里的招牌，也是他直言不讳、锋芒外露的互联网人格。 Test-time Scaling：测试时扩展。指模型在推理阶段通过更多时间、更多计算、更多搜索和更长任务执行，获得更强能力。 Small Explanation Hypothesis：许多复杂研究问题背后，可能都有一段相对简短的解释；如果能生成、枚举、筛选和验证这些解释，就可能让 AI 自动推进科研。 Auto Research：自动化科研。让 AI 不只是执行人类提出的问题，而是自己生成问题、验证问题、产生新的知识。 Reward Hacking：奖励黑客。人或 AI 钻评价体系的漏洞，追求指标、论文、分数、奖项，而不是追求真正有价值的能力和贡献。 独立 PI：脱离原有团队组织结构，以相对独立的方式带学生、上课和做研究，减少大型项目、申请书、验收等组织性 overhead。 古法编程：不依赖 AI、不依赖大模型，靠手册、肌肉记忆和命令行细节完成编程任务的旧式方式。 本期节目参考的绿导师文集： 《读博那些事儿》，知乎专栏，2019 年 9 月。 《给各位天命人的劝退信》，个人主页，2024 年 9 月。 《副教授实名举报计算机专业学生编程水平不如小学生》，知乎专栏，2025 年 5 月。 《绿导师是怎样戴帽的：学术跃进运动的来龙去脉》，知乎专栏，2025 年 12 月。 《一个软工人的辩白》，China Sys 讲座（b站视频），2025 年 12 月。 《Agentic AI 时代的操作系统课：绪论》，b 站课程视频，2026 年 3 月。 《我决定要在人生巅峰退休了》，小红书 “绿导师戴帽子了”，2026 年 3 月 21 日。 登三篇：《大学今天💊了吗》《老登牛逼》《为什么要攻击老登》，小红书 “绿导师戴帽子了”，2026 年 6 月。 00:03:35 绿导师要退休了吗？ 00:04:08 AI 末劫将至，大学教育、科研论文和导师制度是否都成徒劳？ 00:05:55 AI 末日给学生和老师带来的是“一种解脱”？ 00:07:59 test-time scaling 和 small explanation hypothesis，通向 AGI 的秘径？ 00:14:03 绿导师退出了软工圈，软工圈也退出了软工 00:16:06 论文、经费、职称，如何把老师和学生都逼成 reward hacker 00:23:32 面对旧时代的评价体系，绿导师选择掀桌子不玩了 00:29:23 学生选拔崩坏：为什么考研复试学生的编程能力，可能不如小学生？ 00:51:54 《劝退信》之后，绿导师想要什么样的学生？ 01:11:50 绿导师不再教《操作系统》，下一门课是什么？ 01:31:36 《老登三篇》和审稿江湖：学术会议里到底有多少论文是在包装 contribution？ 01:46:16 一路在“退”：退休、退圈、退所、退委员会、退考研出题，是失望，还是以退为进？ 01:53:19 未来三到五年最值得关注的事：真正的 auto research 能不能发生？

本期嘉宾忙秋阳在过去的一年经历了三个大的转变：从相信人类智慧无法战胜的算法竞赛世界级选手，到坦然接受 AI 在算法上超越了他；从利用算法研究计算的自动化，到利用 AI 研究算法研究的自动化；从小而美的小组科研，到大成本、大规模的大团队作战。 他行为的变化背后是认知的转变：过去，人类自己提出问题，也自己解决问题，自己设计算法，处理数据，设计实验。而现在，AI 面对人类提出的问题，正在自动化解决问题这件事本身。 秋阳带领团队发表的 FrontierCS，就是一个测试 AI 面对开放性问题解决能力的数据集，Frontier 的意思是边界，他想要探索 AI 代替人类科研的边界在哪里，随着 AI 和人类分工边界的移动，人类在科研探索中还要扮演什么角色？ 本期 AI 实话实说，我们和秋阳聊了算法竞赛、Frontier CS、开放式科研、合成数据、AI for Science，以及一个更大的问题：如果 AI 真的可以做科研，那么博士生、PI、论文、实验室这些概念还是否存在？整个学术评价体系会变成什么样？ 欢迎关注节目同名小红书“AI 实话实说”加入群组参与互动。 嘉宾介绍： 忙秋阳是 UC Berkeley PhD 和 Sky Computing Lab 的成员。目前主要研究 long-horizon agent、auto research、AI benchmark 和开放式科研任务。此前研究方向包括软件工程、数据库系统、复杂系统漏洞检测和查询优化。他曾参加信息学竞赛和 ICPC，并进入 ICPC 世界总决赛。近期代表工作包括 Frontier CS 和 FrontierSmith，关注 AI 如何解决没有标准答案、但可以被验证和优化的开放式计算机科学问题。 相关术语： FOMO：Fear Of Missing Out 错失性恐惧心理 Long-horizon Agent：长程 Agent，指需要跨越多个步骤、多个 context window，甚至长时间运行才能完成任务的 AI 系统。 Auto Research：自动化科研，让 AI 不只是回答已有问题，而是参与提出方案、优化实验、探索开放式问题。 FrontierCS：一个面向计算机科学开放式问题的 benchmark，关注 AI 是否能在没有标准答案的问题上超过人类 reference。 FrontierSmith：围绕 Frontier CS 进一步生成开放式任务和训练数据的方法，试图让 AI 合成可用于训练和评估的高质量问题。 Open-ended Problem：开放式问题，没有唯一标准答案，但可以通过某种 verifier 或评分函数判断结果好坏。 Reward Hacking：奖励作弊。AI 不是解决真实问题，而是钻评价系统或测试环境的漏洞，拿到高分。 Test-time Scaling：测试时扩展。指给 AI 更多时间、更多 token、更多尝试次数，看它能否通过长期搜索和迭代获得更好结果。 Synthetic Data：合成数据。由 AI 或程序生成的数据，可用于预训练、后训练、评估或构造任务。 快速跳转： 00:05:16 嘉宾竞赛经历 00:06:18 算法竞赛选手的尊严受到了 AI 的巨大冲击 00:10:31 参加算法竞赛的高中生已经有潜力发表 EMNLP 和 SIGMOD best paper 00:12:01 为什么研究方向从数据库/软件工程转向 AI？ 00:15:20 AI 自动化科研之后，人的位置在哪？ 00:19:14 人和 AI 如何分工？ 00:24:15 FrontierCS 看的是什么能力？ 00:28:16 FrontierCS 题目举例，AI 超过人类了吗？ 00:36:22 不同时候人们对 benchmark 的期待 00:42:16 AI + X 在解决不存在的问题，优化不存在的成本? 00:49:20 工业界做 benchmark 的情况下，学术界做的还有意义吗？ 00:55:47 你说 Terminal Bench 是学术界的优秀 benchmark，可怎么它的作者都跑去 anthropic 了？ 00:57:19 做 benchmark 是被人鄙视的，不是做真科学真研究，我们做方法的人才是坠牛的？ 01:01:48 合成数据竟然比人类标注质量还要高？ 01:08:09 所有数据都是 AI 生成的，AI 还能继续进步吗？ 01:12:00 学术界做合成数据有意义吗？工业界不会做得更好吗？ 01:18:07 FrontierCS 里的题目有现实意义吗？ 01:26:18 如何避免 reward hacking？存在一般的办法吗？ 01:29:25 FrontierCS 花了多少钱？谁来出？ 01:32:10 大团队是做 AI 科研的必要条件吗？ 01:34:50 大团队提供的是更多的资源，是什么资源？ 01:35:46 大团队科研如何判断贡献大小？ 01:42:00 AI 来了，教授还要招博士生吗？ 01:43:07 SkyLab 为什么成功？ 01:46:43 社区贡献，而非论文发表，正在成为 AI 博士毕业的新标准？

硅谷 AI 的节奏飞旋，一月如一年，时隔四个月，我们再度访谈 ActAVA AI 的联合创始人姚巍然。只为问出一个核心问题：在医疗健康领域，AI Agent 是否可以替真人干活？ Claude Code、Codex 这类工具所带来的深度变革已经改写了软件工程这个行业。但是一旦把AI外推到其他的行业中，质疑的声音总是接踵而至——AI是否可以在具体和复杂的沟通与规定场景下替代人类。 本期嘉宾巍然的答案是：不行！至少现在还不能...... 巍然团队最近发布了一个面向医疗工作流的 Agent Benchmark：χ-Bench。它测试的是 AI Agent 能不能自动化端到端、长链条、政策密集的医疗流程，比如 prior authorization、utilization management 和 care management。这个 benchmark 虽然只是针对医疗领域，但是它对于其他行业应用 Agent 无疑有着强烈的借鉴作用。 本期 AI 实话实说，我们和巍然聊了 χ-Bench 为什么重要，医疗 Agent 为什么比 coding agent 更难，benchmark 和融资叙事之间的关系，AI 医疗创业公司的护城河，以及一个更大的问题：未来企业到底会继续依赖 OpenAI、Anthropic 这样的闭源模型，还是会走向行业专属、客户自有、可本地部署的模型。 欢迎关注节目同名小红书 AI 实话实说 加入群组参与互动。 嘉宾介绍： 姚巍然，AVA.AI联合创始人，主要关注 healthcare workflow automation、AI agent platform 和 domain-specific model。他所在团队正在开发企业级 Agent 平台，并探索医疗场景中的仿Agent解决方案、Benchmark 和医疗专用大模型。 相关术语： χ-Bench / Chi Bench：面向医疗工作流的 AI Agent Benchmark，测试 Agent 是否能完成端到端、长时间、多政策约束的 healthcare workflow。 Policy-rich workflow：政策密集型流程。指每一步操作都需要受到保险政策、医疗规定、公司 SOP 或内部文档支持。 Long-horizon task：长链条任务。任务不是一步完成，而是需要多轮读取、判断、调用工具、生成文件、和人对话，并在过程中不断更新状态。 Human in the loop：AI 可以完成大部分草稿、检索、整理工作，但最终仍需要真人 review 和 sign off。 LLM-as-a-judge：用大语言模型作为评估器，判断 Agent 的输出是否符合标准。 快速跳转： 00:01:46 开场：四个月后，团队承诺的 Agent 平台做出来了吗？ 00:03:49 什么是 χ-Bench？为什么医疗工作流需要新的 Agent Benchmark？ 00:07:39 现在 AI Agent 能不能端到端自动化医疗 workflow？答案是：不能。 00:25:56 现在 Agent 做不到 end-to-end，对创业公司为什么反而是好消息？ 00:27:14 发布 benchmark 是否也是为下一轮融资铺路？ 00:39:43 Healthcare Agent 公司相对于 foundation model 的护城河是什么？ 00:45:53 小公司员工既要做产品又要服务客户，会不会变成血汗工厂？ 00:51:46 定制化开源模型能不能超过通用闭源模型？ 00:53:30 当前 Agent 的主要 failure mode：rush to submit、policy reasoning、conversation mode 切换 01:04:04 怎么评估 Agent 和病人的对话？如何模拟病人的不信任？ 01:11:11 为什么美国医疗系统是一个 administrative nightmare？ 01:17:00 如果 Anthropic 或 OpenAI 来刷榜，会不会抢走市场？ 01:23:56 Agent 出错了，谁承担责任？为什么产品里必须 human in the loop？ 01:20:34 医院是否会走向自有模型？为什么企业不一定愿意把数据交给 OpenAI？

医疗是个大问题。在美国，这个问题集中体现在高昂的医疗支出和不公平的保险理赔。医疗产业中三大关键角色：病人、医院和保险公司之间需要大量繁琐、重复、敏感的行政工作。 本期嘉宾姚巍然，是 Activa AI 的 co-founder。博士期间，他研究 causal AI；在 Salesforce AI Research，他很早参与了 AI Agent 和deep research agent 等方向；现在，他把这些经验带进了医疗行业，试图做一件很难但很现实的事：把医疗系统里的行政工作，用 AI Agent 自动化。 这期节目里，我们从他的个人经历聊到 Salesforce 为什么没有成为 Agent 时代的先锋，从 Cursor 为什么好用聊到“Cursor for Healthcare”到底是什么意思，从美国医疗系统里的 payer/provider 结构聊到保险拒赔、AI 公正性、责任归属和病人权益。 更大的问题是：如果 AI Agent 真的能进入医疗系统，它到底是在帮医生、帮保险公司，还是帮病人？这究竟只是生产力工具，还是一种新的范式？ 欢迎关注节目同名小红书 AI 实话实说 加入群组参与互动。 嘉宾介绍： 姚巍然，Activa AI 联合创始人，主要关注 healthcare workflow automation、AI agent platform 和 domain-specific model。他所在团队正在开发企业级 Agent 平台，并探索医疗场景中的仿Agent解决方案、Benchmark 和医疗专用大模型。 相关术语： Forward Deployed Engineer / FDE：派到客户现场或深度参与客户项目的工程师，负责理解客户需求、集成系统、部署产品、解决实际问题。 HIPAA Compliance：美国医疗数据合规要求，涉及病人健康信息、日志、权限、基础设施、审计、员工培训等一系列规范。 PHI：Patient Health Information，病人健康信息，包括姓名、症状、社保号、病历等敏感信息。 Open-weight Model Post-training：在开源权重模型基础上继续训练或微调，让模型更适合特定任务或行业。 快速跳转 00:00:54 开场与嘉宾介绍：从 Salesforce AI Research 到医疗 AI Agent 创业 00:03:33 从 causal AI 到 AI Agent：博士、Salesforce、创业三阶段的研究变化 00:09:53 Agent 架构的演化：从早期混乱设计，到 workflow 和 agent loop 00:13:00 2025 年的新风向：RL、diffusion language model 和 deep research agent 00:18:11 Salesforce 为什么很早做 Agent，却没有成为行业先锋？ 00:22:05 为什么离开 Salesforce 创业？为什么最终选择 healthcare enterprise？ 00:26:17 “Cursor for Healthcare” 到底是什么意思？ 00:29:10 美国医疗系统入门：payer、provider、patient，以及为什么行政流程最适合自动化 00:35:52 如何看待美国医保理赔难？ 00:42:21 Actava AI：面向医疗企业 long-running workflow 的 Agent 平台 00:58:13 Healthcare 领域的特殊挑战：HIPAA 合规、客户教育、数据 01:14:16 Actava 在模型训练上的努力 01:23:00 Actava AI 研究：从 benchmark 到模型到 agent 01:28:13 Healthcare Agent 会代替人类吗？ 01:30:28 Healthcare AI 会让医保理赔变得公平吗？ 01:38:16 展望三年后 01:43:49 学术界和工业界的抉择 01:46:25 对新 AI 学生的建议，在 AI 比你聪明的时候你该做什么？ 01:52:02 展望 AGI 的世界

今年 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.io kivi-yao.github.io 讨论到的论文和资料： 珊三对于 diffusion LM 的总结 锦炜参与的 SGLang Diffusion LM 引擎 非自回归翻译 从生成顺序看 diffusion 模型的局限性 diffusion 的学习效率比自回归更高 diffusion LM 的理论上限分析 parallel generation calls are not isolated-- they have sharing pattern to accelerate sequential prefill can be parallelized multiverse--parallel generations for better test time scaling dLLMm 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 leave 01:28:28 谈谈 AGI 01:30:18 为什么你用 gemini 以及看好谷歌？ 01:37:31 AI 会让我们失业吗？怎么办？ 本期提到的论文： Zhao et al., SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning, COLM 2024 Viswanathan et al., Prompt2Model: Generating Deployable Models from Natural Language Instructions, EMNLP Demo 2023. 本期提到的开源项目： sgl-project/sglang THUDM/slime radixark/miles OpenRLHF/OpenRLHF NovaSky-AI/SkyRL InternLM/XTuner ByteDance-Seed/VeOmni 本期提到的人物： slime 的代码神：github.com/zhuzilin SGLang 的代码神：lmzheng.net kivi-yao.github.io