5 Papers That Show Where AI Research Is Heading Right Now

频道: Y Combinator
视频: https://www.youtube.com/watch?v=3rWSvrFahIY
原文语言: en
统计: 共 37 轮

[0:08]

Thank you guys so much for coming. This one will have much a much more applied bent based on the feedback. We have a bunch of really cool people that I'll introduce in a second, but we're covering AI for uh biology by my favorite one of my favorite co- researchers, Yas Beg. We have Luke um out of Tatsu's lab talking about selfplay, Alpha Zero style selfplay for LLMs. Super excited about that. Arnob will be uh presenting he's a researcher at Giga on stream rag uh super different application you know thinking about uh real realtime voice uh agents uh Robert George working on lean for science super exciting and then the AI token maxer himself Luke Worthwine cool so I want to introduce some like call for presentations you know maybe inspire some of my interest and maybe inspire some some of you guys to jump up and and ask for a presentation on this stuff. I think memory has been like the hot topic for at least the last year and a half. There's been so many papers from mem zero to recursive language models cartridges out of uh our lab hnet, you know, dynamic chunking stuff. There's so many different ideas and so I'm definitely interested in that area. If you guys want to present on that, I did this Nome Brown podcast I think a couple weeks ago launched and like he's still of the view that this human generated subspace H is still if we train on that we can test time compute our way out of it and recursive self-improve out of it all the way to get to this F minus H. And I just like really struggle with this and I really really don't see how it's probable. Not that it won't it's not possible, but it's just not probable that we'll sample all of that. So, I'm really interested in that and that's definitely in Luke's. We were talking about that a bunch and I think that basically the left side is alpha go, the right side is alpha zero. And I think that alpha zero unbiased by um humans meandering is uh the way we'll get to much more intelligent systems, maybe even dare say agi. And the right way to say this um would be um I want to be very careful. If the full solution space f is f, training on known human solutions will limit you to some typical set h despite any feasible amount of test time compute or recursive self um improvement. You won't feasibly sample f minus h. Um and especially all of it. If if it's infinite recursive self improvement, infinite test compute maybe, but we don't have infinite. So life's a pom dp and this is a we're finite horizon mdp.

非常感谢大家来到现场。根据上次的反馈，这一场会更偏应用一些。我们请到了一群非常厉害的人，待会儿我会一一介绍。我们要讲的主题包括 AI for biology（AI 在生物学的应用），由我最喜欢的合作研究者之一 Yas Beg 来讲。还有来自 Tatsu 实验室的 Luke，讲 self-play，也就是 AlphaZero 式的 self-play 应用在 LLM 上，对这个我超级期待。Arnob 会来分享，他是 Giga 的研究员，讲 stream RAG，一个非常不一样的应用方向，思路是实时语音 agent。Robert George 在做 Lean for science（把 Lean 用在科学上），也超级令人兴奋。最后是「AI token maxer 本人」Luke Worthwine。好，所以我想发一个「征集分享」的号召，希望既能激发我自己的兴趣，也许也能激发你们当中一些人站起来、主动要求做一次这方面的分享。我觉得 memory（记忆）至少在过去一年半里一直是个热门话题。出了好多论文，从 mem zero 到 recursive language models（递归语言模型），到我们实验室出的 cartridges，再到 H-Net、dynamic chunking（动态分块）那些东西。有这么多不同的想法，所以我对这个领域绝对很感兴趣。如果你们想分享这个，欢迎。我前阵子录了那期 Noam Brown 的播客，我想是几周前上线的，他到现在还持有这样一个观点：这个由人类生成的子空间 H，只要我们在它上面训练，就能靠 test-time compute（测试时计算）一路算出去、靠 recursive self-improvement（递归自我改进）一路改出去，最终触达 F 减 H 的那部分。我真的对这个观点很纠结，我真的真的看不出这怎么会是大概率的事。倒不是说它不可能，而是它就是不大可能——我们不太可能把那一整片空间都采样到。所以我对这个非常感兴趣，而这也绝对落在 Luke 的方向里。我们就这个聊了很多。我觉得基本上左边那一侧是 AlphaGo，右边那一侧是 AlphaZero。我认为不被人类那种东游西荡所偏置（biased）的 AlphaZero，才是我们通往远更智能的系统、甚至我斗胆说一句、通往 AGI 的路径。要严谨地表述的话——我得非常小心地说——如果完整的解空间是 F，那么在已知的人类解上训练，会把你限制在某个典型集（typical set）H 里，无论你投入多少可行量级的 test-time compute 或 recursive self-improvement 都一样。你没法在可行的前提下采样到 F 减 H。尤其是采样它的全部。如果是无限的 recursive self-improvement、无限的 test compute，也许可以，但我们没有「无限」。所以人生是个 POMDP，而我们处在一个有限视界的 MDP（finite horizon MDP）里。

[2:37]

Intelligence per sample. I think this is like the two major problems left in my opinion are intelligence per sample, intelligence per watt. And intelligence per sample. I always think about this like as I get one new sample, I do this continuous learning. What is the right thing to do if I'm trying my goal is to maximize performance condition upon that n. Most people's answer to this right now in practice is ICL. And I actually played with this. As you increase the number of samples in ICL, it is not monotonically improving in performance. And so it actually starts to bob and weave. It gets worse. It gets better sometimes. Um and then it hits a cliff, which is the context um uh length, context length that the model was trained on, and it literally just stops. So it clearly can't go on forever. It doesn't monotonically improve. And I started playing around with Laura. I think Laura at higher at lower ranks for uh lower amounts of sample size actually does impressively well. And then it has this kind of arc. They both peter out pretty quickly as you increase number of samples all the way until you do SFT group O all the way at the end. And if you look at this, it's kind of weird that like you have this like ICL is the optimal thing to do in the beginning and then training the whole thing. If I get one new sample, I want to retrain with Laura at some rank on N plus1 samples just to get that little bump in performance. And there's a different optimal thing to do all along the way as I stream and I get more and more samples. And that's just not how we are. So we're kind of like monotonically improving. And the more chess games that Magnus Carlson plays, he just keeps getting better. The, you know, 10,000 hour rule, etc., etc., we just keep getting better. And it's the same algo. And so I think there's just something really different happening in us. And so there's must exist some learning procedure that is has a much higher intelligence per sample. And then intelligence for Watt out of my lab, Ivonica and John who will hopefully come to the next one uh and give a talk on on this. And I just think it's the right way to think about it. Arguing that having smaller models um are sometimes actually better from an intelligence per watt perspective. Alternatives to back prop for those that know me, I'm very hot on this. Back to the brain um and how we learn. There's very little evidence that the brain is taking the transpose of the weight matrix and there must exist some other learning procedure. I'm highly interested in SPSA, but if there's alternatives that I'm not aware of, please like recommend them. And I'm really interested in novel breakthroughs. Yaso is one of my favorite AI researchers, but he's mostly focused on bio and he always um sends me biopers and it's super interesting.

Intelligence per sample（每个样本的智能产出）。我认为目前剩下的两大主要问题，在我看来就是 intelligence per sample 和 intelligence per watt（每瓦特的智能产出）。先说 intelligence per sample。我老在想这件事：当我拿到一个新样本，我做这种 continuous learning（持续学习）。如果我的目标是在给定这 n 个样本的条件下最大化性能，那正确的做法应该是什么？现在大多数人在实践中给出的答案是 ICL（in-context learning，上下文学习）。我实际拿这个玩过。当你增加 ICL 里的样本数量时，性能并不是单调上升的。它其实开始忽上忽下、左摇右摆，有时变差、有时变好。然后它会撞上一个悬崖，也就是这个模型训练时所用的 context length（上下文长度），到那儿它就直接卡住、不动了。所以它显然没法一直这么下去，它不是单调改进的。我又开始拿 LoRA 来玩。我觉得 LoRA 在较低的 rank（秩）、较少的样本量下，表现其实好得惊人。然后它会走出这么一段弧线。随着你不断增加样本数量，这两种方法都很快就乏力了，一直到最后你上 SFT、上 GRPO 才行。如果你看这条曲线，会觉得挺怪的：在最开始 ICL 是最优做法，然后就变成要训练整个模型。如果我拿到一个新样本，我会想用某个 rank 的 LoRA 在 N+1 个样本上重训一遍，就为了换那一点点性能提升。而在我不断流式接收（stream）、拿到越来越多样本的整个过程中，每一步的最优做法都不一样。可我们人根本不是这样的。我们更像是单调改进的。Magnus Carlsen 下的棋越多，他就一直在变强。一万小时定律之类的，我们就是一直在变强。而且用的是同一套算法。所以我觉得我们身上一定有某种非常不一样的东西在发生。因此一定存在某种学习过程，它的 intelligence per sample 要高得多。然后是 intelligence per watt，这是我实验室里的 Ivonica 和 John 在做，希望他们能来下一场做个分享。我就是觉得这是看待问题的正确角度——他们的论点是，从 intelligence per watt 的视角看，用更小的模型有时其实更好。还有 back-prop（反向传播）的替代方案——认识我的人都知道，我对这个非常上头。回到大脑、回到我们是怎么学习的：几乎没有什么证据表明大脑会去取权重矩阵的转置（transpose），所以一定存在某种别的学习过程。我对 SPSA 很感兴趣，但如果有我还不知道的替代方案，求你们推荐给我。我也对全新的突破非常感兴趣。Yas 是我最喜欢的 AI 研究者之一，但他主要专注在 bio（生物）上，他总给我发各种 bio 的论文，特别有意思。

[5:02]

Whether it's about how birds navigate the world via iron in their liver apparently that's how they they actually navigate crazy robotics, uh speech, other things like that as well. And then of course unhinge founder hacks very interested in that as well. Call for ideas on ways to make the club better. So, better ways to meet you if it's a lightning round if it's not. Um, some people talked about some AI benchmarks that we could actually launch together. That'd be kind of fun. Club challenges to challenge each other. And then, uh, any open source ideas that you want to hack on together for this club or something or otherwise. It' be very interesting. All right, that's all I got. Thank you so much.

比如鸟类是怎么在世界里导航的——据说是靠它们肝脏里的铁，它们居然真是靠这个来导航的，疯狂吧；还有机器人、speech（语音）之类别的东西。当然还有那些「不按常理出牌的创始人骚操作」，我对那个也很感兴趣。也征集一下让这个俱乐部变得更好的点子吧。比如有什么更好的方式让我能认识你们——不管是搞成 lightning round（闪电轮）还是别的形式。有些人提到过我们可以一起发布一些 AI benchmark（基准测试），那会挺好玩的。也可以搞俱乐部挑战赛，互相挑战。还有，任何你们想为这个俱乐部、或者别的什么一起开搞的开源点子，都很有意思。好，我要说的就这些。非常感谢大家。

[5:47]

Hi. Yeah. Uh, thanks France for that introduction. We've been labmates now for like two years, something like that. Yeah. Um, I think France is a great example of someone who brings very creative and very out of distribution ideas to our group all the time, even if I sometimes like have no idea where he gets them from. Um, but um, that being said, uh, he asked me to give a talk on some bioai things and I thought why not? Um, so I'll be presenting on this paper that came out just last week from Biohub folks um, here in California, not too far actually in the Bay Area. I think they just moved to the city actually. Um, so I am a second year PhD student with France, but I'm also co-advised by Steve Quake over at Stanford. Sort of anyone in biology probably will know Steve at least tangentially done a lot of work in bioengineering and all kinds of applications was director of the biohub where this work came out um just until recently. So uh a lot of uh a lot of overlap but uh the high level pitch for this work is that I know most of this audience is probably more like AI ML types. I want to talk a little bit about how sort of a lot of these ideas from sort of that's motivating a lot of progress in language modeling and AI very broadly have been sort of recently been translating into biology with a focus on this recent paper because I think it really does a really excellent job of interrogating how scale which you know at some level has been like the fundamental primitive in terms of assumptions that we as a community have in terms of how to make things better um has actually been playing out for a lot of these biological problems particularly protein biology. So um there won't be like much bio in this talk. I'll try to focus more on the ML, but feel free to ask questions. Um so yeah, like I called this talk the uh bitter lesson comes from biology. The actual paper title is right below that. But I mean just a quick refresher. I'm sure everyone in this specific audience probably read Richard Sutton's famous article. You know, basic premise here is that like, you know, across the past 70 years of AI, methods that win are methods that are general that sort of exploit really fundamentals of like scaling compute and data as opposed to methods that sort of handgineer human domain, human domain knowledge. And Sutton always cites his work in or like you know a lot of the work that was early in the field. So alpha go alpha go zero that's sort of just inordinately scaled compute and then for a long time they were far worse than sort of expert systems until they eventually overtook and then exponentially improve past them right knowledge systems win at first but then eventually sort of these like big large dumber models will like um you know win in the long run this is sort of a new goal in biology is to what extent can we study like this is actually also true for a lot of these sort of biological AI problems right um the bet sort of behind this paper and they do a really exploring is well the same pattern basically also saw protein biology right um can we take like you know a lot of these ideas in scaling law analysis here is from the um uh famous you know neural scaling laws paper and then translate them for all these problems that we care about for say designing a drug or like you know trying to understand how like a cell works right so on the left is something that

嗨，是的。感谢 France 的介绍。我们当同门（labmate）现在大概有两年了吧，差不多。我觉得 France 是个很好的例子——他总能给我们组带来非常有创意、非常 out of distribution（跳出常规分布）的想法，尽管我有时候完全搞不懂他这些点子是从哪儿冒出来的。话虽如此，他让我做一场关于 bio AI 的分享，我想，那有何不可呢。所以我要讲的这篇论文就是上周刚出的，来自 Biohub 那帮人，就在加州，其实离这儿不远，就在湾区。我想他们最近刚搬到城里来。我是 France 的二年级博士生，但同时也由斯坦福的 Steve Quake 联合指导。生物领域的人大概多少都知道 Steve，他在生物工程和各种应用上做了大量工作，一直到不久前都还是这篇工作所出自的那个 Biohub 的主任。所以有很多交集。这项工作的高层概括是这样的——我知道在座大多数人可能更偏 AI/ML 这一类，所以我想稍微聊聊：那些推动语言建模和广义 AI 大量进展的思路，最近是怎么开始被迁移到生物学里的。我会聚焦在这篇最近的论文上，因为我觉得它真的非常出色地拷问了一件事：scale（规模）——在某种层面上，scale 一直是我们这个社群在「如何把事情做得更好」这件事上最根本的假设原语（primitive）——它在很多生物学问题上、尤其是蛋白质生物学（protein biology）里，实际上是怎么发挥作用的。所以这场分享里不会有太多 bio 的内容，我会尽量多讲 ML，但欢迎随时提问。所以呢，我把这场分享叫做「bitter lesson 来自生物学（The bitter lesson comes from biology）」。论文的真正标题就在那下面。先快速复习一下——我相信在座这群人里几乎人人都读过 Richard Sutton 那篇著名的文章。它的基本前提是：纵观过去 70 年的 AI，能笑到最后的方法，是那些通用的、真正利用了「扩展算力与数据」这一根本规律的方法，而不是那些手工堆砌人类领域知识（human domain knowledge）的方法。Sutton 总是引用那些早期领域里的工作，比如 AlphaGo、AlphaGo Zero——它们就是把算力反常地往大里堆，然后在很长一段时间里它们远不如专家系统（expert systems），直到最终反超，并以指数级把后者甩开。也就是说，知识系统一开始赢，但最终是这些又大又「笨」的大模型在长跑里赢。这在生物学里成了一个新目标，就是要研究：这一规律在多大程度上对很多生物 AI 问题也成立？这篇论文背后的赌注、以及他们做得很到位的探索，就是：同样的模式基本上在蛋白质生物学里也能看到，对吧？我们能不能把 scaling law 分析里的很多思路——这里这张图来自那篇著名的 neural scaling laws（神经网络缩放律）论文——迁移到所有我们关心的问题上，比如设计一款药物，或者搞懂一个细胞是怎么运作的？所以左边是某种我们……

[8:33]

