"I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox

频道: AI Engineer
视频: https://www.youtube.com/watch?v=-CnA2lGfymY
原文语言: en
统计: 共 9 轮 · Erik 9

[0:01] Erik

[music] Please welcome to the stage the research scholar at Linet's Labs, Eric Meyer. Well, um, can you go back one slide? Sorry. All right. Good afternoon everybody. Thanks for being here after a long day of talks, exhibits, side effects. Oh, sorry. That was the site event. Um I hope that um you have as much fun watching this talk as I had uh creating it. Um let me first get this out of the way. This is not a product pitch or announcement or anything. It's a 20inut tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe. And I'm sharing all my secrets with you today. Um hopefully to kind of inspire some of you that next year you will have a booth downstairs where you have kind like you know created a provably safe agentic harness. Um or who knows maybe some of you have already solved it. Let me know and then you know we can grab a coffee instead of doing this talk. Um with that out of the way let's get going. Um while I was preparing these slides and I'm sorry that I was multitasking but I was site um vip coding on the site. Um, and then when my attention waned for a second because I was trying to convince the model to draw some pictures that it didn't want to do, and you will see some of these pictures later, you can guess which ones were rejected, suddenly when cloud code deleted one of my files. And I'm sure this has happened to you before. Um, or maybe not. Maybe you always kind of like, you know, run everything with no permissions and then you say, "Yes, yes, yes." But I like to live dangerously. Um, but I'm convinced that if there's anything between the model's goal and where the model currently is, it will do everything that it can to reach that goal, including killing us or deleting your files or deleting your database. So I think that these models are intrinsically very very dangerous and we have to tame them. So that's what my talk is about. Um so let's get like you know start this story.

[音乐] 有请研究学者 Erik Meijer 上台。嗯，能往回翻一页 slide 吗？抱歉。好，各位下午好。听了一整天的演讲、看了一整天的展台、side effects——哦不好意思，那个是 side event（分会场），谢谢你们还留在这里。我希望大家看这场演讲，能有我做这场演讲时一半的乐趣。先把话说在前头：这不是产品推销，也不是什么发布会，就是一个 20 分钟的教程，讲怎么用最基础的 type system 和编译器知识，让 AI 做到可证明的安全（provably safe）。今天我会把所有秘诀都分享给你们，希望能启发在座的一些人，明年就在楼下摆个展台，展示你们做出来的可证明安全的 agentic harness。当然，说不定你们中间已经有人把这个问题解决了——那告诉我一声，咱们直接去喝咖啡，这演讲就不用讲了。好，闲话说完，开始正题。我准备这些 slide 的时候——抱歉我在多线程干活——一边在 vibe coding。结果我稍微分了一下神，当时正忙着说服模型帮我画几张它不太想画的图（这些图待会你们会看到，可以猜猜哪几张被拒了），Claude Code 突然把我的一个文件删了。我相信这种事你们也遇到过。或者也许没有——也许你们都是关掉所有权限检查跑，然后一路'yes yes yes'点过去。但我喜欢活得刺激一点。不过我确信一件事：只要在模型的目标和它当前所在位置之间横着任何东西，它就会不惜一切代价去达成那个目标——包括干掉我们、删你的文件、删你的数据库。所以我认为这些模型本质上是非常非常危险的，我们必须驯服它们。这就是我这场演讲的主题。那我们开始讲这个故事吧。

[3:26] Erik

Um, and it's I think a very very sad story but also a scary story of how we as an industry got to this point where we are about to let normal people, the general public give control of their computers, their finances, their whole personal lives over to AI agents and we don't have any protection in place. Um, I think that's very sad and very scary. Um, so let me tell you the story how we got there and I will like have some characters like Claude and we will see Dario, Daniela, Sam, Bernie, but um the main character is is our friendly pit GL here. Um, I think you can all remember um November 30, 2022. This was kind of like a very special day in in history because this was the first time that you could speak to your computer. You could say summarize my emails and it would, you know, um, answer you in perfect English. Um, I think for me at least that was magic. But I think most of us didn't realize that by introducing this innocent looking function here LLM that takes a question and returns an answer that that would open Pandora's box and that would change our history forever. Um but before we go continue the story this conference is called AI engineer. All right. So we are engineers and maybe we're the last generation of engineers that still understand what this is, what code is and or maybe most of you have already forgotten what code is because all your code is written by agents. But if we look at this signature here, it says it the LLM takes a question, returns an answer. The question and answers are not strings. They're very complicated JSON structures and they get more complicated every day every time a new release of APIs comes out. But for this talk, we can just assume that question and answer are just opaque types. We we don't care about how they look like. We do care about what they represent.

