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

AI Engineer · 21 min · 236 sentences · from YouTube's caption track

Each timecode opens YouTube at the start of that sentence. Line anchors (#s42) are the cue ids in the WebVTT, and every line carries its start and end seconds. All transcripts has every talk, and the whole corpus as one file.

00:01[music]
00:13Please welcome to the stage the research scholar at Live Nets Labs, Eric Meyer.
00:37Well, um can you go back one slide?
00:42Sorry.
00:43All right.
00:44Good afternoon, everybody.
00:46Thanks for being here after a long day of talks, exhibits, side effects.
00:52Oh, sorry, that was the side events.
00:54Um I hope that um you have as much fun watching this talk as I had uh creating it.
01:04Um let me first get this out of the way.
01:07This is not a product pitch or announcement or anything.
01:10It's a 20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe.
01:22And I'm sharing all my secrets with you today.
01:25Um hopefully to kind of inspire some of you that next year you will have a booth downstairs where you have kind of like, you know, created a provably safe agentic
01:37harness.
01:39Um or who knows, maybe some of you have already solved it.
01:43Let me know, and then, you know, we can grab a coffee instead of doing this talk.
01:48Um with that out of the way, let's get going.
01:52Um while I was preparing these slides, and I'm sorry that I was multitasking, but I was site five coding on the side.
02:02Um 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.
02:14You can guess which ones were rejected.
02:17Suddenly, wham!
02:20Claude code deleted one of my files.
02:23And I'm sure this has happened to you before.
02:27Um or maybe not.
02:28Maybe you always kind of like, you know, run everything with no permissions, and then you say yes, yes, yes.
02:34But I like to live dangerously.
02:37Um 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
02:51killing us or deleting your files or deleting your database.
02:56So, I think that these models are intrinsically very, very dangerous, and we have to tame them.
03:02So, that's what my talk is about.
03:04Um So, let's kind of like, you know, start this story.
03:08Um 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,
03:23give control of their computers, their finances, their whole personal lives over to AI agents.
03:31And we don't have any protection in place.
03:34Um I think that's very sad and very scary.
03:38Um so, let me tell you the story how we got there, and I will kind of like have some characters uh like Claude, and we will see Dario, Daniela,
03:47Sam, Bernie.
03:49Uh but um the main character is is our friendly pit cloud here.
03:57Um I think you can all remember um November 30, 2022.
04:04This was a kind of like a very special day in in history because this is the first time that you could speak to your computer.
04:11You could say, "Hey, summarize my emails."
04:14And it would you know, um answer you in perfect English.
04:19Um 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,
04:33that that would open Pandora's Box and that would change our history forever.
04:39Um but before we go continue the story, this conference is called AI Engineer.
04:48All right, so we are engineers and maybe we're the last generation of engineers that still understand what this is, what code is.
04:56Um or maybe most of you have already forgotten what code is because all your code is written by agents.
05:03But if we look at this signature here, it says it the LLM takes a question and returns an answer.
05:09The question and answers are not strings.
05:11They are very complicated JSON structures and they get more complicated every day, every time a new release of APIs comes out.
05:19But for this talk, we can just assume that question and answer are just opaque types.
05:24We we don't care about how they look like.
05:27We do care about what they represent.
05:31Um Now, anyway, the euphoria of like these LLMs as being great tools didn't last very long.
05:40And just when we thought that we have eradicated the smallpox of computer science, SQL injection, it came back with a vengeance because the bad guys discovered that you can trick LLMs
05:54using prompt injection and LLMs have no distinction make no distinction between code and and and text and so they're very very easy to trick and this I think is a bigger problem than SQL injection
06:09ever was.
06:11Um but it was not prompt injection only that made LLMs kind of like have a bad rap.
06:18LLMs 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?
06:27How do you synthesize drugs?
06:29How do you hack into people's systems?
06:32And 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
06:43go find a solution for this problem right now AND QUICK.
06:48COME ON, SOLVE IT BEFORE YOU KNOW the the government steps in.
06:53Um 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.
07:07That's this kind of scary on the right.
07:10Look at that.
07:11What does it say?
07:12There's like some sigma Greek symbols, there's proofs, whatever.
07:16Well, that is Lean.
07:18Probably you have heard of Lean.
07:20Anyone here heard of Lean?
07:22Lean is now like the hot thing, right?
07:24Like VCs are are writing like multi-billion dollar checks if you just say that you're doing something with Lean.
07:32And of course these PhD types researchers are using Lean and you have to suffer because of that.
07:40Um now let's first look at the signature in a slightly simpler language called um Daphne.
07:47And what this thing says is that the LLM takes a question, returns an answer.
07:53It requires this question to be proper, which means that it's not an offensive question, and then the model returns a safe uh answer.
08:03And this thing is proved automatically.
08:05So, if you give it a proper question, it gives you a safe answer.
08:09Um Now, I think there's too much attention for Lean.
08:15I'm a recovering type-a-holic and math addict.
08:18Um I love Lean, but there's many, many other theorem provers and uh model checkers out there like Isabelle, Rock, PVS, TLAPlus.
08:30Um but Lean is the grease that got like, keeps the VC money pumps going.
08:36So, I will use Lean um today.
08:39So, here here's the got like, you know, the the uh interface again in Lean.
08:44And now in Lean, you don't do automatic theorem proving.
08:49If you're like a Lean expert, you will say, "Eric, well, we have grind in Lean, but let's got like, you know, put that aside for a minute."
08:55Um 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.
09:06Um so, it's it's slightly different than um the Daphne example.
09:12But if you think about this thing for just a single nanosecond, you will realize that it's impossible to write a formal proof that an answer is safe or a question is proper.
09:25Um and that is why there are at least a hundred startups down here in the exhibition hall that are using LLMs as a judge, because this is not something that you can formally specify.
09:35What does it mean that an answer is safe?
09:38That's not a mathematical property.
09:40Um And of course, if you own a foundation model like these guys, you don't need external LLMs as a judge.
09:47You just um bake it into the weights and you call it the model is aligned.
09:52Um But unfortunately, trying to bake alignment into the model is not foolproof and models get routinely jailbroken.
10:01So, they had to go to the Pope and ask it to get like, you know, um bless their model that it's safe.
10:08Um Now, I think it's terrible if like a model says something offensive, but those are just words.
10:16And ultimately, the words are are like they just like, you know, they drip off your body.
10:21They don't do anything.
10:23Some human has to act on words to make them dangerous.
10:26Um and so, maybe that is what they mean by broadly safe um when Anthropic uh uh talks about safety um because it's still a human involved.
10:38But then something terrible happened.
10:40Something really terrible happened that changed the world forever.
10:45And that is in June 2023, OpenAI announced tool call support in GPT-4.
10:53And of course, all the other vendors rushed out to copy this.
10:58This is called the principle of minimum differentiation and that is why all these APIs uh look the same.
11:05Um Now, the act of adding tool calls changes AI safety from a philosophical debate to something that causes real danger.
11:15You could say tool calls give the model claws in addition to a mouth.
11:19Or you can say tool calls is like handing a gun a loaded gun to them.
11:25But of course, nobody listens to me.
11:29Everybody ignores what they say.
11:31And these guys just went ahead and have shipped tool calls.
11:35They just, yeah, just just do it.
11:41Now, let's go back to like this is AI engineering conference.
11:45So, let's look at what is the difference in the signature of LLMs when they add the tool calls.
11:50And it's just that little IO there, and of course it messes up the the formatting of of the the um uh signature.
12:00But, if you look at the picture, there what you show, now suddenly Claude goes from like a nice puppy to a dangerous thing.
12:08Look, it has all these dangerous tools.
12:10And now it becomes scary, right?
12:12I've never seen anything scarier than an LLM with tool calls.
12:17Um now, if you look at this, this is like a like a small step for a type, but a giant leap for chaos.
12:23Why is that?
12:25And 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.
12:35So, 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.
12:42But, who cares about the safe answer when all my files are gone?
12:46Right?
12:47So, that's why I say it, it's a giant leap for for chaos.
12:51Um again, sorry, this is an engineering conference.
12:55Let's look at this type IO.
12:57And you don't have to understand it, but just see that there's a type there called real world.
13:02Yes, Lean, this is a direct thing, has a type called real world.
13:06And why is that?
13:08Because something of type IO will mutate the real world.
13:12So, it warns you, don't use this because it can make irreversible side effects.
13:19Um like deleting your files.
13:21[snorts]
13:21So, Solomon Heikes um last year this conference called an AI agent, an LLM that's wrecking its environment in a loop.
13:30And I think he's a hero.
13:31I don't know if Solomon is here this year, but I think he should he deserves uh deserves a round of applause.
13:39Um because I think this is the right definition of an AI agent.
13:45Um by the way, this was one of the pictures that I had trouble to generate because it it clearly depicts violence.
13:53And so it's a kind of an unsafe thing, right?
13:55I have a picture that depicts violence.
13:58Um so are we doomed?
14:00Well, our agents have access to private data.
14:03They have untrusted content like the prompt injections.
14:07And now we give them tools.
14:08Simon Willison calls this the lethal trifecta.
14:12Um what can we do about this?
14:14Well, 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 left to the right right right.
14:24This is actually the secret to solving this problem.
14:28The Dutch team got eliminated yesterday, so you have to see me do the dance.
14:34Um but all that we're doing is we're pushing this IO to the right to the right.
14:40And what you now see is that the tool belt of Claude goes to the left to the left.
14:46And suddenly Claude is a nice puppy again.
14:49Because instead of executing the agentic loop, it creates a plan and says here is a plan to do the agentic loop.
14:56And now Bernie will take that plan and will execute it.
15:00And we all trust Bernie, right?
15:02Bernie is a good guy.
15:04All right.
15:06So just to kind of like show it here.
15:08So in some sense what we're doing, we're air gapping the agentic loop from the agent.
15:13So we don't let the agent run the agentic loop.
15:17Before the agent run it, we want to be able to check it.
15:22All right.
15:23Now, the problem is that if you get the value of type IO of A, um that's a really a black box.
15:31And the Lean manual says that if it's a black box, you cannot reason about it.
15:35So, even though Claude now gives us this plan, there's we cannot look into this plan.
15:40Lean doesn't allow us to do it.
15:42By the way, this is another picture, right?
15:44That's that's promotes drugs use and the model let me do it.
15:49I'm a good hacker, yeah.
15:50I can just make it do forbidden pictures.
15:53Um 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?
16:03It creates an an IO of answer.
16:05So, this is a plan to generate the answer, and then it creates a proof that this um that that plan is safe.
16:14And the the nice thing is here that you can get at that proof without having to run the agentic loop.
16:21But, unfortunately, as I said, like this proof, if it's like something of type IO, it's useless.
16:27Ah, What can we do about that?
16:29So, I keep like moving you guys forward, and then we never get to the final answer.
16:35But, there's one last trick, and you see the the researchers here are becoming more much more sophisticated instead of the flat 2D ones in the past.
16:45Now, they're like real people.
16:48Um And what is better than creating a plan of type IO of A is creating a program that represents an expression of type IO of A. Ooh, that sounds very meta,
17:01right?
17:01Um Not meta in terms of meta.
17:05I don't think they're very meta, but um meta in the terms of like you know, like meta.
17:10You You know, you know what I mean.
17:12Um And again, it's a small step for a signature, but a giant leap for safety.
17:21Because now the model returns an expression, a program that represents a computation.
17:27If you know link or C#, you will recognize that this is one of the tricks that I always use.
17:32If you know Lisp, this is of course second nature for you.
17:36I cannot have like you know, have a talk without talking about monads.
17:41So, if you ask yourself, what is this expression thing?
17:44Well, that's just a monad, but it's not just a monad, it's a free monad.
17:48What is a free monad?
17:50It's a monad that loves tie dyes.
17:53Um And now if you look at the the signature of the the property to prove that something is safe, you see that it takes an expression of a computation
18:06that returns an answer.
18:07Um 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.
18:17Right?
18:17So, now we're safe, we're home safe.
18:19And Jeff Huntley wanted to remind you that we can solve the drive factor problem just by doing taint analysis on these expression on these programs.
18:30Okay, this is the last code I will show you because I'm running out of time, but just want to show you here that, you know, you now have a simple inductive recursive interpreter
18:40for this language and you have a simple inductive proof.
18:43And the models can generate these proofs.
18:47So, 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,
19:00then 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 rewrite the plan into a program and a program that we could prove to be safe.
19:17Now, you would say, "Eric, oh, you're a genius."
19:19No, I'm my brain is the size of a peanut.
19:22This is something that's called proof-carrying code and it was invented by academics in the 1990s and I'm just stealing it.
19:30Um, all right.
19:31At the higher level, if you didn't understand the code, three points.
19:36Agents are dangerous until proven safe, so you should never ever let your agents do something unless you can absolutely prove that it's safe.
19:45And the language that this agents generated was not designed like normal users don't understand free monads.
19:53Doesn't matter.
19:54It's a machine that consumes it.
19:56It's a machine that generates it.
19:57It's a machine that proves it.
19:58So, we should stop designing languages for humans and it's all basic, only requires programming 101.
20:05Um, there we go.
20:07All right.
20:08That's it.
20:10Um, the end of the story.
20:12If you're curious to play with this, a bunch of academics, in particular Nada Amin from Harvard, have implemented this.
20:19It's it's there on GitHub.
20:21It uses a slightly different language than what I use.
20:25It uses also a slightly different language than free monads, but the idea is the same.
20:30The language doesn't matter.
20:31It's it's the the principle that matters.
20:34So, 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.
20:53Thank you so much.
21:09[music]
21:12Oh.