we trust it's like a language model we have like this nice smooth log linear scaling laws that we see that moss like predictively falls as a function of compute and data uh the question on the right is whether this curve will exist for bio spec more generally but proteins specifically in this paper you know sort of does our LLM recipe transfer or does biology really out of distributional domain relative to language sort of break it right that's the bet and like in this talk I'll basically chat about like three like vignettes from this paper that sort of interrogate to what extent this is true so this slide is all the biology you'll ever need about a quarter of the slide at least for this presentation um let's talk about proteins so in your body there's like broadly three major classes of macro molecules. There's lipids, carbohydrates, and proteins. Um, a protein is just a string of amino acids, a special type of biomolelecule. There's 20 varieties of amino acids. If you put them together into a sequence, you can have like a virtually infinite number of possible molecules that then fold into. So, you can think about it largely as just every single protein is this 20 letter alphabet. And that string specifically determines a unique 3D shape. And by virtue of the shape of that protein, what job it does in your cell like presents catalyzes a reaction, keeps pathogens out, etc. Um, The work done in this paper is that their goal is to train um ESMC sort of their like third major or fourth major iteration in a long series of models of the group of evolutionary scale group originally at Meta then their own company now Biohub have been training for a few years now where the cell is very similar to language where we let's just take hundreds of millions of years of or sort of evolved sequences that we've sort of gone out and found across biology both in humans but also across bacteria and in our environment and just go train a big mass language model on them, right? So, I mean nowadays we mostly train NTP models, but the pitch here is that if I take some protein represented as like you know these strings of 20 tokens like hide a few and then can I train a really big BERT style transformer to predict mass positions as a function of the other ones nearby. And the crucial part is that we never tell it anything about the protein beyond just the sequence.

……我们所信任的东西，就像一个语言模型，我们能看到这种漂亮平滑的对数线性缩放律（log-linear scaling laws），loss 会作为算力和数据的函数、以可预测的方式下降。右边的问题是：这条曲线对 bio 会不会也存在——更广义地说是对生物，但这篇论文里具体说的是蛋白质。我们这套 LLM 的配方能不能迁移过去？还是说生物相对于语言真的是个 out-of-distribution（分布外）的领域，会把它整个搞崩？这就是那个赌注。在这场分享里，我基本上会聊这篇论文里的三个小片段（vignettes），它们分别从不同角度去拷问这件事到底在多大程度上成立。所以这张幻灯片包含了这场报告你将需要的全部生物学知识——至少是其中的四分之一这么一小块。我们来说蛋白质。你身体里大体上有三大类生物大分子（macromolecules）：脂质（lipids）、碳水化合物（carbohydrates）和蛋白质（proteins）。一个蛋白质就是一串氨基酸（amino acids），一种特殊的生物分子。氨基酸有 20 种。把它们串成一个序列，你就能得到几乎无限多种可能的分子，它们再折叠成形。所以你大体可以这么想：每一个蛋白质都是用这套「20 个字母的字母表」写出来的。而这个字符串就唯一地决定了一个独特的三维形状。又因为这个蛋白质的形状，它在你细胞里做什么工作就定了——比如呈递（presents）、催化某个反应、把病原体挡在外面，等等。这篇论文做的工作是，他们的目标是训练 ESM C——这是 Evolutionary Scale 这个团队一长串模型里的第三个、或者说第四个主要迭代版本。这个团队最早在 Meta，现在自己开了公司，如今在 Biohub，他们已经训练这类模型好几年了。这里的「细胞」跟语言非常像：我们就拿上亿年间演化出来的序列——我们跑遍生物界、从人类身上、也从细菌身上、从我们所处的环境里找来的序列——然后就在它们上面去训练一个大的掩码语言模型（masked language model）。当然，如今我们大多训练的是 NTP（next-token prediction，下一个 token 预测）模型，但这里的卖点是：如果我拿某个蛋白质、把它表示成这些由 20 种 token 组成的字符串，然后藏掉（mask 掉）其中几个，那我能不能训练一个非常大的 BERT 风格的 transformer，让它根据附近的其它 token 去预测这些被掩掉的位置？而关键的一点是：我们从不告诉它关于这个蛋白质的任何信息，除了序列本身。

[10:34]

Right? So all this guy's got access to is just this string and it's being asked to basically learn things about the grammar of that protein as a function of which protein other amino acids tend to co-occur with right so like I think there's like this old saying in natural language processing it's like you'll know a word by the company that it keeps and here the idea is that you'll know a protein by amino acids it keeps and the bet is that if we do this at scale just on the simple sequence task we will eventually get all these sort of other properties of protein say like structure that we do care about sort of for And uh yeah like I said before there's been a lot of prior work on this like largely from evolutionary scale but a few other or a few other sort of groups working largely on this bit. Uh this table will be a map for the rest of the talk. So like every row is a concept you probably already know from natural language and then analog onto the protein context. So tokens become amino acids. The internet becomes sort of all evolution sequence databases all the proteins we can actually go out and measure. Mass token prediction stays as mass token prediction and sort of emerging capabilities. we talk about language model having like become emerging structure and function within like basically understanding of a protein and then there's also sort of like this really fun stuff at the bottom. So like recently there's been a lot of advancements in sort of these interpretability toolkits from the mechi folks you know things like sparse autoenccoders some of the earliest work basically in really trying to interrogate um using the toolkit the language modeling community has built to understand language models now in a protein language model setting. So I'm going to fill in the right hand column for the rest of this talk with sort of evidence and three questions which is that do these models learn with scale? Um can they basically substitute for a lot of these handbuilt features sort of does the bitter lesson hold and like what do these representations actually encode interpretably? So question one is do scaling laws even hold in the protein context in the way that we see them in the language context. First let me just try talk a little bit what we measure when we're talking about sort of emergent properties sort of how do we actually like study the model see if it's learning anything right we need a proxy for does the model understand protein structure for instance right um the one the authors use in this paper is that they look at the internal or they basically take the model representations during training and they use this to predict um long distance protein contacts so the idea here is that proteins have a one-dimensional sequence but they fold into complex threedimensional shapes and if the model is sort of understood something complex about the protein structure or something emerging about the protein structure. It should be able to predict um contacts that occur over long distances sort of nearby contacts are rather kind of obvious and this is like a really challenging object for it to get just sort of denovo purely from sequences alone. They called this P at L right um sort of a long contact precision at some given length and it's just a clean unsupervised readout sort of structural knowledge inbuilt in the model that's learned during this language modeling

对吧？所以这家伙能拿到的全部信息就只有这个字符串，而它被要求去做的，基本上就是学会这个蛋白质的「语法」——根据哪些其它氨基酸倾向于跟某个氨基酸共同出现（co-occur）来学。自然语言处理里有句老话：「观其伴而知其词（你通过一个词结伴的对象来认识这个词）。」这里的思路就是：你通过一个蛋白质结伴的那些氨基酸来认识这个蛋白质。而这个赌注是：如果我们在规模上、仅仅在这个简单的序列任务上做这件事，最终就能得到蛋白质所有那些我们确实关心的别的性质，比如说结构（structure）。是的，就像我前面说的，这方面已经有很多在先的工作，主要来自 Evolutionary Scale，也有另外几个团队基本上在做这件事。这张表会是这场分享接下来部分的「地图」。每一行是一个你大概早就从自然语言里知道的概念，然后把它类比到蛋白质的语境里。于是 token 对应成氨基酸；互联网对应成所有演化序列数据库——所有我们真能跑出去测量到的蛋白质；掩码 token 预测（mask token prediction）还是掩码 token 预测；至于涌现能力（emerging capabilities），在语言模型里我们谈的是涌现出某些能力，而在这里则是涌现出对一个蛋白质的结构与功能的理解。底下还有一些特别好玩的东西。最近在 interpretability（可解释性）的工具箱方面有很多进展，来自做 mech interp（机制可解释性）的那帮人，比如 sparse autoencoders（稀疏自编码器）这类东西——最早的一批工作基本上就是用语言建模社群造出来的这套工具，去拷问、去理解语言模型；现在则把它搬到蛋白质语言模型的场景里。所以接下来这场分享，我会用证据和三个问题把这张表的右栏填满。这三个问题是：这些模型会不会随 scale 学习？它们能不能基本上替代掉很多手工搭建的特征（handbuilt features）——也就是 bitter lesson 在这儿成不成立？以及这些表征（representations）以可解释的方式实际编码了什么？所以问题一：scaling law 在蛋白质语境里成不成立——是不是像我们在语言语境里看到的那个样子？先让我稍微讲讲，当我们谈所谓涌现性质（emergent properties）时，我们究竟在测量什么、我们究竟怎么去研究这个模型、看它有没有学到任何东西。我们需要一个代理指标（proxy），来衡量「这个模型理解不理解蛋白质结构」。这篇论文的作者用的那个指标是：他们在训练过程中提取模型的内部表征，用它来预测蛋白质的长程接触（long distance contacts）。这里的思路是：蛋白质有一个一维序列，但它们会折叠成复杂的三维形状。如果这个模型对蛋白质结构理解到了某种复杂的东西、或者涌现出了某种关于蛋白质结构的东西，那它就应该能预测那些发生在长距离上的接触——近距离的接触相当显而易见，而这个对它来说是个相当有挑战性的目标，因为它得纯粹从序列本身、从头（de novo）把这些搞出来。他们把这个指标叫做 P@L，就是在某个给定长度下的长程接触精度（long-range contact precision），它是一个很干净的无监督读出（unsupervised readout），衡量在这个语言建模目标的训练过程中，模型内建学到的结构知识……

[13:08]

objective. Um on the right I plot the performance of this or the authors plot the performance of this I should say against training compute for the for basically this new model family the authors have built recently called the ESM cranberry at 300 million 600 million 6 billion parameter scales. uh interestingly and they had this fit line which is basically this predict compute optimality curve which they um estimated just from sort of lowend training runs. So relatively low computational budget and they find it actually extrapolates very cleanly to real model training runs meaning so the answer is like do these models with scale and this data at least suggests that the answer is like yes right like you do see this nice log linear curve right if you keep investing more and more compute you training more and more protein data with larger and larger models um you see the same exact same broad qualitative shape as the LM scaling or sort of LM setting and arrest retransfers cleanly meaning that without any kind of like predisposed part of the model that we've taught to look at purching structure even didn't get any protein structures. It does a good job of sort of picking these out just from sequence co-occurrence patterns. Um there's like one interesting twist though is that I said before there's been a lot of prior work from this group as well as others and trying to answer these scale questions. So not the first ones to look at this but previous models um so the sort of the prior generation ESM2 models shown in um purple here had actually not shown the same behavior. They sort of hit this wall where they kept adding more parameters and they got diminishing returns and you had this sort of flattening out the scaling curve. this ESMC or ESM Cambrian model sort of the green line keeps climbing with no plateau. And their fix for this wasn't really like they came up with like a really clever inductive bias in the architecture. Not to say there isn't a lot of excellent engineering work in this paper, but really it was just data scaling, right? They um had about 50 million training samples in their original ESM2 paper and here they just pushed that to 2.8 billion by pulling largely in metagenomic data. So essentially amino acids or protein sequences that have been found from sequencing DNA actually out in like dirt and oceans and like human guts from like organisms that nobody has like really ever cultured or even has really really elucidated. And their conclusion is that more data ends up being really important and keep getting sort of uh are basically justifying the cost for increasing compute. So it's like the protein version of LM data wall conversation, right? Like except here in biology, evolution has been generating this train data for for four billion years and not humans in like the past 30 or so. And you know compared to tokens in natural language like I mean we've only sampled like less than 1% of all known protein sequence diversity and that's like only currently at this moment in time let alone like all of the sequence diversity evolution has sampled since the beginning of life on Earth.

……目标。在右边，我（应该说是作者）把这个指标的表现对训练算力作图，针对的就是作者最近搭的这个新模型家族，叫 ESM Cambrian（ESM 寒武纪），在 3 亿、6 亿、60 亿参数这几个规模上。有意思的是，他们还拟合了一条线，基本上就是这条「预测算力最优」的曲线（compute-optimality curve），是他们仅仅从低端的训练 run（相对很低的算力预算）估出来的。结果他们发现，它居然能非常干净地外推到真实的大模型训练 run 上。意思就是说，对于「这些模型会不会随 scale 学习」这个问题，至少这份数据暗示的答案是「会」。你确实能看到这条漂亮的对数线性曲线：如果你持续投入越来越多的算力、用越来越大的模型在越来越多的蛋白质数据上训练，你会看到跟 LM（语言模型）缩放、也就是 LM 场景里几乎一模一样的、宏观上同样的定性形状，而且这套东西迁移得很干净。这意味着：我们没有在模型里预置任何「专门去看蛋白质结构」的部件，甚至根本没给它任何蛋白质结构，它却光靠序列共现模式（co-occurrence patterns）就把这些结构信息挑出来了，而且干得相当不错。不过有一个有意思的转折：我前面说过，这个团队以及其他人在回答这些 scale 问题上已经有很多在先的工作，所以他们不是第一批看这个的。但之前的模型——也就是上一代的 ESM2 模型，在这儿用紫色画出来——其实并没有表现出同样的行为。它们撞上了一堵墙：他们不断往上加参数，却得到递减的收益（diminishing returns），于是缩放曲线就这么平掉了。而这个 ESM C、也就是 ESM Cambrian 模型，也就是这条绿线，则一直往上爬，没有出现平台期（plateau）。而他们对这个问题的解法，并不是说他们在架构里想出了什么特别巧妙的归纳偏置（inductive bias）——不是说这篇论文里没有大量出色的工程工作，但真正起作用的其实就是数据规模化（data scaling）。他们最初那篇 ESM2 论文里大约有 5000 万个训练样本，而这里他们把这个数字一路推到了 28 亿，主要靠拉入宏基因组（metagenomic）数据。所以本质上就是那些从「实地测序 DNA」得来的氨基酸或蛋白质序列——从泥土里、海洋里、人类肠道里，从那些根本没人真正培养过、甚至从没真正搞清楚过的生物体里测出来的序列。他们的结论是：到头来更多的数据真的非常重要，而且不断地证明了增加算力这笔成本是值得的。所以这就像是 LM 那场「数据墙（data wall）」讨论的蛋白质版本，对吧？只不过这里在生物学里，是演化（evolution）用了四十亿年来生成这批训练数据，而不是人类在过去 30 年左右生成的。要知道，跟自然语言里的 token 相比——我是说，我们才采样了所有已知蛋白质序列多样性中不到 1% 的部分，而这还只是当下这一刻已知的部分，更别提演化从地球生命起源以来所采样过的全部序列多样性了。

[15:33]

Um sort of question two in this paper I think is interesting is that um it's sort of the most bitter lesson part and they really try to evaluate to what extent their paper can do or how well their model trained purely on mass language modeling objectives can compete against a structure based model with sort of handtuned inductive components. So I'm sure you're all familiar with Alphaold won the Nobel Prize a few years ago was sort of a landmark moment in bio really show that these computationals have a lot of value in the biology sphere. Alfold is brilliant but its power comes from basically building handput in or handbuilt inputs sort of a manual feature curation called a multiple sequence alignment or an MSA. So to fold a protein it goes and finds hundreds of evolutionary cousins of that protein and stacks them up. Um these patterns of sort of coariation across a family are essentially this encodesical information you need to do to be able to get structure. This is like a beautiful domain engineering application and it's the sort of like really good human crafting objective bias that the bitter lessons at least claims should eventually lose right think like hog features in CD and compared to sort of things we used to do before this is actually like far more bitter lesson than like say building a whole physics simulator for a protein but it's also really slow to do this right we need to build this huge databases the sequence alignment it takes time right and it's absent precisely where you often want it for instance the antibody design task we come back to at the end um ESM just throw this away all it says is it just takes input sequence and instead of an alignment and it just feeds in the model's representations as the input to their structure predictor and these are just like per residue embeddings. So take your input sequence you get a set of like per amino acid just like some numerical representation and we just train the specialized module to do predicting the like large protein structure right so this folding network it's kind of like a projection into uh 3D corded space so same target same output no handbuilt features and the question becomes can this general model representation like match the sort of specialist model in getting that MSA value one interesting architectural note though for sort of the more ML folks in the crowd um the one there in their projection networks for the part that converts representation to structure.

这篇论文里我觉得很有意思的第二个问题，可以说是最贴近 bitter lesson 的那部分——他们认真去评估了，纯粹用 mass language modeling（掩码语言建模）目标训练出来的模型，能在多大程度上、或者说能多好地，跟一个基于结构、带有人工调过的 inductive（归纳偏置）组件的模型一较高下。我想大家应该都熟悉 AlphaFold，它几年前拿了诺贝尔奖，可以说是生物领域的一个里程碑时刻，真正展示了这些计算方法在生物领域有巨大的价值。AlphaFold 很出色，但它的威力基本上来自于构建人工放进去、或者说人工搭建的输入——一种叫做 multiple sequence alignment（多序列比对，MSA）的人工特征整理。所以为了折叠一个蛋白质，它会去找那个蛋白质的成百上千个进化上的“表亲”，把它们堆叠起来。这些跨整个家族的共变（co-variation）模式，本质上编码了你做结构预测所需要的信息。这是个非常漂亮的领域工程应用，是那种很优质的、人工精心打造的目标偏置——而 bitter lesson 至少声称，这类东西最终应该会输，对吧，就像计算机视觉里的 HOG 特征一样。而且跟我们以前的做法相比，这其实比给蛋白质搭一整套物理模拟器要“bitter”得多。但这么做也真的很慢，对吧，我们得构建这些庞大的数据库、做序列比对，很费时间。而且恰恰是在你最想要它的地方它却缺席——比如我们最后会回头讲的抗体设计任务。ESM 就把这一整套扔掉了，它说的就是：我只拿输入序列，不要比对，直接把模型自己的表征（representations）喂给结构预测器，这些就是逐残基（per residue）的 embedding。所以你拿你的输入序列，得到一组逐氨基酸的、纯粹是某种数值表征的东西，然后我们只训练一个专门的模块去预测那个大的蛋白质结构。所以这个折叠网络，有点像是往三维坐标空间里的一个投影——同样的目标、同样的输出，但没有人工搭建的特征。于是问题就变成了：这种通用模型的表征，能不能在拿到 MSA 那份价值上，匹配上专门的特化模型？不过有一个有意思的架构上的注脚，给在场更偏 ML 的朋友们——他们在投影网络里，也就是把表征转成结构的那部分里……