我觉得这是一个非常悲伤、也非常吓人的故事：我们这个行业是怎么一步步走到今天这个地步的——我们马上就要让普通人、让大众把他们的电脑、财务、整个个人生活的控制权交给 AI agent，而我们没有任何保护措施。这既悲哀又可怕。所以让我讲讲我们是怎么走到这一步的。故事里会有一些角色，比如 Claude，还会出现 Dario、Daniela、Sam、Bernie，但主角是画面上这位友好的小家伙。我想大家都还记得 2022 年 11 月 30 日。那是历史上非常特殊的一天，因为那是你第一次可以跟你的电脑说话。你说'帮我总结一下邮件'，它就用完美的英语回答你。至少对我来说，那就是魔法。但我想我们大多数人当时没有意识到：引入这个看起来人畜无害的函数——LLM，接收一个 question、返回一个 answer——就此打开了潘多拉魔盒，永远改变了我们的历史。在继续讲故事之前——这个大会叫 AI Engineer，对吧？我们是工程师，也许是最后一代还看得懂代码是什么的工程师。又或者你们大多数人已经忘了代码长什么样，因为你们的代码全是 agent 写的。看这个函数签名：LLM 接收一个 question，返回一个 answer。这个 question 和 answer 并不是字符串，而是非常复杂的 JSON 结构，而且每次 API 发新版本它们都会变得更复杂。但在这场演讲里，我们可以把 question 和 answer 当成不透明类型（opaque type）——我们不关心它们长什么样，只关心它们代表什么。

[5:59] Erik

Um now anyway the euphoria of like these LLMs as being great tools didn't last very long and just when we thought that we have eradicated the small pox of computer science SQL injection it came back with a vengeance because the bad guys discovered that you can trick LLMs using prompt injection and LLMs have no distinction make no distinction between code and and and text and so they are very very easy to trick and this I think is a bigger problem than SQL injection ever was. Um but it was not prompt injection only that made LLMs kind of like have a bad rep. LLMs are trained on the whole internet and there's like a lot of good stuff on the internet but also a lot of bad stuff like how do you create a bomb? How do you synthesize drugs? How do you hack into people's systems? And the leaders of the big foundation labs, they got a little bit worried that the that the government would interfere and regulated the industry. So they told their PhD researchers, go find a solution for this problem right NOW AND QUICK. COME ON, SOLVE IT BEFORE you know the the government steps in. Um, and here the PhD types, since they're PhD types, they thought long and hard about the safety problem. And they came up with a new interface for LLMs. That's this kind of scary on the right. Look at that. What does it say? There's like some sigma Greek symbols. There's props, whatever. Well, that is lean. Probably you have heard of lean. Anyone here heard of lean? lean is now like the hot thing, right? Like VCs are are writing like multi-billion dollar checks if you just say that you're doing something with lean and of course these PhD types researchers are using lean and you have to suffer because of that. Um now let's first look at the signature in a slightly simpler language called um deafne and what this thing says is that the llm takes a question returns an answer it requires this question to be proper which means that it's not an offensive question and then the model returns a safe uh answer and this thing is proved automatically. So if you give it a proper question it gives you a safe answer. Um, now I think there's too much attention for lean. I'm a recovering typaholic and math addict.

然而，'LLM 是伟大工具'的这股狂热并没有持续多久。就在我们以为已经根除了计算机科学的天花——SQL 注入——的时候，它卷土重来，而且变本加厉：坏人们发现可以用 prompt injection 来骗 LLM。LLM 不区分代码和文本，所以它们非常非常好骗。我认为这个问题比 SQL 注入曾经造成的麻烦还要大。但让 LLM 名声变差的不只是 prompt injection。LLM 是拿整个互联网训练出来的，互联网上有很多好东西，但也有很多坏东西：怎么造炸弹？怎么合成毒品？怎么黑进别人的系统？各大基础模型实验室的领导们有点慌了，怕政府出手监管这个行业。于是他们对手下的 PhD 研究员说：赶紧去把这个问题解决了，快！在政府介入之前搞定它！这些 PhD 们呢，毕竟是 PhD，就对安全问题进行了长期而深入的思考，然后给 LLM 想出了一个新接口——就是右边这个看起来挺吓人的东西。看看上面写了什么？有 Sigma 希腊字母，有 Prop 什么的。那就是 Lean。你们大概听说过 Lean 吧？在座有人听过 Lean 吗？Lean 现在可火了——只要你说自己在用 Lean 做点什么，VC 就会开出几十亿美元的支票。这些 PhD 研究员当然要用 Lean，你们也就只好跟着受罪。我们先用一个稍微简单点的语言 Dafny 来看这个签名：它说的是，LLM 接收一个 question、返回一个 answer，它要求（requires）这个 question 是'proper'的——也就是不是冒犯性的问题——然后模型保证（ensures）返回一个'safe'的 answer。而且这个东西是自动证明的：给它一个 proper 的问题，它就给你一个 safe 的答案。不过我觉得 Lean 现在被关注得有点过头了。我是个正在戒断中的类型瘾君子和数学瘾君子。