[17:28]

There is actually one really interesting feature that actually builds off some of the work from our lab alum Dan Fu. Um and they have a actually a looped model, right? I mean there's a lot of excitement about these recently for parameter sharing and I just think they're cool algorithmically for a number of reasons. And this is gives them basically a lever by which they can scale inference time compute, right? So essentially they have a model that predicts structures and they have a procedure by which representations can be fed through a series of layers and sort of refine their structure predictions without necessarily retraining or any kind of fine tuning. This is like our test time compute access and something like say diffusion steps could be or like test time sampling from LA lab. I'll keep this in mind just for later results. And the sort of like headline figure I would say pointing out here is that um they basically show that yeah their technique works really well. Um just a quick definitions on the left we have this thing called DOCQ pass rate. This is just a metric for how good your structure prediction was. Essentially it's a measure of the fraction of test cases where the predicted shape of two proteins stick that stick close together is close enough to be like really useful to realistic settings. And there are two groups in each panel. One is for single sequence with no MSA and the other is um a single sequence plus an optional MSA you can also feed to the model or is required for competitor model. And when we look at the sort of outcomes from this, what we see is that for general protein protein complexes, ESM fold 2, their sort of new projection model from a single sequence with no MSA lands within about three points of alpha 3 which does take these handcrafted features. So we get near par without the crutch and but if we look at the antibody applications which is on the right on the left hand side here right um the modality but is like you know essentially behind like all modern NC or MAB based drugs or monol antibodies tons and tons of applications in human biology and biotech. um we are actually winning or are comparably winning or the authors are comparably winning. So broadly like single sequence ESM fold 2 does actually build alpha fold 3 sort of 50 versus 47 on this really specific design task that people really do care about and biologically this makes a lot of sense compared to say like um other classes of proteins the amount of sort of sequence variation that's been sampled in the space of all known antibodies relative to structure is considerably smaller considering their enormous diversity. So the headline isn't that MSAs are dead yet, right?

那里其实有一个非常有意思的特性，它实际上是建立在我们实验室校友 Dan Fu 的一些工作之上的。他们用了一个 looped model（循环模型），对吧，最近大家对这类模型很兴奋，因为它能做参数共享，而且我从算法角度就觉得它们很酷，有好几方面的原因。这基本上给了他们一个杠杆，可以用来扩展 inference time compute（推理时算力），对吧。所以本质上他们有一个预测结构的模型，并且有一套流程，可以让表征反复地过一系列层、不断精炼它的结构预测，而不必重新训练、也不需要任何 fine-tuning。这就相当于我们的 test time compute（测试时算力）入口，类似于比如 diffusion steps（扩散步数），或者像 LA 实验室那种 test time sampling（测试时采样）。这一点我先记着，留到后面的结果再说。我想在这里指出的那张“头条图”是——他们基本上证明了，是的，他们这套技术效果非常好。左边先快速讲两个定义：我们有个东西叫 DOCQ pass rate（DockQ 通过率），这就是衡量你结构预测有多好的一个指标。本质上它衡量的是这样一个比例：在测试用例里，两个会贴在一起的蛋白质，其预测出来的形状有多大比例足够接近真实情况、接近到对现实场景真正有用。每个 panel（子图）里有两组，一组是单序列、不带 MSA，另一组是单序列再加一个可选的 MSA——这个 MSA 你也可以喂给模型，或者是对手模型必须要的。当我们看这里面的结果时，会发现：对于一般的蛋白质-蛋白质复合体，ESMFold 2，也就是他们这个从单序列、不带 MSA 出发的新投影模型，落在距离 AlphaFold 3 大约三个点以内，而 AlphaFold 3 是要用那些人工打造的特征的。所以我们在没有那根“拐杖”的情况下逼近了平手。但如果我们看抗体方面的应用，也就是这里右边、我左手边的这个——这种 modality（药物形态）基本上是所有现代 NC 类或 MAB 类药物（单克隆抗体，monoclonal antibodies）背后的东西，在人体生物学和生物技术里有海量海量的应用——我们其实是赢了，或者说打成相当不错的平手，或者说作者们打成了相当不错的平手。所以总体上，单序列的 ESMFold 2 在这个人们真正在意的、非常具体的设计任务上，确实压过了 AlphaFold 3，大概是 50 对 47。从生物学上讲这也很合理：跟比如其他几类蛋白质相比，在所有已知抗体所构成的空间里，相对于结构而言、已经被采样到的序列变异量要小得多——考虑到它们本身巨大的多样性。所以这里的头条结论并不是说 MSA 已经死了。

[19:32]

It's that handle features only help where it's abundant and basically where drug designers really need it often does go away. And this general method still basically just save a lot from pre-treating across all known revolutionary contacts. So we're not quite there yet. And one other thing though worth flagging is that a second point says give it MSA. We can also scale the amount of test time compute. So how many loops we run in this recursive model in order to prove performance. And we do see um basically returns on this meaning that like the better loss at least at inference time also seems to broadly hold. And it's not just accurate just as an aside. This is just quick um it's also just much faster. MSA construction just takes a lot of classical computational biology time. So at least if throughput is your concern or latency is your concern, you can with this single representation like get quicker results. Though the wall clock times here are like you know well within like I would consider to be pretty good to start off with. Um, and the last bit, I'll get through this a little bit quicker, is just they did a really interesting analysis of like sort of mechanistic interpretability, like what are these models actually learning and sort of can we find features that are interpretable as humans in the same way that sort of language modeling folks in the Mechai community have found in language models like anthropic has. Um here they sort of just apply the same tool or they borrow a lot of the tools for like sparse coding analysis here where they look at activations from these models and try to see if they can decouple them find these like mono semantic activating directions inside their feature spaces and they ask is this also going to be a property in protein models and their answer is largely yes um right so from like pure fill-in-the-blank pre-training the model's latent space decomposes into clean features that correspond to real biological concepts here the these concepts have been annotated by LM agents And they're organized actually quite interestingly in a nice hierarchy. So you have like features that correspond to say individual amino acids at the bottom then like structural motifs then like whole protein domains, right? So look longer or larger portions of the individual protein molecule up to like functional sites and whole protein roles, right? And none of this was supervised, right? The model like learned to organize its latent space purely just through MLM, which is like crazy. Um I'll just with one example maybe to close things out before I finish everything and I think I'm actually have one more slide after this. Um this is a instance of a feature activation that corresponds to a really specific well-known protein motif called the nucleophilic elbow. This is a type of catalytic domain that's used in a lot of enzyme catalysis. It's really interesting because it's evolved multiple times in multiple different proteins unrelated to each other. So it's a it's a vitif biology keeps coming back to and the model has basically learned to identify in the four quite structurally diverse proteins from like both evolutionary distance as well as the rest of the protein. So it's like found a consistently occurring motif in very different backgrounds. So it's like it's basically learn to look at the right thing not just sort of memorizing

而是说，人工特征只在它本身就很充裕的地方才帮得上忙，而恰恰在药物设计者真正最需要它的地方，它往往就消失了。这个通用方法基本上仍然靠的是在所有已知进化接触（evolutionary contacts）上做预训练所学到的大量东西。所以我们还没完全到位。还有一件值得指出的事是，第二个点说的是：给它 MSA，我们同样可以扩展 test time compute 的量——也就是在这个递归模型里跑多少个循环，来提升性能。我们确实看到了基本上是有回报的，意思是说那条“bitter lesson”至少在推理时似乎也大体成立。而且它不只是更准，顺带一提——这点很快——它还快得多。构建 MSA 要耗费大量经典计算生物学的时间。所以至少如果你关心吞吐量、或者关心延迟，用这种单一表征就能更快拿到结果。不过这里的墙钟时间（wall clock time）本来就在我认为相当不错的范围里。最后一小块，我会讲快一点，就是他们做了一个非常有意思的 mechanistic interpretability（机制可解释性）分析——这些模型到底在学什么？我们能不能像语言建模圈、像 Mech Interp（机制可解释性）社区在语言模型里找到的那样、像 Anthropic 那样，在这里找到对人类而言可解释的特征？这里他们基本上是套用了同样的工具，或者说借用了很多做 sparse coding（稀疏编码）分析的工具——他们看这些模型的激活，试图把它们解耦、在其特征空间里找到那些 mono-semantic（单一语义）的激活方向，然后问：这是不是在蛋白质模型里也成立的一个性质？他们的答案基本上是肯定的。所以从纯粹的“完形填空”式预训练出发，模型的隐空间（latent space）分解成了一些干净的特征，对应于真实的生物学概念——这里这些概念是由 LM agents（语言模型 agent）标注的。而且它们的组织方式其实相当有意思，呈现出一个漂亮的层级。所以你在最底层有对应单个氨基酸的特征，然后是结构基序（structural motifs），再然后是整个蛋白质结构域（protein domains），也就是单个蛋白质分子里更长、更大的片段，一直往上到功能位点（functional sites）和整个蛋白质的角色。而这一切都没有被监督，对吧——模型纯粹通过 MLM（掩码语言建模）就学会了这样组织它的隐空间，这简直疯了。我在结束之前可能就用一个例子来收尾——我想这之后其实我还有一张幻灯片。这是一个特征激活的实例，它对应于一个非常具体、广为人知的蛋白质基序，叫做 nucleophilic elbow（亲核肘）。这是一类用于很多酶催化的催化结构域。它很有意思，因为它在多个彼此不相关的不同蛋白质里独立演化出来过很多次。所以这是一个生物学一再回到的基序，而模型基本上学会了在四个结构上相当不同的蛋白质里识别它——既跨越进化距离，也跨越蛋白质的其余部分。所以它就像是在非常不同的背景里找到了一个反复出现的基序。所以它基本上学会了去看对的东西，而不只是去记住……

[22:07]

like you know broad similarly comparable sequences. It's like a deeper level of intuition. And if you look at the sort of the whole SE activation space, you can find like nice structures that sort of correspond to like various known aspects of biology, right? This organization isn't just local, it scales to all of life, right? So they um ended up building actually a huge atlas of their pro with their model afterwards sort of just folding and analyzing um millions of or up to I think seven billion proteins. This is the largest atlas I think out there in alpha protein structure databases, more than alpha folds even. And they've predicted like you know O of a billion of these as I mentioned before and laid them out here by the representations in SAPE space and you get like a really nice interesting like protein space family map right you can find that there's clear families that'll cross clear here are like for instance crisper castine enzymes which if you're not a biologist maybe you still probably have heard of and really important for a lot of biotechnology applications it's kind of like a Google maps from proteins and it's produced all as a byproduct of the model right like just naturally it's like picked up evolutionary relationship as well as functional ones just denovo for free which I think is like I don't know if you're maybe not a protein nerd like me I just think this is like utterly crazy right um so like just to finish like does a bitter lesson scale to biology not perfectly yet I mean some of this analysis still requires a lot of handcrafted features and it's not fully competitive but we're getting very close um but even if we just don't care about one specific downstream the model just from a relatively quite small amount of or like a relatively quite simple pre-training objective and a lot of data has like learned an enormous amount of bio that we can reverse interrogate after the fact um and just for record like they found that data scaling does keep improving. Um I want to just point out you know partially as a process like our partially just like try to convert a lot of smart people like we have in the audience there's lots of folks work on ML a lot of applications software um biology is a great place to work in ML because the models are still really young and the other thing is that the data is increasing exponentially per year and that rate of increase is also going up meaning that like we're not data limited it's a great time to work in this space and we need a lot of these tools uh and any audience members watching this on YouTube similar pitch um just as one last thing um I didn't get talking into detail but the one application they use for their models for inverse design. So they actually develop a lot of potential protein drugs and they validate a lot of use at least in um wet lab settings to show that these are potential like proteins that you can design using this model purely in sequence space for the most part by the way um with the exception of like one structure head at the end um that bind various like known molecules that have therapeutic effect right so for instance uh this PDL1 binder is basically the most or is like basically a medication that is now the sort of big success of amunotherapy it's helped plenty of patients with cancers in ways that historically have never been able to tackle before, right? And developing

……那种宽泛相似、大体可比的序列。这是一种更深层次的直觉。而如果你去看整个 SAE 激活空间，你能找到一些漂亮的结构，对应于生物学里各种已知的方面。这种组织不只是局部的，它一直扩展到所有生命，对吧。所以他们后来用这个模型构建了一个巨大的图谱（atlas），基本上就是去折叠和分析数百万个、我想多达大概七十亿个蛋白质。我认为这是现存最大的蛋白质结构图谱，比 AlphaFold 的还大。他们预测了我前面说的差不多十亿个，然后按它们在 SAE 空间里的表征把它们铺排出来，你就得到一张非常漂亮、非常有意思的蛋白质空间家族图谱——你能发现有清晰的家族会聚成一片，比如这里就是 CRISPR Cas 类酶，如果你不是生物学家，可能你也还是听说过它，它对很多生物技术应用都非常重要。这就有点像是蛋白质的 Google Maps，而它完全是作为模型的一个副产品产出的，对吧，就是很自然地、它就在白手起家（de novo）、免费地把进化上的关系以及功能上的关系都拾起来了——我觉得这……我不知道，如果你不像我这样是个蛋白质狂热者，我就觉得这简直疯了。所以收个尾：bitter lesson 能扩展到生物学吗？还没完美做到。我是说，这里有些分析仍然需要大量人工特征，还没有做到完全有竞争力，但我们已经非常接近了。不过就算我们不在意某一个具体的下游任务，模型仅仅从一个相对相当小、或者说相对相当简单的预训练目标加上大量数据，就已经学到了海量的生物学知识，而我们可以事后反向地去拷问它。另外为了存档说一句，他们发现数据规模化（data scaling）确实仍在持续带来提升。我想顺便指出一点，部分算是一种自我安利——因为现场我们有很多聪明人，很多人做 ML、做很多应用、做软件——生物学是一个做 ML 非常好的领域，因为这些模型还非常年轻；另一件事是数据每年在指数级增长，而且这个增长率本身也在上升，意味着我们并不受数据限制。现在是进入这个领域非常好的时机，我们也很需要这些工具。任何在 YouTube 上看这个的观众，同样安利一下。最后再说一件事——我没有展开细讲，但他们把模型用于的一个应用是逆向设计（inverse design）。所以他们其实开发了很多潜在的蛋白质药物，并且验证了不少、至少在湿实验室（wet lab）环境里验证了，证明这些是你可以用这个模型设计出来的潜在蛋白质——顺便说，基本上大部分都是纯粹在序列空间里做的，除了最后有一个结构 head（结构预测头）之外——这些蛋白质能结合各种已知的、具有治疗效果的分子。比如说，这个 PD-L1 结合物基本上就是免疫治疗（immunotherapy）那个巨大成功背后的一种药物——它已经帮助了大量癌症患者，以历史上从未能够攻克的方式。而开发……

[24:45]

medications that sort of targeted this protein was immensely challenging. And like if we can basically reduce the costs for developing such future drugs for future targets, it would have enormous human impact. So like even if the data scale doesn't sell you, then maybe some of the human impact will. But broadly speaking, it's a really exciting time and it's wonderful to see that a lot of these lessons are at least translating and people are really making steady progress. Okay, next we have Luke. um second year PhD out of uh Tatsu and Tangu's lab uh fresh from the UK. Then he went to Harvard CS uh worked on adversarial robustness and now post-training selfplay and is directly uh uh in the spirit of this um alpha zero kind of mindset and so we've been chatting with that about that a lot. All right, please welcome Luke. Okay. Hi everyone. Um, yeah, I'm Luke. Um, I guess I'll be presenting on this paper we put out uh a few months ago called Scaling Selfplay with Selfguidance. I guess more generally, I'll be talking about selfplay for LMS. Um, this work was with some great co-authors, Caillou, Kan, and my two advisers, Tatu and Tangu. Okay, so um, what does the current training stack look like for big LMS? Two simple parts basically. We pre-train the model on web text and then we postrain it. And interestingly recently the post- trainining we've ended up spending you know a huge amount of compute on doing large scale long reinforcement learning runs. And what does that reinforcement learning look like? You collect a huge number of tasks coding tasks maths tasks tasks interacting with different bits of software. And you just have the agent take a bunch of actions in those environments. you get some reward back and we train the model on that data upwaiting the good rollouts down waiting the bad rollouts and like I said the interesting change that's happened is we're now approaching the amount or even surpassing that we're spending on pre-training actually on this very long running RL post training and I've swept some things under the rug that we do at post training as well like a bit of instruction tuning and and uh alignment but really most of the compute spent on these long RL runs okay so we also know that as we increase the number of uh RL tasks during post- training and we increase the amount of compute we get better downstream performance and I think this is best illustrated by this like really beautiful plot from the composer 2 technical report from cursor where what they're both basically showing is they have loads of RL tasks such that they only ever the model only ever sees each task once and so on the x-axis scaling training step is basically each training step I'm putting in some compute and a new RL task and what they show is nice smooth line as you increase the amount of tasks and compute you put in, you get this reliable improvement.

……那种靶向这个蛋白质的药物，曾经是极其有挑战性的。如果我们基本上能为将来针对新靶点的此类药物开发降低成本，那对人类的影响将是巨大的。所以就算数据规模化打动不了你，也许其中一些对人类的影响会打动你。但总体上，这是个非常激动人心的时刻，很高兴看到很多这些经验教训至少正在被迁移过来，人们也确实在稳步取得进展。好，接下来是 Luke。他是 Tatsu 和 Tengyu 实验室的二年级博士生，刚从英国过来。之后他去了哈佛读 CS，做过对抗鲁棒性（adversarial robustness），现在做 post-training 里的 self-play，而且直接就是契合这种 AlphaZero 式的思路——所以我们一直跟他聊这个聊了很多。好，欢迎 Luke。好，大家好。是的，我是 Luke。我想我会讲我们几个月前放出的这篇论文，叫做 Scaling Self-Play with Self-Guidance（用自我引导扩展 self-play）。更广义地说，我会讲 LLM 的 self-play。这项工作是和几位很棒的合作者一起做的——Caillou、Kan，以及我的两位导师 Tatsu 和 Tengyu。好，那么，现在大模型的训练栈（training stack）长什么样？基本上就两个简单的部分：我们先在网页文本上做 pre-train，然后做 post-train。有意思的是，最近这个 post-training，我们最后在大规模、长时间的强化学习（RL）跑批上花了巨量的算力。那这个强化学习长什么样？你收集大量的任务——编程任务、数学任务、跟各种软件交互的任务，然后你让 agent 在那些环境里采取一堆动作，你拿回一些 reward，然后我们就在这些数据上训练模型，给好的 rollout 加权、给坏的 rollout 降权。就像我说的，已经发生的那个有意思的变化是，我们现在在这种长时间运行的 RL post-training 上花的算力，正在逼近、甚至超过我们在 pre-training 上花的量。我也把一些我们在 post-training 里做的事情含糊带过了，比如还有一点 instruction tuning（指令微调）和 alignment（对齐），但真正大部分算力都花在这些长时间的 RL 跑批上。好，那我们还知道，当我们在 post-training 期间增加 RL 任务的数量、增加算力时，我们能得到更好的下游性能。我觉得这一点用 cursor 那份 Composer 2 技术报告里的这张非常漂亮的图来说明最好不过——他们俩基本上展示的是，他们有海量 RL 任务，多到模型对每个任务都只见过一次。所以横轴上，扩展训练步数（scaling training step），基本上每一个训练步我就投入一些算力、加一个新的 RL 任务，而他们展示出来的是一条漂亮平滑的曲线：随着你投入的任务和算力增加，你会得到这种可靠的提升。

[27:39]

And I guess they had this nice eval set on the left, but they also have a downstream benchmark on actual coding on the right. And that's also like increasing reliably in a really nice way. This recipe tells us great, just collect more and more RL tasks, put them in a loop, and model going to keep getting better and better. But generally, we're going to have to collect these RL tasks by hand, which might be a problem if you want to keep on feeding. You'll notice log scale on the x-axis there. And I guess there's another problem where you might think that um eventually we'd like the model to surpass any of the problems we can give it. So I guess the question that Cell Play asks is how can we automatically generate new RL task to the model, train on those and repeat. Okay, so like I said in traditional RL, we'll have a predefined task and we train the model on that predefined environment and task. But in selfplay, we do something slightly different where the model does two things. It's going to generate RL tasks and it's going to attempt to solve those tasks. And crucially, we train it to be better at both of these things. So, we train it to be better at in virtual commas, we'll go through what it means to be better to generate tasks and then also to get high reward in those tasks. So, how do we fit I guess some papers we've likely seen from the past into this description of selfplay? Because you might be thinking, this doesn't look exactly like what I thought of when I read the alpha go alpha zero paper. So those traditional works we'd call symmetric selfplay. And in this case uh let's say in alpha go how you train the model is you have the go agent and then you have the rules of go and you have the go board. That's great but that is nonrl environment I can interact with. Like I need an opponent to play against. And so this generate RL task part. They have an older version of the agent take the role of the opponent. So in this case generating the task because I just put an older version of myself in there and now I have a nice RL task. It's a go board with an opponent. So this would traditionally be called symmetric selfplay because the model is taking on the same ball twice, a go player.

我想他们左边有这么一个不错的评测集（eval set），但他们右边还有一个在真实编程上的下游 benchmark，而那个也在以一种非常漂亮的方式可靠地往上走。这个配方告诉我们：太好了，只要不断收集越来越多的 RL 任务，把它们放进一个循环里，模型就会越来越好。但一般来说，我们得靠人工来收集这些 RL 任务，如果你想一直喂下去，这可能就是个问题。你会注意到那里横轴是 log scale（对数刻度）。另外还有一个问题，你可能会想，我们最终是希望模型能超越我们能给它的任何问题。所以 self-play 提出的问题就是：我们怎么能自动生成新的 RL 任务给模型、在那些任务上训练，然后再重复。好，就像我说的，在传统 RL 里我们会有一个预先定义好的任务，我们就在那个预定义的环境和任务上训练模型。但在 self-play 里，我们做的事情略有不同——模型做两件事：它要生成 RL 任务，也要尝试去解这些任务。而关键在于，我们训练它把这两件事都做得更好。所以我们训练它在打引号的意义上更“好”——我们待会会过一遍“更好地生成任务”、以及“在这些任务里拿到高 reward”分别意味着什么。那我们怎么把过去一些大家很可能见过的论文塞进这个 self-play 的描述里呢？因为你可能在想，这看起来跟我读 AlphaGo、AlphaZero 那篇论文时所想的并不完全一样。所以那些传统的工作我们会称之为 symmetric self-play（对称 self-play）。在这种情况下，比如说在 AlphaGo 里，你训练模型的方式是：你有围棋 agent，你有围棋规则，你有棋盘。这很好，但那不是一个我可以交互的 RL 环境——我需要一个对手来对弈。所以在这个“生成 RL 任务”的部分，他们让一个旧版本的 agent 来扮演对手的角色。所以在这种情况下，生成任务，就是因为我把一个旧版本的自己放进去了，于是我现在就有了一个不错的 RL 任务——一个带对手的棋盘。所以这传统上会被称作 symmetric self-play，因为模型两次都在扮演同一个角色——一个围棋棋手。

[29:34]

More recently, however, uh in the LM space, there's been the rise of asymmetric selfplay. This actually hails from a lot of older work on control problems and things like this. But asymmetric selfplay, we instead more generally just have a model that I will call in this talk a conjecturer that will just generate entire RL tasks for the solver to then operate in. The solver is the equivalent of the agent here. So the conjecturer might come up with a coding problem and then come up with a bunch of unit tests and then it'll go into that environment to do a bunch of rollouts, get reward and train on that. Great. So so why do why am I excited about selfplay? Why do I think you should be excited about selfplay? So I guess this first point is the first point I have to go go in some some depth. So so in principle nothing bounds learning. And what do I mean by that? So if I take a bunch of demonstrations from humans and I train a model on that, I think it's clear that the model will never get better than those demonstrations. So the next step is okay, I'm going to create a bunch of environments out of the model learning those environments. That's regular RL. We have two problems there. One, if you ace all of the environments, you'll never get any better. Or the second problem is if I can't even get any reward in those environments, I will also never get any better. So selfplay on the other hand is going to say I'm going to keep on generating new learning signal with new tasks. learn it and just keep on improving hopefully forever. And indeed, we saw this was the case with two-player games like Go. It just kept on getting better beyond human uh performance and kept improving. So, the promise for LM is I can take some I can train on a bunch of human data. I get to like human level and then I can run loads of selfplay and go far beyond that and hopefully solve really interesting problems with with our models. But unfortunately, this is not how it works. So in practice if I run which we'll get into this talk if I run selfplayer for a long time it plateaus I the model stops improving at some point which is the exact same that happens when you run RL like as much as I'm trying to tell you there's a bunch of secret source going on like it doesn't actually play out.

不过最近在 LLM 领域，兴起了 asymmetric self-play（非对称 self-play）。这其实源自很多更早的、关于控制问题之类的工作。但非对称 self-play 里，我们更一般地说，就是有一个模型——在这个 talk 里我会把它叫做 conjecturer（猜想者/出题者）——它会直接生成一整个 RL 任务，让 solver（求解者）在里面去操作。这里的 solver 就相当于 agent。所以 conjecturer 可能会想出一个编程问题，然后再想出一堆单元测试，接着它就进到那个环境里去做一堆 rollout、拿 reward、然后在那上面训练。很好。那么，我为什么对 self-play 感到兴奋？我为什么觉得你也应该对 self-play 感到兴奋？我想第一个点是我得稍微展开讲一讲的。原则上，没有什么东西约束着学习的上限。我这话什么意思？如果我拿一堆人类的演示数据来训练模型，我想很清楚的是，模型永远不会变得比那些演示更好。那下一步是：好，我要用模型来造出一堆环境、让它学这些环境，这就是常规 RL。在那里我们有两个问题：一，如果你把所有环境都打满分，你就再也变不好了；或者第二个问题，如果我在那些环境里连一点 reward 都拿不到，我同样也永远变不好。而 self-play 则反过来说：我要不断用新任务生成新的学习信号，学会它，然后就这么一直改进下去，但愿是永远。而且我们确实看到，在像围棋这样的双人博弈里就是这样——它就是不断变好，超越了人类的水平，并持续提升。所以对 LLM 的许诺就是：我可以拿一些……我可以在一堆人类数据上训练，达到大概人类水平，然后我就能跑大量的 self-play、远远超越那个水平，但愿能用我们的模型解决真正有意思的问题。但不幸的是，事情并不是这么运作的。所以在实践中，如果我跑——我们这个 talk 会讲到——如果我把 self-play 跑很长时间，它会进入平台期，模型在某个点就停止改进了，这跟你跑 RL 时发生的事情一模一样。所以尽管我一直想告诉你里面有一堆秘诀（secret sauce）在起作用，但它实际上并没有那么顺利地兑现。

[31:33]

So basically this paper we try to figure out like why is this happening and then like do one step to solving the problem but by no mean by no means completely solve it. Okay. So to begin with we need to understand like the baseline LM selfplay algorithm pretty simple we're going to sample synthetic tasks from the conjecturer which is just our model conjecture and solver same model just given it two different names the model will then the solver then attempts them and we verify the correctness using some reward signal somehow like perhaps the conjectur wrote unit tests for us to check and then we're going to update the solver just on all the correct rollouts and then this is the key part the conjecturer gets updated ated on this reward which is zero if the prover if the solver could not solve the problem and one minus the solver rate otherwise okay what is that actually doing that is basically saying all the conjecturer must do is produce problems that are hard for the solver model and I think in principle that makes a lot of sense the idea is if the conjecturer can ace this I will keep on giving you problems at the frontier of your capability you will be able to solve them and learn from them and we'll just keep on expanding and expanding expanding and get better and better and Okay, so let's see how this recipe does. So we take in our paper like 3,000 formal math problems. So this is just uh in lean for you can write out the problem statement in this coding language in math. So you write out a math problem in this coding language. You can write the proof in the coding language. Then you can automatically verify if it's correct. So we take 3,000 problems and we run like our best RL baseline on it. And this is the amount of compute we put in here. And on the y axis we have how many problems you solve. And you can see it plateaus out and we fit a law and it asmmptotes at like 60%. And if we on the right hand side we're gonna say how much synthetic new task did we generate. RL generates no synthetic task. So by construction this stays at zero. Now I'm going to fill in the vanilla selfplayer with that solver rate reward. And I'm not going to show the left for now. We see as time goes on the conjecture gets better and better at its job. It keeps on generating more and more tasks on the frontier of the solver's capabilities which seems really good and yet these tasks are completely useless. The cell play does no better than regular RL.

所以基本上在这篇论文里，我们试图搞清楚为什么会发生这种情况，然后朝着解决这个问题迈出一步，但绝对、绝对没有把它彻底解决。好。那么首先我们需要理解一下基线的 LM self-play 算法，其实很简单：我们会从 conjecturer（猜题者）那里采样合成任务——这其实就是我们的模型，conjecturer（猜题者）和 solver（解题者）是同一个模型，只是给它取了两个不同的名字。然后 solver 会去尝试解这些题，我们用某种 reward 信号来验证答案是否正确——比如也许 conjecturer 给我们写了单元测试来检查。然后我们只在所有正确的 rollout 上更新 solver，接下来这是关键部分：conjecturer 会根据这样一个 reward 来更新——如果 solver 没能解出这道题，reward 就是 0；否则 reward 就是 1 减去 solver 的解题率（solve rate）。好，这实际上在干什么呢？它基本上是在说，conjecturer 唯一要做的就是产出对 solver 模型来说很难的题目。我觉得原则上这是很有道理的，思路是：如果 conjecturer 能做到这一点，我就会不断给你出处在你能力边界（frontier）上的题目，你将能够解出它们并从中学习，于是我们就不断地扩张、扩张、再扩张，越来越强、越来越强。好，那我们来看看这个配方效果如何。在我们的论文里，我们拿了大约 3000 道形式化数学题。这些题是用 Lean 写的，你可以用这门编程语言把题目陈述写出来，在数学里——你用这门编程语言写出一道数学题，你可以用这门编程语言写出证明，然后就能自动验证它是否正确。所以我们拿了 3000 道题，在上面跑我们最好的 RL 基线。这是我们投入的计算量（compute），纵轴是你解出了多少道题。你可以看到它趋于平稳，我们拟合了一条曲线，它渐近于大约 60%。右边这张图我们要看的是我们生成了多少新的合成任务。RL 不会生成任何合成任务，所以从构造上讲它一直保持为零。现在我要把带有那个 solver-rate reward 的原始（vanilla）self-play 填进来。左边那张图我暂时先不展示。我们看到，随着时间推移，conjecturer 在它的工作上越来越擅长，它不断生成越来越多处在 solver 能力边界上的任务，这看起来真的很好，然而这些任务却完全没用。self-play 的表现并不比普通 RL 更好。

[33:45]

So this is not very promising. So now we need to understand why. And here what I'm visualizing or I'm literally showing you is one of the problems the conjecture generates late on in training. And we don't really understand this. I've highlighted in blue that the conclusion to the statement in lean. And if anyone's using that this is horrific. This is an incredibly complicated, overly complex disaster of a statement. And so what is basically happening is we reward the conjecture for producing tricky problems. But the easiest way to produce tricky problems is produce these basically messy, artificially complex and elegant problems. It is the exact equivalent of if I wanted you to get like 50% solve rate problem, I could just give you like a three-page long high school calculus problem and you would make some little mistake somewhere. But that was a completely useless synthetic problem for like other tasks we care about in maths for example. Great. So how do we fix this in a minute because I've been talking too slowly. So we've diagnosed this problem. Here is like roughly at a high level how we try attempt to solve it. So there are two parts of our algorithm SGS self-guided selfplay. We're going to take the set of problems we cannot solve the 3,000 problems and we do two things. one for each of those problems we cannot solve we're going to get the conjecturer to produce a related problem to it. So once you prompt it to produce a synthetic problem that is related. So this way we're trying to ground the synthetic data distribution in a distribution of problems that we think is good at least. And next if you still just trained on the solvent rate reward you would eventually ignore this prior and still produce that junk. So we're going to introduce a new reward signal which is the model takes on a third role and it will literally judge it looks at synthetic problem and the target problem it came from and decide if these two things are actually related and not overly complex. So we call this third component a guide. Okay. So the algorithm looks like this. It's very similar. We for every target problem we haven't solved we'll sample a conjecture uh from the conjecture that is related to it. We then will attempt to solve them. And then what changed here is when we update the conjecturer, we now have this dual reward. One, we still want the problem to be tricky.