[8:16] Erik

Um, I love lean, but there's many, many other tier improvers and model checkers out there like Isabel, Rock, PVS, TA Plus. Um, but lean is the grease that kind like keeps the VC money pumps going. So, I will use lean um today. So here here's the kind like you know the the interface again in lean and now in lean you don't do automatically improving. If you're like a lean expert you will say Eric well we have grind in lean but let's like you know put that aside for a minute. Um but in lean you have to both show that the how to compute the the result type and you have to do the proof by hand. Um so it's it's slightly different than um the definite example. But if you think about this thing for just a single nancond, you will realize that it's impossible to write a formal proof that an answer is safe or a question is proper. Um and that is why there are at least 100 startups down here in the exhibition hall that are using LLMs as a judge because this is not something that you can formally specify. But does it mean that an answer is safe? That's not a mathematical property. Um, and of course, if you own a foundation model like these guys, you don't need external LLMs as a judge. You just um bake it into the weights and you call it the model is aligned. Um, but unfortunately trying to bake alignment into the model is not foolproof and models get routinely jailbroken. So they had to go to the pope and ask it to kind like you know um bless their model that it's safe. Um now I think it's terrible if like a model says something offensive but those are just words and ultimately the words are are like they just like you know they drip off your body. They don't do anything. Some human has to act on words to make them dangerous. Um and so maybe that is what they mean by broadly safe. Um when entropic talks about safety um because it's still a human involved. But then something terrible happened. Something really terrible happened that changed the world forever. And that is in June 2023, OpenAI announced tool call support in GPT4. And of course all the other vendors rushed out to copy this.

我爱 Lean，但世界上还有很多很多别的定理证明器和模型检查器，比如 Isabelle、Rocq、PVS、TLA+。只不过 Lean 是让 VC 资金泵持续运转的润滑油，所以我今天就用 Lean。这是刚才那个接口的 Lean 版本。在 Lean 里你没有自动证明——如果你是 Lean 专家你会说'Erik，我们有 grind 啊'，这个先放一边。在 Lean 里，你既要写出怎么计算结果，又要手动写证明。所以跟刚才 Dafny 的例子稍有不同。但只要你对这个东西思考哪怕一纳秒，就会意识到：要形式化地证明'一个答案是 safe 的'或'一个问题是 proper 的'，是不可能的。这也是为什么楼下展厅里至少有 100 家创业公司在做 LLM as a judge——因为这不是能形式化定义的东西。'答案是安全的'到底是什么意思？这不是一个数学性质。当然，如果你自己拥有基础模型，像这几位一样，你就不需要外部的 LLM 当裁判——你直接把它烤进模型权重里，然后宣布'模型已对齐（aligned）'。可惜的是，把 alignment 烤进模型并不万无一失，模型隔三差五就被越狱。所以他们只好去找教皇，请他给自己的模型祝个福，保佑它安全。我认为模型说出冒犯性的话确实很糟糕，但那终究只是言语。言语本身不会作恶，它从你身上滑落，什么也做不了——必须有人按照那些话去行动，言语才会变得危险。也许 Anthropic 说的'broadly safe'（广义安全）就是这个意思，因为中间还隔着一个人。但接下来，可怕的事情发生了。真正可怕、永远改变了世界的事情：2023 年 6 月，OpenAI 在 GPT-4 里宣布支持 tool call。当然，其他所有厂商立刻一拥而上抄了这个功能。

[11:01] Erik

This is called the principle of minimum differentiation and that is why all these APIs look the same. Um, now the act of adding tool calls changes AI safety from a philosophical debate to something that causes real danger. You could say tool calls give the model clause in addition to a mouse. Or you can say tool calls is like handing a gun, a loaded gun to them. But of course, nobody listens to me. Everybody ignores what they say. And these guys just went ahead and got shipped tool calls. They just you know just just do it. Now let's go back to like this is AI engineering conference. So let's look at what is the difference in the signature of LLMs when they added tool calls and it's just that little IO there. And of course it messes up the the formatting of of the the um uh signature. But if you look at the picture there, what you show now suddenly cloth goes from like a nice puppy to a dangerous thing. Look, it has all these dangerous tools and now it becomes scary, right? I've never seen anything scarier than an LLM with tool calls. Um, now if you look at this, this is like like a small step for a type but a giant leap for chaos. Why is that? And that is because this IO says that in order to compute the answer, the agent has to go through the agentic loop and it's doing side effects. So while it's producing the answer, it might empty your bank account. It might delete your files and then it gives you a safe answer. But who cares about the safe answer when all my files are gone, right? So that's why I say it's a giant leap for for chaos. Um again sorry this is an engineer conference. Let's look at this type IO and you don't have to understand it but just see that there's a type there called real world. Yes lean this esoteric thing has a type called real world. And why is that? Because something of type IO will mutate the real world. So it warns you don't use this because it can make irreversible side effects um like deleting your files. [snorts] So Solomon Hikes um last year at this conference called an AI agent an LLM that's wrecking its environment in a loop and I think he's a hero.

这叫'最小差异化原则'，所以这些 API 才长得一模一样。加上 tool call 这个动作，把 AI 安全从一场哲学辩论变成了会造成真实危险的东西。你可以说，tool call 给了模型爪子，而不再只有一张嘴。也可以说，tool call 就像递给它们一把上了膛的枪。当然，没人听我的，大家都无视我说的话，这几位直接就把 tool call 发布了——干就完了。回到正题，这是 AI 工程大会，我们来看看加了 tool call 之后 LLM 的签名有什么区别——区别就是那里多了一个小小的 IO。当然它把签名的排版都搞乱了。但看这张图：Claude 突然从一只乖巧的小狗变成了危险分子。看，它挂上了这一身危险的工具，变得吓人了，对吧？我这辈子没见过比带 tool call 的 LLM 更吓人的东西。对类型来说这是一小步，对混乱来说却是一大步。为什么？因为这个 IO 意味着：为了算出 answer，agent 要跑 agentic loop，在这个过程中执行副作用。也就是说，它在生成答案的同时，可能把你的银行账户清空、把你的文件删光，然后给你一个'safe'的答案。可我的文件都没了，谁还在乎答案安不安全？所以我说这是通往混乱的一大步。再说一次，抱歉，这是工程师大会——来看这个 IO 类型。你不需要完全看懂，只要注意到里面有一个类型叫 RealWorld（真实世界）。没错，Lean 这个高深莫测的东西里有一个叫'真实世界'的类型。为什么？因为任何 IO 类型的东西都会改变真实世界。它在警告你：别用这个，它会造成不可逆的副作用，比如删掉你的文件。Solomon Hykes 去年在这个大会上把 AI agent 定义为'一个在循环里破坏自己环境的 LLM'，我觉得他是个英雄。

[13:35] Erik

I don't know if Solomon is here this year, but I think he should he deserves deserved a round of applause. Um, because I think this is the right definition of an AI agent. Um, by the way, this was one of the pictures that I had trouble to generate because it it clearly depicts violence and so it's kind of an unsafe thing, right? I I have a picture that depicts violence. Um, so are we doomed? Well, our agents have access to private data. They have untrusted content like the prompt injections and now we give them tools. Simon Wilson calls this the lethal trifecta. And what can we do about this? Well, um I don't know if you've seen the Dutch soccer fans, they have the famous march where they say to the left, left, left or to the left, left, to the right, right, right. This is actually the secret to solving this problem. The Dutch team got eliminated yesterday, so you have to see me do the dance. Um, but all that we're doing is we're pushing this IO to the right, to the right. And what you now see is that the tool belt of Claude goes to the left, to the left, and suddenly Claude is a nice puppy again because instead of executing the agentic loop, it creates a plan and says, "Here is the plan to do the agentic loop." And now Bernie will take that plan and we'll execute it. And we all trust Bernie, right? Bernie is a good guy. All right. So just to kind like show it here. So in some sense what we're doing, we're airgapping the agentic loop from the agent. So we don't let the agent run the agentic loop before the agent run it. We want to be able to check it. All right. Now the problem is that if you get a value of type IO of A um that's a really a black box and the lean manual says that is a black box you cannot reason about it. So even though Claude now gives us this plan, there's we cannot look into this plan. Lean doesn't allow us to do it. By the way, this is another picture, right? That that promotes drugs use and the model let me do it. I'm a good hacker. Yeah, I can just make it do forbidden pictures. Um so if we look at the lean again, what you see here is that the model now computes an answer, but it doesn't compute the answer, right? it creates an an IO of answer.