所以这并不是很有希望。那么现在我们需要搞清楚为什么。这里我可视化展示给你们看的，其实就是 conjecturer 在训练后期生成的一道题。我们并不真正理解它。我用蓝色高亮了 Lean 里这条陈述的结论部分。如果有人在用 Lean 的话，这玩意儿太可怕了。这是一条极其复杂、过度繁琐、堪称灾难的陈述。所以基本上发生的情况是：我们因为 conjecturer 产出刁钻的题目而奖励它，但产出刁钻题目最简单的办法，就是产出这种又乱、又人为复杂、看似精巧的题。这完全等价于：如果我想让你的解题率落在 50% 左右，我大可以丢给你一道三页长的高中微积分题，你总会在某个地方犯点小错。但对于我们在数学里真正关心的其他任务来说，这道合成题完全没用。好。那我们怎么修复这个问题呢？我得快点讲，因为我讲得太慢了。我们已经诊断出了这个问题。下面大致从高层讲讲我们尝试解决它的思路。我们的算法 SGS——self-guided self-play（自引导自博弈）——有两个部分。我们会拿出那些我们解不出来的题目，也就是那 3000 道题，然后做两件事。第一，对于每一道我们解不出来的题，我们让 conjecturer 产出一道与它相关的题。也就是说你 prompt 它去产出一道相关的合成题。通过这种方式，我们试图把合成数据的分布锚定（ground）在一个我们至少认为不错的题目分布上。其次，如果你仍然只在 solver-rate reward 上训练，最终它会无视这个先验（prior），照样产出那些垃圾。所以我们要引入一个新的 reward 信号：模型扮演第三个角色，它真的会去做评判——它看着合成题以及它所源自的目标题，判断这两者是否真的相关、是否没有过度复杂。我们把这第三个组件叫做 guide（引导者）。好。所以这个算法长这样，它非常相似。对于每一道我们还没解出来的目标题，我们会从 conjecturer 那里采样一道与之相关的猜想题。然后我们会去尝试解它们。这里改变的地方是：当我们更新 conjecturer 时，我们现在有了这个双重 reward。第一，我们仍然希望题目是刁钻的。

[35:49]

That is important. So we can get RL signal on it for the solder. And we'll multiply it by this guide score. Great. Okay. There's a bunch of kind of subtleties we cover in the paper that I will skip over because we don't have loads of time. If you want to talk about I'm going to say largeish scale RL infra, the academic size. That's what I spent most of my time doing. So I would like to talk about that, but there is not time. So let's just look at the head headline results here. Here is basically the same type of plot. I've put the RL baseline on here. Recall that like standard selfplay is exactly in line with that. We've also put parallel sampling down here just to show you that indeed RL at least gives you a boost. And I guess I wouldn't be here unless our method works better. So the method does work better. Um like ground how much better it's doing. We we we were using a 7 billion parameter model here and this is it like 670B like big brother and we spend eight times as much compute doing the selfplay at this you yeah we do eight times compute the selfplay but we get like to the ability of that larger model at least it's pass up for ability so you spend a lot more compute but we are able to get this like little 7B guy to do as well as the bigger model but very sadly you will notice like this is not at 100%. So like the work is is by far not done. The problems itself plays like you would just ate all the problems here and so there's a bunch of well there's lots of future work but luckily a PhD is very long so I'll be able to work on that. Um but yeah that's the summary. Awesome. Thank you so much Luke Bailey. Okay uh next one we have Arnab Matei. Is that the right way to say it? Matei. um who is a researcher currently at Giga one of YC's fastest growing companies I think market cap is like 400 million 300 million something like that now so really fast growing YC company uh PhD University of Washington focus on bandit learning um yeah please let's tell us about stream rag

这很重要，这样我们才能在它上面为 solver 拿到 RL 信号。然后我们会把它乘以这个 guide 分数。很好。好。论文里还有一堆细节上的微妙之处，我会跳过，因为我们时间不多。如果你想聊我会说是中等偏大规模（largeish scale）的 RL 基础设施——也就是学术界的规模——这是我大部分时间在做的事，所以我很想聊这个，但没时间了。那我们就直接看这里的头条结果（headline results）。这基本上是同一类型的图。我把 RL 基线放在了这里。回想一下，标准的 self-play 恰好和它重合。我们还把并行采样（parallel sampling）放在了下面，只是想让你看到，RL 至少确实带来了提升。我想我要不是因为我们的方法更好，也不会站在这里讲了。所以这个方法确实更好。嗯，要把它好到什么程度落到实处——我们这里用的是一个 70 亿（7B）参数的模型，而这个是它的「老大哥」、约 6700 亿（670B）的大模型，我们在这个 self-play 上花了八倍的计算量。是的，我们花了八倍计算量做 self-play，但我们至少在 pass@k（前 k 次通过率）这个能力上达到了那个更大模型的水平。所以你花了多得多的计算量，但我们能让这个小小的 7B 选手做得和那个更大的模型一样好。但很遗憾，你会注意到这并不是在 100%，所以这项工作远远没有完成。这些题它自己玩 self-play——你基本上会把这里所有的题都「吃光」，所以还有一大堆——嗯，还有很多后续工作要做，但幸运的是博士读起来很长，所以我有时间去做这些。嗯，但是的，这就是总结。太棒了，非常感谢 Luke Bailey。好，下一位我们请到 Arnob Matei。这样念对吗？Matei。嗯，他目前是 Giga 的研究员，Giga 是 YC 增长最快的公司之一，我记得市值大概是 4 亿、3 亿什么的，现在嘛，真的是一家增长非常快的 YC 公司。他是华盛顿大学（University of Washington）的博士，专注于 bandit learning（赌博机学习）。嗯，好，请给我们讲讲 stream RAG（流式 RAG）。

[37:51]

so um there's a paper by the group at meta and I kind of chose chose this paper to kind of maybe highlight some of the new emerging challenges that are coming up especially in a voice AI kind of setup. Um my goal with this talk is not more like about talking specific details about this paper but more like to highlight the good problems that they have identified and I feel like there's a lot of research that is to be done here and it also kind of closely mirrors what at least I do in my production uh setup like I look at these kind of problems I do the research and then I try to come up with a method that will work probably in production. So yeah, let's get started. This is a very classical setup where uh you probably ask a input question to an alm and it gives an output. And if you remember maybe from 2023 maybe there was a lot of hallucinations but especially like say around citations and all but over time maybe the hallucinations went down and a big role was uh rag like you kind of give the input query to a rag system. it kind of goes and figures out relevant information that needs to be provided to an LLM and then the LM probably gives you an output which is hopefully not hallucinated. Now uh a lot of voice AI uh startups are also coming up and a natural expectation with the voice AI is that okay you're having like a conversation like oh you can ask oh what's the weather like and the agent would reply like hey the weather currently is like 22°C and so on and maybe you can ask a follow-up question so it's more like conversational in nature and so even here as well you would like the output to We like there shouldn't be any hallucination. Especially in voice, we care about this even more because from a human perspective, it's difficult to kind of actively catch hallucinations when you're listening to it compared to like when you're reading it over text. So one might ask, okay, what's the issue with just using rag here? like can't you just take the input query take apply rag give the relevant information to the voice agent and get the output the issue is that rag would add a lot of latency um like for example if I ask a voice agent some question and the voice agent takes 10 seconds to reply that's not at all natural especially if you want to have some sort of natural conversation so that's where this paper kind of looks at A very clever idea I would say uh which is like instead of like waiting for the question to end and then activate your rag pipeline you kind of start analyzing the words that are being spoken by the user and somehow figure out a way to run the rag system while the question is being spoken. Like for example uh like you might ask like hey what's the weather today like I'm I want to decide based on that whether I want to go out or not. The main question is in the first part. So the second part of your question might be irrelevant. So we want um some sort of uh mechanism via which we can figure out okay uh when to call this rack system and appropriately get the right uh information.

好的，嗯，有一篇 Meta 团队的论文，我之所以选这篇论文，是想借此凸显一些新出现的挑战，尤其是在语音 AI（voice AI）这种场景下冒出来的挑战。我这次分享的目标，与其说是讲这篇论文的具体细节，不如说是凸显他们识别出来的那些好问题（good problems）。我觉得这里有大量研究有待去做，而且它也相当贴近至少我自己在生产环境（production）里做的事——我会去看这类问题，做研究，然后试着想出一个大概能在生产环境里奏效的方法。那好，我们开始吧。这是一个非常经典的设置：你大概会向一个 LLM 提一个输入问题，它给出一个输出。如果你还记得，也许是在 2023 年，那时候有大量幻觉（hallucination），尤其是在引用之类的地方，但随着时间推移，幻觉也许减少了，其中一个很大的功臣就是 RAG——你把输入查询（query）交给一个 RAG 系统，它会去找出需要提供给 LLM 的相关信息，然后 LLM 大概就给你一个但愿没有幻觉的输出。现在，很多语音 AI 创业公司也涌现出来，对语音 AI 一个很自然的期待是：好，你像在对话一样——比如你可以问「哦，今天天气怎么样」，agent 会回答「嘿，现在的天气大概是 22 摄氏度」等等，也许你还可以追问，所以它本质上更偏对话式（conversational）。所以即便在这里，你也希望输出——我们希望这里不应该有任何幻觉。尤其在语音里，我们更加在乎这一点，因为从人的角度看，当你在听的时候，相比于在文字里阅读，主动抓出幻觉是更困难的。所以有人可能会问，好，那这里直接用 RAG 有什么问题呢？难道你不能就拿输入查询、套上 RAG、把相关信息给语音 agent、然后拿到输出吗？问题在于 RAG 会引入大量延迟（latency）。比如说，如果我问语音 agent 一个问题，而语音 agent 要花 10 秒才回答，那一点都不自然，尤其是当你想进行某种自然对话时。所以这正是这篇论文切入的地方，我会说这是一个非常巧妙的想法：与其等问题说完再去激活你的 RAG 流水线，你不如开始分析用户正在说出的词语，并设法在问题还在被说出的过程中就去运行 RAG 系统。比如你可能会问「嘿，今天天气怎么样，我想根据它来决定要不要出门」。主要的问题在前半句，所以你问题的后半句可能是无关的。所以我们想要某种机制，借此搞清楚：好，什么时候去调用这个 RAG 系统，并恰当地拿到正确的信息。

[41:43]

So this particular paper focuses on two approaches. Uh the first one is fairly simple. Um so it's called fixed rag uh fixed interval streaming rag. So the idea is like you divide the audio into certain blocks and after each block arrives you can like run rag on every block. So uh so after when the block B arrives you run your rag get the results for the rag RB and you keep on doing till this uh till the end probably. Now the question the main question here is like which block to consider because you ideally cannot like wait the entire goal was you cannot wait till the end and then run the rag. So what do you do? So the main uh maybe idea here is that rack pipeline has lot of mini components. So maybe some of the components are like easy to run or like more faster to run. So for example uh you can kind of get some documents very quickly and you can say okay for the entire query what were the top documents and for the intermediate query what were the top documents and are they matching or not? This is just one of the ideas which is from the paper. Uh and then based on that you can decide okay should I go ahead with the intermediate query and uh just do the entire rack pipeline on that. Um so the thing I want to stress is not the method per se but the point that okay when you are getting this uh input in chunks at what point can you stop and say that okay like this chunk is like super relevant for me. Uh so this is like an active question I would say like how would you do that? This uh paper does it in a very simple manner which is just to maybe look at the initial path of the rack pipeline and if they kind of match like if the end path matches the intermediate part then you go ahead with the intermediate and let the full rack pipeline complete. Another approach could be like you you can probably fine-tune a model to kind of trigger on its own like when to call the rack because in the previous approach you were calling rag on every single chunk. So maybe that's computationally wasteful. So what you can probably do is when a particular chunk arrives you can maybe fine-tune some model and ask it to decide whether uh this chunk uh is like in critical new information and you should generate a new query or the query that you generated based on the past chunks are good enough for you to just answer the question. And uh based on that you can generate the final audio.

所以这篇具体的论文聚焦于两种方法。嗯，第一种相当简单。它叫 fixed RAG——固定间隔的流式 RAG（fixed interval streaming RAG）。思路是：你把音频切分成若干块（block），每一块到达之后，你就可以在每一块上运行 RAG。所以当第 B 块到达时，你就跑你的 RAG，拿到这块的 RAG 结果 RB，然后你一直这么做，大概直到结束。现在这里主要的问题是：该考虑哪一块？因为理想情况下你不能一直等——整个目标就是你不能等到最后再去跑 RAG。那你怎么办呢？这里主要的、也许是核心的想法是：RAG 流水线有很多小组件，所以也许有些组件很容易跑、或者跑得更快。比如，你可以很快地拿到一些文档，然后你可以说：好，对于整个查询，排名靠前的文档是哪些；对于中间这个（还没说完的）查询，排名靠前的文档又是哪些；它们匹配不匹配？这只是论文里的一个想法。然后基于此你可以决定：好，我该不该就拿这个中间查询往下走、在它上面跑完整条 RAG 流水线。嗯，我想强调的不是方法本身，而是这一点：当你以分块（chunk）的形式拿到这个输入时，在哪个时间点你可以停下来说「好，这一块对我来说超级相关」。所以我会说这是一个很活跃的开放问题：你要怎么做到这一点？这篇论文用一种非常简单的方式来做，就是去看一下 RAG 流水线初始那段的结果，如果它们大致匹配——如果（完整查询的）末态结果和中间这段的结果匹配——那你就拿中间这个查询往下走，让完整的 RAG 流水线跑完。另一种方法可能是：你大概可以 fine-tune 一个模型，让它自己来触发——决定何时去调用 RAG。因为在前一种方法里，你是在每一个 chunk 上都调用 RAG，那也许在计算上很浪费。所以你大概可以这么做：当某个特定的 chunk 到达时，你也许可以 fine-tune 某个模型，让它来判断这个 chunk 是不是关键的新信息、你是否应该生成一个新查询，还是说你基于过去那些 chunk 已经生成的查询已经足够好、足以让你回答问题了。然后基于此你就可以生成最终的音频。

[44:44]

Yeah. So in in the paper they kind of describe a post- training pipeline. What they do is like they kind of uh for the partial uh spoken uh question they kind of generate some pseudo queries using some LLM and then uh they run a rag on that and they look at the retrieved documents and based on the retrieved documents they kind of decide okay is this uh partial query like uh something new or is it already like we already have the useful material. So in this okay um in this paper essentially they are kind of basing their decision based on the retrieval quality of the partial question so far. That's that would be my takeaway. But maybe there are different ways in which you can do this assessment. Maybe you can look into the semantic of the question so far like is the partial question so far good enough for me to answer this question just by looking at the question. No no no need to do this entire lag pipeline. So there are my my point is like you need not uh this need not be the only way there might be so many different ways and that's where the research maybe uh is required like while a user is speaking their question how do we like on like why instead of waiting till the end how do we like figure out okay this part of that question is good enough for us to go and do the retrieval yeah so that that's what they do probably I'll quickly give a glimpse of the results from the paper. Um this paper is a year old. So they were like yeah looking at some smaller open source models. Um so they were they kind of considered the rag benchmark converted into audio and uh showed that the latency kind of decreases for the synthetic data sets by 0.5 seconds and for human data sets like human spoken data sets by uh almost like 1.5 seconds and uh the accuracy uh comparison like uh if there was rag uh after the final query and streaming rags it kind of remains the same like um yeah so yeah so that's what the paper is about so like the key takeaway is like there are some interesting small problems here like but if you can crack the small problems it can lead to huge gains in the production yeah thank you okay next up we have Robert George. Um, come on up. Uh, thirdyear PhD at Caltech.