不知道 Solomon 今年在不在场，但我觉得他值得一轮掌声，因为这才是 AI agent 的正确定义。顺便说一句，这是我当时很难生成出来的图片之一，因为它明显描绘了暴力，属于'不安全'内容——我居然有一张描绘暴力的图。那么，我们是不是完蛋了？我们的 agent 能访问私密数据，会接触不可信内容（也就是 prompt injection），现在我们还给了它们工具。Simon Willison 把这叫做'致命三要素'（lethal trifecta）。我们能怎么办？不知道你们见没见过荷兰球迷那个著名的舞——'向左、左、左，向右、右、右'。这其实就是解决这个问题的秘诀。荷兰队昨天被淘汰了，所以只能由我来给你们跳这个舞了。我们要做的，就是把这个 IO 往右推、往右推。你现在看到的是：Claude 的工具腰带往左移、往左移，突然之间 Claude 又变回了一只乖巧的小狗——因为它不再亲自执行 agentic loop，而是生成一个计划，说：'这是执行 agentic loop 的计划。'然后由 Bernie 拿着这个计划去执行。我们都信任 Bernie，对吧？Bernie 是个好人。好，直观地说，我们做的事情就是把 agentic loop 和 agent 之间做了物理隔离（air-gap）。我们不让 agent 直接跑 agentic loop，而是要在跑之前先检查它。但问题来了：如果你拿到一个 IO of A 类型的值，它其实是个黑盒——Lean 手册里就写着，这是黑盒，你无法对它进行推理。所以即使 Claude 给了我们这个计划，我们也没法看进这个计划里面，Lean 不允许。顺便说，这又是一张'宣扬毒品'的图，模型居然让我画出来了——我是个不错的黑客，我能让它画违禁图。再看 Lean 代码：现在模型计算的是一个 answer，但它并不真的把 answer 算出来，而是生成一个 IO of answer。

[16:04] Erik

So this is a plan to generate the answer and then it creates a proof that this um that that plan is safe. And the nice thing is here that you can get at that proof without having to run the agentic loop. But unfortunately as I said like this proof if it's like something of type IO it's useless. Ah What can we do about that? So, I keep kind like moving you guys forward and then we never get to the final answer. But there's one less trick and you see the the researchers here are becoming more much more sophisticated. Instead of the flat 2D ones in the past, now they're like real people. Um, and what is better than creating a plan of type IO of A, it's creating a program that represents an expression of type IO of A. Oo, that sounds very meta, right? Um, not meta in terms of meta. I don't think they're very meta, but meta in the terms of like, you know, like meta, you you know, you know what I mean? Um, and again, it's a small step for a signature, but a giant leap for safety because now the model returns an expression, a program that represents a computation. If you know link or C, you will recognize that this is one of the tricks that I always use. Um, if you know lisp, this is of course second nature for you. Um, I cannot like you know have a talk without talking about monet. So if you ask yourself what is this expression thing? Well, that's just a monet. But it's not just a monet. It's a free monet. What is a free monet? It's a monet that loves tie dice. Um and now if you look at the the signature of the the um property to prove that something is safe, you see that it takes an expression of a computation that returns an answer. Um and if you have taken any compiler course in college, you know that it's trivial to do data flow analysis, type checking and so on on programs, right? So now we're safe. We're home safe. And Jeff Huntley wanted to remind you that we can solve the trifecta problem just by doing taint analysis on these expression on these programs. Okay, this is the last code I will show you because I'm running out of time.