是的。所以在这篇论文里，他们描述了一条后训练（post-training）流水线。他们做的是：对于这部分说出来的、不完整的问题，他们用某个 LLM 生成一些伪查询（pseudo queries），然后在这些伪查询上跑 RAG，看看检索（retrieval）回来的文档，再基于检索到的文档来判断：好，这个不完整的查询是不是某种新东西，还是说我们已经有了有用的材料了。所以在这篇论文里，本质上他们是基于「到目前为止这个不完整问题的检索质量」来做决策的。这就是我会带走的要点。但也许还有别的方式来做这种评估。也许你可以去看到目前为止这个问题的语义——比如，仅凭看这个问题，到目前为止这个不完整的问题是否已经足够好、足以让我回答这个问题了，根本不需要去跑整条 RAG 流水线。所以——我的意思是，这不一定是唯一的方式，可能有很多很多不同的方式，而这正是也许需要做研究的地方：当用户正在说出他们的问题时，我们要怎么做到——为什么不等到最后，而是怎么搞清楚「问题的这一部分已经足够好、足以让我们去做检索了」。是的，所以这大概就是他们做的事。我快速给大家瞥一眼论文里的结果。嗯，这篇论文是一年前的，所以他们当时用的是一些较小的开源模型。嗯，他们把 RAG 的 benchmark 转换成了音频，结果显示：对于合成数据集，延迟下降了约 0.5 秒；对于人类数据集、也就是人类说出来的数据集，延迟下降了将近 1.5 秒；而在准确率（accuracy）对比上，比较「在最终查询之后做 RAG」和流式 RAG，二者基本保持一致。嗯，是的，所以这就是这篇论文讲的东西。所以关键要点是：这里有一些有意思的小问题，但如果你能攻克这些小问题，它在生产环境里能带来巨大的收益。好，谢谢。好，下一位我们请到 Robert George。嗯，上来吧。他是 Caltech（加州理工）的三年级博士。

[47:31]

Yes.

是的。

[47:31]

Okay. My brother got his PhD at Caltech.

好。我哥哥在 Caltech 拿的博士学位。

[47:34]

Um, and, uh, you work on AI for math and science.

嗯，然后，呃，你做的是 AI for math and science（用 AI 做数学和科学）。

[47:38]

Yeah.

对。

[47:38]

Um, and what are you going to tell us about?

嗯，那你打算给我们讲点什么？

[47:40]

I'm going to tell us about lean. Basically, Luke already told a little bit, but I want to go more in depth. So, I'm going to be talking about lean and what I think is this new era of verified intelligence. Um so let's get into it. So again there's bunch of breakthroughs in the past like couple of weeks itself like first I want to go back like two years before you know like we said that IMO open and even deepine actually at the 2024 IMO got the gold medal then you know there's this very famous problem list which is very famous right now where people are trying to kind of solve new open unsolved odos problems and you know you can see that it's keep on keep on increasing with the new models from like open AAI depend and all. Um just two weeks ago OpenAI claimed to solve another big breakthrough 80-year-old Odosh problems. You know Terry Tower was has this promotional video at OpenAI which he showed really well about these kind of things. And then last week Deepmind released something also solving bunch of new not only ODOS problems but problems in like other different fields right but this paper is cool because they also use some kind of formal verification in the loop. So I want to say that you know we all took like high school calculus we took undergrad college math courses and all this you know informal math is very very flexible right um your your professor say sometimes you know proof by QED like you know sometimes it's like proof by intimidation or something that right there many of the steps are not fully written down but this is where I believe that you know formal world is like you have to be fully explicit right and I'll talk and introduce the language lean again before lean In past couple of hundred years, you know, people have been doing formal math a lot, but you know, lean has just kind of this really good design language just kind of taken off, right? So again, first thing is it's very easy to check if a proof is correct or not. You cannot fool this theorem prover. Secondly, uh it's scalable. Again, there's bunch of issues over there, but I can talk more about that soon. So before that I just want to give you like a precursor. So people do know about like um there was a thing previously like in the 1990s even right now actually 2020s and all this is there's this thing called automatic theorem provers which are basically like SMT solvers um they are basically um minimal effort from humans you know but they're very limited expressivity in what type of mathematics they can encode in some sense right and on the far right hand side you can see interactive theorem provers like lean rogue Isabel which are very have a much more stricter like expressive logic system. So it's based at least some of them are based on dependent type theory but much more effort from humans to kind of write down these proofs right like if you're talking about like 10 years people have been contributing to this very famous library called math lab in lean um there's a lot of human effort to kind of pick premises and all this and again we all know how good LLMs are right now at kind of combining with these kind of theorem provers to kind of do proof checking for like research level math right and it's so much news that I you know if If I go on Twitter right now, I can open up a bunch of posts saying how much progress past couple of hour probably in some sense right so first

我打算给大家讲 Lean。其实 Luke 刚才已经讲了一点，但我想讲得更深入些。所以我要讲 Lean，以及我认为的这个 verified intelligence（可验证智能）的新时代。嗯，那我们就开始吧。还是那句话，过去这几周里有一大批突破，先说，我想先回到大概两年前——你知道，我们之前说过，IMO 上，OpenAI、甚至 DeepMind，其实在 2024 年 IMO 上拿到了金牌；然后有一份现在非常有名的问题清单，大家在尝试解决一些此前未解的开放性 Erdős 问题（Erdős problems），你能看到随着 OpenAI、DeepMind 等等的新模型出来，这个清单一直在不断增长。嗯，就在两周前，OpenAI 宣称又攻克了一个大突破——一个有 80 年历史的 Erdős 问题。你知道，Terry Tao（陶哲轩）在 OpenAI 那边有个宣传视频，他把这类事情讲得非常好。然后上周 DeepMind 也发布了一些成果，不仅解决了一批新的 Erdős 问题，还解决了其他不同领域里的问题；但这篇论文很酷，因为他们还在 loop 里用了某种 formal verification（形式化验证）。所以我想说，你知道，我们都学过高中微积分，上过本科大学的数学课，所有这些非形式化的数学其实非常非常灵活，对吧——你的教授有时会说，你知道，proof by QED（证毕），有时候像是 proof by intimidation（靠唬人来证明）之类的，很多步骤其实并没有完整写出来；而我认为这正是 formal world（形式化世界）的不同之处，在那里你必须做到完全显式（fully explicit），对吧。我会讲一讲、并再次介绍 Lean 这门语言。在 Lean 之前，过去几百年里，你知道，人们一直在大量地做形式化数学，但 Lean 恰恰是这样一门设计得非常好的语言，一下子就火起来了，对吧。所以，还是那句话，第一点是，它非常容易检验一个证明对不对。你没法骗过这个 theorem prover（定理证明器）。其次，呃，它是 scalable（可扩展）的。当然，这里头有一堆问题，但我待会儿可以再多讲。在那之前我只想给你一个铺垫。大家确实都知道，比如，以前——上世纪 90 年代，乃至现在、其实到 2020 年代——有一个东西叫 automatic theorem provers（自动定理证明器），它们基本上就像 SMT solvers，嗯，它们基本上需要人投入极少的精力，你知道，但从某种意义上说，它们在能编码哪类数学方面表达力非常有限，对吧；而在最右边那一端，你能看到 interactive theorem provers（交互式定理证明器），像 Lean、Rocq、Isabelle，它们有一套严格得多、表达力强得多的逻辑系统。所以它是基于——至少其中一些是基于 dependent type theory（依赖类型论），但需要人投入多得多的精力来写出这些证明，对吧；比如，谈到这个，十年来人们一直在为 Lean 里一个非常有名的库做贡献，叫 Mathlib，嗯，要挑选前提（premises）等等需要大量的人力投入；而且我们都知道现在的 LLM 有多厉害，对吧，把它们和这类 theorem prover 结合起来，去做研究级别数学的证明检验，对吧。这方面的新闻太多了，我是说，要是我现在打开 Twitter，我能翻出一大堆帖子，从某种意义上说，讲过去这几个小时里大概又有了多少进展，对吧。所以首先——

[51:00]

thing is I want to introduce why leen you know Luke mentioned this formal very messy language but I actually think it's a very beautiful language again one can argue no but um it's a very fast language again it's also people think of it as only a theorem prover but it's actually also a functional programming language right you can use it as a programming language itself so it's compile checking Um it's very good unified. So this is what like the proofs and programs. Um you can do like meta programming, you can do macros, custom automation, you know, you can I've seen people trying to even create like games on with using lean, right? It's actually super cool. So lean has something called the foreign face interface where you can do like external library bindings like you can do on the CUDA or something that um I want to point out the math liy. I think that is the coolest biggest formalized math library out there. um I forgot how many number of lines probably at least in a million or so but all of these are really high quality math right from like say topology to algebraic geometry and all this and again it's an interactive theorem prover so you always have to you know the human can sometimes be in a loop but it is also a very scalable language because you know not only frontier labs are pushing a lot of money into it and also the world is but um there's more data being generated either through synthetic or like a lot of people like even myself I do manual formalizations. Um so just very short I don't want to take time but this is how a simple lean code looks like like in VS code you have like an info goal view which shows like what are the current kind of sub goals. So goal is basically like what are you trying to prove at this step. So the first theorem is like you're basically showing associivity of addition of like natural numbers right like a plus b plus c is equal to a plus c plus b and each line in a proof is usually called like a tactic. So usually when people talk about like proof search they mean like you know you can search over this kind of tactic space there are methods where you do foolproof generation but you know these are the two different axis. So this is how lean code looks. It's not as bad as it seems.

第一点是，我想介绍一下为什么用 Lean。你知道，Luke 提到这是一门很乱的形式化语言，但我其实觉得它是一门非常漂亮的语言——当然有人会说不是，但是，嗯，它是一门非常快的语言；还有，人们往往只把它当成一个 theorem prover，但它其实也是一门 functional programming language（函数式编程语言），对吧，你可以把它当编程语言本身来用，所以它是编译期检查（compile checking）。嗯，它非常好地把东西统一了起来。这就是所谓的「证明即程序」（proofs and programs）。嗯，你可以做 meta programming（元编程），可以做宏（macros）、自定义自动化，你知道，我甚至见过有人尝试用 Lean 来做游戏，对吧，真的超酷。所以 Lean 有个东西叫 foreign function interface（外部函数接口），你可以用它做外部库绑定，比如可以绑到 CUDA 之类的东西上。嗯，我想指出 Mathlib，我认为那是现存最酷、最大的形式化数学库。嗯，我忘了它有多少行代码了，大概至少有一百万行左右吧，但这些全都是质量非常高的数学，对吧，从拓扑学（topology）到代数几何（algebraic geometry）等等；而且，再说一次，它是个 interactive theorem prover，所以你总是需要——你知道，有时候得有人在 loop 里；但它同时也是一门非常 scalable 的语言，因为，你知道，不仅前沿实验室（frontier labs）往里砸了很多钱，全世界也都在投，而且嗯——还有越来越多的数据被生成出来，要么是通过合成（synthetic），要么是很多人——比如我自己，我会做手工形式化（manual formalizations）。嗯，所以非常简短地——我不想占太多时间——这就是一段简单的 Lean 代码长什么样：在 VS Code 里你会有一个 info goal 视图（信息目标视图），它会显示当前有哪些子目标（sub goals）。所谓 goal（目标）基本上就是你在这一步想要证明的东西。第一个 theorem 基本上是要你证明自然数加法的结合律（associativity），对吧，就是 a 加 b 加 c 等于 a 加 c 加 b；而证明里的每一行通常叫做一个 tactic（策略）。所以通常当人们谈到 proof search（证明搜索）时，他们指的就是，你知道，你可以在这种 tactic 空间里搜索；也有一些方法是做整证生成（full-proof generation），但你知道，这是两个不同的维度（axis）。所以这就是 Lean 代码长的样子，没有看上去那么糟糕。

[52:59]

It's a steep learning curve. I think it's much better than even C++ in some sense like learning but um you at least get really um at least for me I get very happy when I see oh I've fully proven this theorem right there's no assumptions like I cannot like handwave or fool the lean kernel basically like you have to be fully 100% sure um now I want to talk about the formalization breakthroughs right I talked about informal but actually the first book was actually in 2020 Ilia and uh Stan was from open they released something called GPDF um this was first generative language model for automatic theorem proving mini F2F is just like a Olympia level kind of competition but you see the amount of progress like it's kind of exponential right like from open source models big players in China in the US Canada like across the entire world um last year's IMO you know again deep mind claimed to not have used lean I if you see the open air solutions some kind of DSL of lean kind of stuff in the solutions um but even Steve prover from China also got the IMO gold And then obviously there's a bunch of like axi improver there's harmonic AI like they got recently in the pakam they got all the 12 problems solved most of the odos problems now when people are saying they kind of um claim to have a solution using AI they also prove it um using like say Aristotle from harmonic um and then another amazing work was kind of this fields metal work from math inc and obviously the Google Google deep mind stuff in some sense right and again I love the fact that you know everyone's is talking about math and all but you know for me personally there's also these two other bubbles right like there's also code now one can argue what is program verification as well you know bugs are really expensive it's like a huge trillion dollar industry wide coding is all of a sudden really great like everyone is generating but we I want code that needs guarantees right I think that's like something which I'm very interested in and also AI for science matters like there's uh repro uh reproducibility and all this kind of stuff so I want to go through this really fast but um LMS can write code but can they prove it's correct um you know there's scale of generated code there's that of bugs uh how can you kind of capture human intent and the verification language and again in short I want to talk about like program verification is like there's these three concepts where humans actually always have some kind of like specification about like what they want their code to do so a proof is basically saying that the code kind of satisfies that specification um there's this work which I introduced called bridge where you can use this lean as a functions programming language to kind of elicitate the llms to kind of prove this kind of code better. Um so I like this code from max tagm where they say that we should shift from actually wide coding to like very coding right. Um verifiable coding will be like definitely I think a much more better way. Um and you should contribute to CS lab. This is started from Clark Barry's group at Stanford. There's bunch of from deep mind and all. But if you want to contribute to CS concepts and all, you should definitely contribute with CSL. Um I want to go through quickly just about one last work about uh torch which I recently introduced.

它的学习曲线很陡。从某种意义上说，我觉得学起来它甚至比 C++ 还好上手，但嗯，你至少能得到——至少对我来说，当我看到「噢，我已经把这个 theorem 完整证出来了」的时候我会非常开心，对吧，没有任何假设，我没法靠挥挥手蒙混（handwave），也骗不过 Lean kernel（Lean 内核），基本上你必须百分之百完全确定。嗯，现在我想谈谈形式化方面的突破，对吧。我刚才讲的是非形式化的，但其实第一本——第一项工作其实是在 2020 年，Ilya 和，呃，Stan，他们是 OpenAI 的，他们发布了一个叫 GPT-f 的东西，嗯，这是第一个用于自动定理证明的生成式语言模型；miniF2F 就像是一个奥林匹克级别（Olympiad level）的竞赛集，但你能看到进展之大——可以说是指数级的，对吧，从开源模型，到中国、美国、加拿大乃至全世界各地的大玩家。嗯，去年的 IMO，你知道，DeepMind 又一次声称没有用 Lean，但要是你去看 OpenAI 的解答，里头有某种 Lean 的 DSL 之类的东西；不过即便是中国的 Seed Prover 也拿到了 IMO 金牌。然后显然还有一堆，比如 AxiomProver，还有 Harmonic AI，他们最近在 Putnam（普特南竞赛）上把 12 道题全解出来了，现在大多数 Erdős 问题——当人们说他们声称用 AI 给出了某个解时，他们也会去证明它，嗯，用的是比如 Harmonic 的 Aristotle。嗯，然后另一项了不起的工作是 Math Inc 那项类似菲尔兹奖级别（Fields Medal）的工作，当然还有 Google、Google DeepMind 的那些东西，从某种意义上说，对吧。还有，我很喜欢这一点：你知道，大家都在谈数学等等，但对我个人而言，还有另外两个领域（bubble），对吧——还有代码，现在有人会问 program verification（程序验证）又算什么？你知道，bug 真的非常昂贵，这是个上万亿美元的庞大产业；vibe coding（凭感觉写代码）突然变得非常好用，对吧，人人都在生成代码，但我想要的是需要保证（guarantees）的代码，对吧，我觉得这是我非常感兴趣的事情。还有 AI for science（用 AI 做科学）也很重要，比如有可复现性（reproducibility）之类的问题。所以我想很快地过一下这个——嗯，LLM 能写代码，但它们能证明代码是正确的吗？你知道，生成的代码规模摆在那儿，bug 的规模也摆在那儿；你怎么才能在验证语言里捕捉到人的意图（human intent）呢？还是简短点说，我想谈谈 program verification，它有这三个概念：人类其实总是对自己想让代码做什么有某种规约（specification），所以一个 proof 基本上就是在说：这段代码满足了那个 specification。嗯，有一项工作我介绍过，叫 Verina——你可以把 Lean 当作函数式编程语言来用，去更好地引导（elicit）LLM 证明这类代码。嗯，所以我喜欢 Max Tegmark 的这句话，他说我们应该从 vibe coding 转向 verified coding（可验证地写代码），对吧。嗯，verifiable coding（可验证编程）我觉得肯定会是一种好得多的方式。嗯，你应该为 CSLib 做贡献，它源自斯坦福 Clark Barrett 的团队，还有一帮来自 DeepMind 等等的人。但如果你想为各种 CS 概念做贡献，你绝对应该用 CSLib 来贡献。嗯，我想很快地再过一下最后一项工作，是关于 torch 的，我最近介绍过它。

[56:05]

This is the first unified framework for actually writing down neural networks in lean. So you have this kind of full like pytor style like tensor system. Everything compiles down to a shared intermediate representation. You can kind of prove properties of specs like I can show you some examples. You have like verified floatingoint arithmetic. you can kind of do even like neural network verification like certified robustness kind of stuff right and again there's bunch of applications which I show but I think one cool thing that I'll show this and the next slide is that you know you can show that the flash attention is equal to like at least in the spec level is equal to the uh normal standard attention right again we don't worry about like IO and all this processing also you can a very standard fact is like the attention mechanism is permutation in if you don't have position like curtains so I actually kind of trained a GP2 style like Karpathi's thing in torching itself fully natively in lean right and you can kind of prove properties about it and all this um one thing I think I can end with this slide is that thinking machine lab last year released something about um this kind of non-determinism even when you have like temperature zero um when you put it into your LM inference I actually kind of formalize this whole system in torch lean all the way down to like almost a GPU kind of like small cuda level kernel verification because the whole goal in this blog was saying that the tiny floatingoint arithmetics can flip the final argmax in the kind of the batch thing. So again there's a blog you can check it out on my website but uh I was very very cool that you can kind of do real life software verification um in some sense and uh again there's a bunch of different slides I have but I kind of want to end on this note just for the sake of time but you know I see a future where uh science like even code can be formally verified through a lot of building blocks which people are putting a lot of effort in and this is one of the examples that I think is like my fuse matter like kind of contribution to the ammo wall in some sense.

这是第一个用来在 Lean 里真正把神经网络写出来的统一框架。所以你能拿到一套完整的、类似 PyTorch 风格的 tensor 系统，所有东西都会编译到一个共享的中间表示（intermediate representation）。你可以去证明各种 spec 的性质，我可以给你看几个例子。比如你有经过验证的浮点运算（verified floating-point arithmetic），你甚至可以做神经网络验证（neural network verification），比如认证鲁棒性（certified robustness）这类东西。我展示了一大堆应用，但我觉得这一页和下一页里有个很酷的点：你可以证明 flash attention 等价于——至少在 spec 层面上等价于——普通的标准 attention，当然我们这里不去操心 IO 和那些处理细节。还有一个非常标准的事实：如果你不加位置编码（position），attention 机制是排列不变的（permutation invariant）。所以我其实在 Lean 里完全原生地训练了一个 GPT-2 风格的模型，就是 Karpathy 那套东西，直接在 torch 里跑，然后你可以证明关于它的各种性质等等。我想用这一页来收尾：Thinking Machines Lab 去年发布过一篇博客，讲的是即使你把 temperature 设成 0、放进你的 LLM inference 里，仍然会有这种非确定性（non-determinism）。我其实把这整套系统都在 torch Lean 里形式化了，一路往下做到几乎是 GPU 那种小型 CUDA 级别的 kernel 验证。因为这篇博客的整个核心是说，微小的浮点运算可以在 batch 里翻转最终的 argmax 结果。这篇博客你可以在我网站上看，我觉得非常非常酷的一点是，你在某种意义上真的可以做现实世界的软件验证（software verification）。我还有一堆别的 slide，但为了时间，我想就停在这个点上。我看到一个未来：科学，甚至代码，都能通过大量基础构件被形式化验证，这些构件正有很多人投入精力去做。这就是其中一个例子，算是我对这堵 formal/AI 大墙在某种意义上的微薄贡献吧。

[58:05]

All right, great job. Okay, for our last presentation, it's going to be the antithesis of lean and token maxing to the max. Um, very excited uh to introduce Luke Orthwine, his close friend. um we're friends in in uh in Woodside together. Um and did his uh CS degree at Harvard, then ran growth at WeChatad from 2012 till 2015. Uh which is why we call him the lion of Hong Kong. Um and now has been running his startup channel AI and is probably the most unhinged technical CEO that I know. So

好的，干得漂亮。好，我们最后一场分享，将是 Lean 的对立面，是把 token maxing 推到极致。我非常激动地介绍 Luke Orthwine，他是我的好朋友。我们在 Woodside 是朋友。他在 Harvard 拿了 CS 学位，然后从 2012 到 2015 年在微信广告（WeChat ad）负责增长（growth），所以我们叫他「香港之狮」。现在他在做自己的创业公司 Channel AI，他大概是我认识的最不按常理出牌的技术型 CEO。所以——

[58:52]

thank you Francois. Um yeah so the the idea behind this talk is sort of um what we uh at channel have done to try to take the the best advantage of sort of rethinking how you should do software engineering in this world of agentic programming assistance cla etc. Um and really you know the the ways in which uh I think many assumptions about what good programming is are now sort of the opposite of what you should be doing. Uh and these are sort of what we have have worked through ourselves and found very useful and wanted to share with all you guys to give some context. channel AI. We're a consumer entertainment uh AI business. Uh and we're really focused on the problem of automating as much as possible of not just software development but content development. How do you really create like an endto-end system uh that is pure AI that uh gets people to pay you money uh and stay engaged etc. Uh we've had pretty solid success with that so far. Um, and it's inspired us to think in our own workflows, how can we just sort of max this and and be as far ahead of the curve as possible. Um, and chess is an imperfect analogy to what programming used to be like, but I think the ways that it uh is useful is like yeah, maybe programming before you wanted to be very linear. You wanted to predict the future. You wanted to design very thoughtfully systems that would be like robust and work well uh and and be correct. Um, and even if you're trying to do something sloppily, it's still like a single threaded process where you only are worrying at a given moment about what's in front of you. Um, and to me, I'm a big fan of real-time strategy games using Agentic systems. Feels exactly like playing real-time strategy games to me. Uh, and there are a lot of properties of those games that are very different from chess. Um, one thing and especially if you look at like highle play uh there is no single aspect that you can do perfectly and like succeed. You have to be balancing many different things at once. You have to always have your economy running, your production running, your units doing something productive. You need to be engaging. And so this notion of like how do you maximally parallelize both what your systems are doing but also your attention so that you are adding the corrective uh feedback that's necessary as you learn new things as the map is exposed all this kind of stuff. Um anyway this to me feels like exactly what like coding with agents is like um and this what we'll talk about. Um so in terms of like tools we've built just to like ground this in a very simple thing. This is the LW stuff is just like our linear work trees. Um, a lot of people early on started using realizing how useful git work trees are when you do coding development. Having separate uh I assume everybody kind of knows where they are, but in case not like you know it was fine to have one repo on your machine when you were the only one doing development. Now you need to have like lots and lots of repos on your machine all doing development in parallel. Uh all compiling separately and like not stepping on each other's toes. Um and so the combination of like uh using work trees, using task management software, uh having the actual work itself be portable, um which is what the team bit comes in, and then like sticking in autonomous agents, one or many different ones on a given workflow. Um the way

谢谢 Francois。是这样，这次分享背后的想法，大致是我们在 Channel 所做的事情——也就是在这个 agentic 编程助手（Claude 等等）的世界里，怎么彻底重新思考软件工程该怎么做。我觉得，很多关于「什么是好的编程」的假设，现在恰恰应该反过来。这些是我们自己摸索出来、并觉得非常有用的东西，想分享给你们。先交代点背景：Channel AI 是一家做消费级娱乐（consumer entertainment）的 AI 公司。我们真正聚焦的问题是，尽可能自动化的不只是软件开发，还有内容开发——你怎么真正做出一套端到端、纯 AI 的系统，让人愿意给你付钱、并持续保持参与等等。到目前为止我们做得还挺扎实的。这也启发我们去想，在自己的工作流里，怎么把这件事推到极致、尽可能走在曲线前面。下象棋（chess）是个不完美的类比，用来比喻过去的编程，但我觉得它有用的地方在于：以前的编程，你想做得很线性，你想预测未来，你想非常深思熟虑地设计出那种鲁棒、能良好运行、且正确的系统。哪怕你想随便糙一点地做，它本质上仍然是一个单线程的过程，你在任一时刻只需要操心眼前这一件事。而对我来说，我很喜欢即时战略游戏（real-time strategy games，RTS），用 agentic 系统的感觉，对我来说就完全像在玩 RTS。这类游戏有很多和象棋非常不一样的特性。有一点，尤其是看高水平对局，没有任何单一方面是你做到完美就能赢的，你必须同时平衡很多不同的东西：你得让经济一直运转、生产一直运转、单位一直在做有产出的事，你得一直在交战。所以「怎么最大化地并行——既并行你的系统在做的事，也并行你的注意力，以便随着学到新东西、随着地图被揭开等等，及时补上必要的纠正性反馈」，这种思路对我来说就完全是 RTS 的感觉，也是我们接下来要讲的。说到工具，我们造了一些东西，先用一个很简单的例子来落地一下。这个 LW 的东西就是我们的 linear work trees（linear 工作树）。很多人早期就开始用、并意识到 git work trees 在做编程开发时有多有用。我假设大家大概都知道——万一不知道：当你是唯一一个在开发的人时，机器上只有一个 repo 是没问题的；但现在你需要机器上有非常非常多的 repo，全都在并行开发、各自独立编译、互不干扰。所以这是一个组合：用 work trees、用任务管理软件、让工作本身可移植（portable，这就是 team 那一块的作用），再往里塞自主 agent——一个或多个不同的 agent 跑在某个工作流上。我们大致——

[1:02:26]

that we basically ship stuff, the way I ship stuff, uh is I have an orchestrator agent that's run by Claude usually, but could be codeex 2. Uh, I try to have as minimal a number of keystrokes as possible to go from like here's an idea of something that needs to be fixed to work being started on it because I can course correct that work later. Think like grabbing a unit and just like clicking across the map and you'll come back later to like make it work effectively. Um, status tracking, watching your mini map, it's the RTS equivalent uh from the orchestrator of all the different uh spawned workers that you have working. Uh, and then all those workers being instructed basically to try to go as far as they can, really put like a really low premium on their time and effort and a high premium on yours. So even if they're going to be wrong, even if they're going to need to be corrected later, it's better for them to push as far as they can before they ask for feedback. Uh, so that you can just have a lot of them running in parallel, even if it's wasteful from like a per per token standpoint. it's like saving you a lot of time or letting you do more things at once. Anyway, so they try and take everything all the way to a PR uh not just a PR but also like a summary that's well I'll get into that later anyway. So uh uh and then like how do you take each the results of every worker who completes something and like feed it back into the system so that the system learns and becomes better again like without the human having to type a lot of things or doing minimal work so they can do a lot of these things at once. Uh and then other pieces like how do you tag in other teammates? we'll also get into. Um, but anyway, this is very much like an RTS where you're like producing units, trying to move them around, trying to constantly adapt to stuff, but also with really high visibility, not just like spawning 20 agents and like hoping that you'll, you know, solve this problem for me, make no mistakes, and it'll just work in the end, cuz that doesn't actually happen in production. Um, so like some general guidelines or or or practices uh that that that we use that I use uh at least um but but that we've we've uh spread through our team is like trying to run almost everything including scripts that you run because sometimes scripts are a lot better and save on context space than than just like doing everything by the LLM obviously but running everything from the cloud instances always like never typing anything outside of it if you can avoid it. Uh having this portability because a lot of times you start work on a ticket, you start work on something and actually the reason you're stuck on it is cuz someone else on your team or even maybe another machine. Maybe you're running it locally on your computer and then you're like, "Oh like I got to go home now, but I want this to run overnight and I make it really easy to move it elsewhere uh and let other people pick it up. Uh maybe it needs more compute to do something. Whatever.

——我们交付东西、我交付东西的方式，是我有一个编排者 agent（orchestrator agent），通常由 Claude 来跑，但也可能是 Codex 2。我尽量让从「这有个需要修的点子」到「工作开始干起来」之间的击键次数最少，因为我之后可以再去纠偏这份工作。可以类比成在 RTS 里抓起一个单位，直接点到地图另一头，等会儿再回来让它真正干好活。状态追踪、盯着你的小地图（mini map），就是编排者这边对应 RTS 的动作，用来看你 spawn 出来的所有不同 worker 在干什么。然后这些 worker 基本上被指示要尽可能往前推，真的把它们的时间和精力看得很轻、把你的时间看得很重。所以哪怕它们会出错、哪怕之后需要被纠正，让它们在求反馈之前尽量往前推，仍然是更好的——这样你就能让一大堆 worker 并行跑，即使从每个 token 的角度看很浪费，但它给你省了大量时间，或者让你能一次做更多事。总之，它们会尝试把每件事一路推到 PR，不只是 PR，还有比如一份摘要（summary），这个我后面会讲。然后就是，你怎么把每个完成了某件事的 worker 的结果反馈回系统，让系统能学习、变得更好——同样，不需要人类打很多字、或者用最少的人力，这样人就能一次做很多这种事。还有别的环节，比如怎么把其他队友（teammates）拉进来（tag in），我们后面也会讲。但总之，这非常像 RTS：你在生产单位、试图四处调动它们、不断适应各种情况，但同时保持很高的可见性（visibility）——而不是像「spawn 出 20 个 agent，然后指望它们替我解决这个问题、不犯任何错、最后就能跑通」，因为那在生产环境里根本不会发生。说一些通用的指导原则或做法，至少是我自己用、并且我们在团队里推广开来的：尽量让几乎所有东西都从云端实例（cloud instances）跑起来，包括你跑的脚本——因为有时候脚本比什么都让 LLM 直接做要好得多，也比直接全靠 LLM 更省 context 空间，这很显然——但如果能避免，就永远不要在它之外打任何字。还有这种可移植性（portability），因为很多时候你在一张 ticket 上开始干活、在某件事上开始干活，而你卡住的真正原因，可能是你团队里的另一个人、甚至是另一台机器。也许你在自己电脑上本地跑着，然后你想「哦我现在得回家了，但我想让它跑一整夜」，我就把它弄得非常容易挪到别处去、让别人接手。也许它需要更多算力来做某件事，随便什么原因。

[1:05:11]

It needs more memory." Um, and uh, and then also just like always running in dangerously skip permissions mode like whenever possible. Uh, if you can't be running in dangerously skip permissions mode, do what you need to do to like make a sandbox so you can, but if you're having to give feedback at any regular pace, like you're going to go really slow. Uh, and then like so what yeah, what do the workers do? As I mentioned before, they're always trying to go to PR. Uh, they are not rigorously adhering to like the given spec you do. they're trying to learn and adapt to it as they go because your specs will be wrong. Uh, and it's okay for them to make assumptions because you can correct them uh as you catch them. Um, and then, you know, for like, for example, front-end development doing every everything is like pre-baked into the worker spawn. So boot the local dev server, run tests yourself on it, have it ready and waiting so that the human can just come and open a browser tab pointing to the right port and they can just test the thing as quickly as possible. Minimizing the number of human steps that need to be taken and like clicks to just move something forward to the next step uh step. Um and also just like lots of things baked in that are like what are things that we know really reliably? the agent's going to be bad about how do we learn about those things, bake them in, put them in uh to not just like the cloud MD file, but also like broader reaching graphs that you have of MD files uh which I'll get to later uh to make those things less of a problem. So, for example, one of like the really obvious things that Claude is super bad at today is predicting how long it'll take to do something. If you ask it like how long is it going to take to solve this problem be like a maybe like two weeks of like you know one engineer's work and in practice it takes like one prompt and it can do it in 20 minutes cuz it's trained on what it would have taken a human to do those things that's all it's like basis for training data the these systems haven't been around long enough for that to be updated and I think they'll like always be behind anyway so you can take all these things and be like no no never trust yourself in these ways uh and uh and then also like you people think a lot and a lot of times it's kind of true that like the code is the source of truth but the code is often like a really expensive source of truth for the agents to pull context out of and it's actually really cheap especially when you have all the context loaded in memory to like aggressively document things in a way that benefit future agents. So uh not just like writing comments in the code but also structured linked uh um sort of wiki style knowledge knowledgebased files that will make future agents have an easy time um basically take advantage of the context as much as you can uh and also helps the visibility of humans and and audit auditability of what you do.