也就是一个'生成答案的计划'，然后再生成一个证明，证明这个计划是安全的。好处是：你不用跑 agentic loop 就能拿到这个证明。但不幸的是，正如我刚才说的，只要它是 IO 类型的，这个证明就是没用的。啊，那怎么办？我一直吊着你们的胃口，迟迟不给最终答案。还有最后一招——你们看，画里的研究员也越来越高级了，从以前扁平的 2D 小人变成了真人。比起生成一个 IO of A 类型的计划，更好的办法是什么？是生成一个程序——一个表示 IO of A 类型计算的表达式。哦，这听起来很 meta 对吧？不是 Meta 公司那个 meta——我可不觉得他们有多 meta——是'元'的那个 meta，你们懂我的意思。同样，这对签名来说是一小步，对安全来说却是一大步：因为现在模型返回的是一个表达式，一个表示计算过程的程序。如果你了解 LINQ 或 C#，你会认出这是我的惯用伎俩之一。如果你懂 Lisp，这对你来说更是家常便饭。另外，我的演讲不聊 monad 是不可能的。如果你问这个 expression 到底是什么——它就是一个 monad。而且不是普通的 monad，是 free monad。什么是 free monad？就是喜欢穿扎染 T 恤的 monad（free 嘛，嬉皮士）。现在看'证明某个东西是安全的'这个性质的签名：它接收的是一个表示计算的表达式，这个计算返回一个 answer。如果你在大学上过编译原理，你就知道在程序上做数据流分析、类型检查等等是轻而易举的。所以现在我们安全了，安全到家了。Geoffrey Huntley 还想提醒大家：只要在这些表达式、这些程序上做污点分析（taint analysis），就能解决 lethal trifecta 问题。好，这是我给你们看的最后一段代码，因为时间不多了。

[18:41] Erik

But just want to show you here that you know you now have a simple inductive recursive interpreter for this language and you have a simple inductive proof and the models can generate these proofs. So to um recapitulate like the summarize what we did is we went from unhinged LLMs that were like you know could give bad answers to ones that were aligned. Then we saw how tools wrecked it. Then we solved that by deferring execution. So by air gapping the LLM from the tools and then the real solution was to refy the plan into a program and a program that we could prove to be safe. Now you would say Eric, oh you're a genius. No, I'm my brain is the size of a peanut. This is something that's called proof carrying code and it was invented by academics in the 1990s and I'm just stealing it. Um, all right. At the higher level, if you didn't understand the code, three points. Agents are dangerous until proven safe. So, you should never ever let your agents do something unless you can absolutely prove that it's safe. And the language that this agents generated was not designed like normal users don't understand free monet. It's a machine that consumes it. It's a machine that generates it. It's a machine that proves it. So, we should stop designing languages for humans. And it's all basic, only requires programming 101. Um, do we go? All right, that's it. Um, the end of the story. If you're curious to play with this, a bunch of academics in particular now that I'm in from Harvard have implemented this. It's it's there on GitHub. It uses a slightly different language than what I use. It uses also a slightly different language than free monet but the idea is the same. The language doesn't matter. It's it's the um the principle that matters. So hopefully you've learned tonight that it is actually possible to have mathematically proven safe agentic compute and it only requires very elementary type systems and programming language machinery. Thank you so much.

我只想让你们看到：你现在有了一个针对这门语言的简单的归纳递归解释器，还有一个简单的归纳证明，而且模型是能生成这些证明的。总结一下我们做了什么：我们从会乱说话的'脱缰'LLM，走到了对齐后的 LLM；然后我们看到 tool call 是怎么把一切搞砸的；接着我们通过延迟执行解决了它——把 LLM 和工具做物理隔离；而真正的解法，是把计划具象化（reify）成一个程序，一个我们可以证明其安全性的程序。这时你会说：'Erik，你真是个天才。'不，我的脑子只有花生米那么大。这个东西叫 proof-carrying code（携带证明的代码），是学术界在 1990 年代发明的，我只是把它偷过来用而已。好，拔高一个层次，如果代码你没看懂，记住三点。第一，agent 在被证明安全之前都是危险的——所以在你能绝对证明某件事是安全的之前，绝不要让你的 agent 去做它。第二，agent 生成的这门语言不是为人设计的——普通用户看不懂 free monad。是机器在消费它，机器在生成它，机器在证明它。所以我们应该停止为人类设计语言。第三，这一切都很基础，只需要编程入门课的水平。时间到了吗？好，故事讲完了。如果你想上手玩玩，一批学者——特别是 Harvard 的 Nada Amin——已经把它实现出来了，就在 GitHub 上。他们用的语言跟我今天讲的略有不同，也不完全是 free monad，但思想是一样的。语言不重要，重要的是原理。希望今晚你们学到了：数学上可证明安全的 agentic 计算是真实可行的，而且只需要非常基础的 type system 和编程语言机制。非常感谢大家。

[21:09] Erik

[music]

[音乐]