它需要更多内存。还有就是，尽可能始终在「危险跳过权限（dangerously skip permissions）」模式下跑。如果你没法在 dangerously skip permissions 模式下跑，那就想办法搞个 sandbox 让自己能这么跑；但如果你得以任何常规节奏不停地给反馈，那你就会跑得非常慢。然后，worker 都在干什么？像我前面说的，它们总是奔着 PR 去。它们不会严格死守你给的那份 spec，而是边做边学习、边适应，因为你的 spec 会有错。让它们做点假设也没关系，因为你抓到了就能纠正。再比如前端开发，所有东西都预先烤进 worker 的 spawn 里：启动本地 dev server、自己在上面跑测试、让它就绪待命，这样人类只要过来、打开一个指向正确端口的浏览器标签页，就能尽快把东西测了。尽量减少人类需要走的步骤、需要点的鼠标，好把东西往下一步推。还有就是把很多东西预先烤进去——那些我们很可靠地知道 agent 会做得很糟的事情，我们怎么去摸清这些事、把它们烤进去，不只是烤进 CLAUDE.md 文件，还烤进你拥有的那张范围更大的 MD 文件图谱里（这个我后面会讲），让这些事不再那么成问题。比如说，今天 Claude 超级不擅长的一个明显例子，就是预估做某件事要花多久。如果你问它「这个问题要花多久解决」，它会说「大概一个工程师两周的工作量」，可实际上只要一个 prompt、20 分钟它就能搞定。因为它是基于「人类做这些事要花多久」训练的，那就是它训练数据的全部依据；这些系统出现的时间还不够长，还没法更新这一点，而且我觉得它们大概会永远落后。所以你可以把这些事都拿过来，对它说「不不，在这些方面永远别信你自己」。还有，人们想得很多——而且很多时候确实没错——说「代码才是真相之源（source of truth）」；但代码对 agent 来说，往往是一个非常昂贵的真相之源，要从里面把 context 抽出来很费劲。而其实是非常便宜的——尤其是当你已经把所有 context 都加载进内存里时——去激进地把东西文档化，用一种能让未来的 agent 受益的方式。所以不只是在代码里写注释，还有结构化的、带链接的、wiki 风格的知识库文件（knowledge based files），让未来的 agent 用起来很轻松，基本上就是尽可能地利用好 context；这也提升了人类的可见性、以及你所做之事的可审计性（auditability）。

[1:07:54]

Uh, so macro by default, micro win it counts is another RTS principle. Like you can't win a game of RT uh like RTS game usually if you're just really good at moving your individual units because if you didn't make any units, you're just going to lose. Uh so yes, it's important to like deep dive and tunnel vision into certain things that are really critical. Some tickets for sure take a long time, but anytime you're like tunnel visioned into something, you should always be thinking, how do I spawn as many other little things that don't take my cognitive bandwidth as much and just like move those things forward? Um, so that always you're basically like maxing out your cognitive capacity. Um, and again, like things can wait. You can come back to them like 3 days later. It's not that expensive and you can just ask Claude like remind me what the hell I was doing with this thing. All this stuff is really cheap. what's expensive but doesn't feel expensive is like not doing these things at the same time. Um anyway, so macro necessary, micro useful, but you can win honestly in RTS games and I think in a lot of things, including in programming, if you just macro enough, if you just do enough things, you'll kind of uh stupidly adjust your way towards something that's good if you're just always really quickly identifying problems and solving them. Um and yeah, this is gets back to like the high visibility thing. So, one of the things that I really like about you like how I set things up is it's not like a lot of agents that are kind of tucked away and that you have to like dig in hard to actually read what their ongoing stream is and what they're actually doing like like in an RTS game like you click buttons to immediately jump to different key points in the map so you can always be auditing stuff and always like catch it and correct it quickly if it's a critical thing. That true I that too I find is like super useful in programming. Uh because again like they're going to make mistakes all the time. They're going to like go in wrong directions and you definitely save time and value if you catch them early, fix them, course correct. Uh so you should be kind of like looking around between your different agents, monitoring them while you are also trying to have as many as you can. Um another thing to this point that I personally like a lot uh and is like a big thing in RTS games is audio. So, like the only way that you can manage a big army across the whole map is to have lots of audio cues where it's like your base is under attack or you know this guy's moving or whatever thing is happening. You don't have to be looking at you can hear and it's like okay I need to put my attention to this thing and you know based on like a lot of variety these audio cues that you can learn and they're good like pneumatic devices. Uh what's important?

「默认宏观，关键处再微操（macro by default, micro when it counts）」是另一条 RTS 原则。一局 RTS，如果你只是非常擅长操控单个单位，通常是赢不了的——因为如果你压根没造兵，你就是会输。所以是的，对某些真正关键的东西深挖、钻进去看，是很重要的，有些 ticket 确实要花很长时间；但每当你钻进某件事里时，你都该一直在想：我怎么再 spawn 出尽可能多的、不怎么占我认知带宽的小事，把那些东西也往前推？这样你基本上就是一直在把自己的认知容量拉满。再说一遍，很多事情是可以等的，你可以三天后再回头看，那没多贵；你可以直接问 Claude「提醒我一下我之前拿这玩意儿到底在干嘛」。这些东西都很便宜。真正昂贵、却感觉不出昂贵的，是「不去同时做这些事」。总之，宏观是必要的，微操是有用的；但说实话，在 RTS 游戏里、我觉得在很多事情里（包括编程），只要你宏观做得足够多、只要你做的事情足够多，你就会以一种近乎笨拙的方式磕磕绊绊地、一路调整着走向一个不错的结果——只要你总是非常快地识别问题、并解决它们。这又回到了高可见性那一点。我特别喜欢自己这套设置的一点是：它不像那种把一堆 agent 藏起来、你得费劲钻进去才能看到它们正在输出的流、看到它们到底在做什么。就像在 RTS 游戏里，你点几个按钮就能立刻跳到地图上不同的关键点，所以你能一直在审视、一直能抓到问题，碰到关键的事就快速纠正。这一点我也发现，在编程里超级有用。因为同样，它们会一直犯错、会朝错误的方向跑，而你越早抓到、修掉、纠偏，就越能省时间、省价值。所以你应该在你不同的 agent 之间四处巡视、监控它们，同时还尽量多开几个。还有一点我个人很喜欢、也是 RTS 游戏里的一个大件，就是音频（audio）。要在整张地图上管理一支大军，唯一的办法就是有大量音频提示，比如「你的基地正遭受攻击」，或者「这个家伙在移动」，或者别的什么正在发生的事。你不必盯着看，你能听到，然后就「好，我得把注意力放到这件事上」。基于各种各样你能学会的音频提示——它们是很好的助记装置（mnemonic devices）。什么是重要的？

[1:10:29]

What do I need to act on right away? What don't I? So, like the way I run my personal setup is I actually have all of my individual agent uh like T-M sessions mapped to different Warcraft and Starcraft units uh that are colorcoded and themed based on the type of ticket it is. And then they play the actual sound effects from Warcraft and Starcraft units. So, I immediately know and like visually identify. I don't even have to read like this tab needs my attention. This thing's going on. Anyway, like to me it just seems like a natural way of like take advantage of these and and again like Cludes made all these things for me really quickly as like a side ticket that I was working on over time while I worked on eight other things. So it's like why not do these things and these these devices pneumatic devices uh or or whatever like cues for people are really optimized in gaming and they like know what good sound design is to like be memorable and otherwise catch your attention in different ways. Um, yeah, and like cult use of color, icons, anything that's just like quicker to read and process because I actually do think like these things matter a lot, especially if you're trying to uh really aggressively get a lot of stuff done and the sky is kind of the limit in how you can do that stuff. Another thing we built internally is like an APM tracker. Uh, and I'll just show quickly here. Um, so and this this is Warcraft 3, which is like one of the lower APM requiring professional RTS games, but this is what it looks like to actually play this game well uh at the at the top level. And one of the things that you'll notice is like no APM is not the uh the thing that like if you max it, you're the best player in the world, but nobody is good who doesn't have high APM. And so you can just kind of take that as a mental rubric like if I'm like thinking and like typing slowly and like am I if this was a competition, would I really be the best? Like do I really need to take that much time in everything I'm doing? and how much can I just take like lots of little micro decisions and you know fall toward the right uh the right goal or toward making things better. Um anyway, so this is just something like we we you know each of us run like personally on our computers and keep an eye on and it's just like just keep track of like are things moving and this this APM is not like clicks you have because I don't think that's like a great tracker for for for agent use. We use tool you tool calls. It's like how many tool calls are your agents doing per minute? Uh this minute, this five minutes, this hour, this day, this seven days, like how do you max all those things and have high numbers. Um and again, it's like it's it's one metric among many, but it's how are you actually being really productive or are you really doing the most you could be doing if you have a low APM? Uh probably not. So otherwise like things probably a lot of people know uh easy way to to use tokens more effectively is just like do a lot of things in parallel do different things with the same agent do different agents in parallel it will uh invariably like for complex tasks usually give you a better outcome than if you did it by yourself and just like in an RTS like you should be spending your resources you should never have your claude tokens like sitting unused that's really inefficient economy like use them all

我得马上处理什么？什么不用？所以我个人这套设置的跑法是：我其实把我每一个 agent 的 tmux 会话都映射成不同的魔兽争霸（Warcraft）和星际争霸（Starcraft）单位，按 ticket 的类型做了配色和主题区分；然后它们会播放魔兽和星际单位真正的音效。这样我立刻就知道、并且能在视觉上识别出来——我甚至都不用读，就知道「这个标签页需要我注意，这件事正在发生」。总之对我来说，这就像是一种很自然的方式去利用这些东西；而且同样，这些都是 Claude 很快帮我做出来的，就当作一张我抽空在做的边角 ticket，我一边还在干另外八件事。所以就是「为什么不做这些事呢」？这些装置——助记装置，或者随便你怎么叫、给人用的各种提示——在游戏里被优化得非常好，游戏行业很懂什么是好的音效设计（sound design），知道怎么让它令人难忘、或者用各种不同方式抓住你的注意力。是的，还有对颜色、图标这类东西的狂热使用，任何能让你更快读取、更快处理的东西——因为我真的觉得这些东西很重要，尤其当你想非常激进地把大量事情做完时，你能怎么搞这些花样，几乎是没有上限的。我们内部还造了一个东西，叫 APM tracker（每分钟操作数追踪器）。我快速给大家看一下。这是魔兽争霸 3，它算是职业 RTS 里对 APM 要求较低的一款，但这就是在顶级水平上真正把这游戏打好是什么样子。你会注意到一点：不，APM 不是那种「你拉满它、就成了世界第一」的东西；但没有谁是高手却没有高 APM 的。所以你可以把它当成一把心智标尺：如果我在那儿慢吞吞地想、慢吞吞地打字——如果这是一场比赛，我真的会是最强的吗？我真的需要在做的每件事上都花那么多时间吗？我又能在多大程度上只做大量小的微决策，然后磕磕绊绊地朝着正确的目标、朝着把事情变好的方向走？总之，这就是我们每个人在自己电脑上跑、并随时留意的东西，就是用来记一下：事情有没有在动。而这个 APM 不是指你点了多少下，因为我觉得那对衡量 agent 的使用不是个好指标。我们用的是 tool calls——就是你的 agent 每分钟做了多少次 tool call：这一分钟、这五分钟、这一小时、这一天、这七天，你怎么把所有这些数字拉满、保持高位。再说一遍，它只是众多指标中的一个，但它反映的是你到底有没有真正高产、有没有真正把你能做的做到极致；如果你的 APM 很低，那大概是没有。除此之外，很多人大概都知道的：更高效地用 token 的一个简单办法，就是大量并行地做事、用同一个 agent 做不同的事、用不同的 agent 并行做——对于复杂任务，它几乎必然会给你比你自己单干更好的结果。就像在 RTS 里，你应该把你的资源花出去，绝不该让你的 Claude token 闲置不用，那是非常低效的经济模式——把它们全用起来。

[1:13:50]

every hour period that you man. Um, knowledge base. This is like a really big thing that that for us I think is still like somewhat early on. But, uh, this whole presentation I made and started the exact same way that, uh, I'm just describing how I do tickets, which is I went to Claude, I took what France asked me to talk about, I pasted it in, I said, "Look at our knowledge base and how we do stuff." And put together a PowerPoint presentation based on the philosophies embedded in there and like what I've told you before. and he didn't like oneshot it, but it's like I maybe did like 15 edits to it, you know, and and got to this presentation. Uh, and then I refed it all back into the knowledge base and said like learn everything that I've said and all the the the advice I've given and corrections I've given and like make those better instilled in the knowledge base. And this knowledge base is basically just because like linked docs are much faster diverse by LLMs. And so uh and you can encode everything including business knowledge and indeed like Claude and and Codex are really good at coming up with features and stuff if they have enough knowledge about your business. Uh so trying to build this up in an automated way is super useful. People come up with their own tickets. Uh because if you have something you could do everybody you should just like do it. Everybody should be full stack all the time. Uh be reactive. Uh and uh even if agent does it way worse than you or slower than you, it's still better to have it do it. And uh it's easy to change things when they're screwed up. Satisficing is a word from economics is like do things satisfi like enough but not perfect. Uh really really key principle for like everything. Uh mix different ticket sizes at the same time. Uh you know in like we we've three and a halfx our output uh PRs per engineer per month. uh both because LM have made ourselves better, but like when we like really adopted this stuff broadly with everyone on the team this last month, we grew another 60% in our PRs per engineer per month. So like you're not going to get a lot smarter, but the thing you can train on yourself is like how do I act like people who are good at doing these kinds of things really well like RTS pro players? What does it look like to be like optimal in this and how can I learn the methods of doing it just like program like an RTS pro? Thank you.

你管理的每一个小时段。嗯，knowledge base。这对我们来说其实是个很大的东西，我觉得目前还算处在比较早期的阶段。不过呢，我做的这整场 presentation，开头用的方式跟我刚才描述我怎么处理 tickets 是一模一样的：我去找 Claude，把 France 让我讲的内容拿过来，粘贴进去，然后说「看看我们的 knowledge base，看看我们是怎么做事的」，然后基于里面沉淀的那些理念、以及我之前告诉过你的那些东西，整理出一份 PowerPoint presentation。它并没有一次就搞定，但大概就是我对它做了 15 次左右的修改，你懂吧，最后做成了这份 presentation。然后我又把这一切全部喂回 knowledge base，跟它说「把我说过的所有话、我给过的所有建议、我做过的所有更正都学下来，让它们更好地固化进 knowledge base 里」。而这个 knowledge base，基本上就是因为相互链接的文档能被 LLM 更快地处理和理解。所以呢，你可以把一切都编码进去，包括业务知识，而且说真的，像 Claude 和 Codex 这种，只要它们对你的业务了解得足够多，它们真的很擅长想出各种功能之类的东西。所以，试着用一种自动化的方式把这套东西积累起来，是超级有用的。大家自己提出自己的 tickets。因为如果有件事你能做、所有人都能做，那你就应该直接去做。所有人都应该随时是全栈的。要主动、要积极响应。而且就算 agent 做得比你差很多、或者比你慢很多，让它去做仍然是更划算的。而且东西搞砸了的时候也很容易改回来。Satisficing（满意即可）是经济学里的一个词，意思是把事情做到「足够好」就行、而不是追求完美。这是个对一切都极其关键的原则。把不同大小的 tickets 同时混着做。你知道吗，我们已经把每个工程师每月的产出——也就是 PR 数量——提升到了原来的三点五倍。一方面是因为 LLM 让我们自身变得更强了，但更关键的是，上个月当我们真正在团队里让所有人都广泛地采用这套做法之后，我们每个工程师每月的 PR 数又增长了 60%。所以说，你不会一下子变得聪明很多，但你能在自己身上训练的，是「我该怎么像那些把这类事情做得特别好的人那样去做」，就像 RTS（即时战略）职业选手那样。在这件事上做到最优是什么样子？我又该怎么学会做这件事的方法，就像照着一个 RTS 职业选手的套路去打？谢谢大家。

[1:16:06]

Okay, I think that's all we have. Um, now I think Vikica, we have cookies, ice cream, and popsicles and mochi donuts. Okay, what is a mochi donut? It's delicious. Okay. Um, yeah. So, thank you guys so much for coming. It was a lot of fun. Uh, I will send out a feedback form. Please review it and give me give me back your thoughts. um think about those uh call for presentations and calls for ideas. If you guys have ideas, let's let's definitely hear them. Um and uh looking for more papers coming up probably in in two weeks. I think we're already fully slated. Um and then basically the first one in July uh you know, we're looking to fill out as well. So if you wanted to present, please let me know. That's all I got. Thank you everyone.

好，我想我们要讲的就这么多了。嗯，那现在，我想 Vikica 这边——我们准备了曲奇、冰淇淋、冰棒，还有麻薯甜甜圈（mochi donuts）。好，麻薯甜甜圈是个啥？很好吃。好的。嗯，对了。所以，非常感谢大家今天能来，今天玩得很开心。我会发一份反馈表出来，请大家填一填，把你们的想法反馈给我。另外也想想那个征集 presentation、征集点子的事。如果你们有什么想法，我们绝对很想听到。嗯，下一批要讲的论文大概在两周后，我想我们的安排已经排满了。然后基本上七月的第一场，你知道的，我们也还想把它填满。所以如果你想来做分享，请告诉我。我要说的就这些。谢谢各位。