Verifiably Safe Agentic Compute | Erik Meijer, AI By the Bay 2025
Recording: Verifiably Safe Agentic Compute | Erik Meijer, AI By the Bay 2025
Yeah. Um, welcome everybody. Um, I don't know if you remember November 22nd, November 30th, 2022 as well as I do. This was the day that chat GPT was released and I think when everything changed and it's quite amazing to realize that that was not even three years ago. Um and before that and after that I think for me everything was completely different at that time I was um running a a large team at Meta where we had like hundred like people with PhDs and like you know in math and statistics and machine learning and we were building models for um developer productivity. Um and then when chat GPD came out, we tried to give it some of the kind like examples that we also gave to our own models and that we were proud of. And then when you realize that this generic model can do better than all these specialized models, you know, something special is happening. Um, and I and I'm pretty sure that like everything that you've done in the past three years was impossible um before that
And yeah, I I just want to get like you to remember how quick things went. Um, but at the same time, I do think and maybe that shows my age and we were talking like before for before this talk about this. Um it's easy when things move so fast and everything is different is to um forget your history and and as the saying goes um if you forget your history you're doomed to repeat all the mistakes um and I lived through a previous um AI hype. This was in the 80s um that was the Japanese fifth generation project. Um if you read the papers um and articles from that time I think they they could have been written yesterday um the same promises like you know like AI will kind of do all our work um these machines they built special hardware too and it was not GPUs but it was different stuff but there was a big difference um right now we're using these kind generic large language models And back then we were trying to use um formal reasoning, formal planning, logic programming, functional programming. So it was a very more um like formalistic approach to AI. Um well I was kind like back then I was doing my PhD and um I was doing my PhD in AI trying to do um natural language processing and the idea was like if we like get a lot of data like natural language data from newspapers from books whatever think like NS archive from the 80s um and if we write parsers for all this this these natural languages. Then once we get once we can parse these languages now we can now we have knowledge then we can translate between English and Dutch and and French whatever and we can really understand language but quickly I realized this is not going anywhere
Um, and I I feel sad for all the people that smart people that did their PhDs um in AI back then because I I think all of this stuff that they did is basically worthless. So I switched to uh programming languages instead. Programming languages are much easier than natural languages. There you can use formal methods. You can write parsers that actually work. You can analyze them. You can translate them. So I worked on that
Um and then in 2017 um when neural nets came up I thought oh maybe this this is a like you know a better approach to AI. So I switched um to do AI for developer productivity. Um when I started that people were asking me Eric are you crazy you're giving away all your teams to do something that cannot work. Um, and guess what? Now everybody is building like some agent to do coding or whatever. But what I say is that that's that's a solved problem. So coding um using AI to code, it's a solved problem, but it's also solving the wrong problem. And hopefully um that is something that like when you leave this talk, you will remember, right? like what I'm going to tell you is that you're doing everything wrong. Um and so now um I'm I'm I have this kind like you know one person lab um where I'm investigating provably safe AI and I will talk a little bit about that
Um and the the two things that I'm working on it's like universalis that's a programming language and automat it's a runtime but the funny thing is that um it's based and and um my lab is called lipns lab because it's based on the ideas of lightn who invented calculus I don't think that um newton did it but like it was lenitz um but anyway like that's the basis of all machine learning that we do today of course, but also back then like in in the 16th or 17th 18th century he was already thinking about using machines to automate boring work. Um so like this is not a new idea. So even in the 80s it was not even a new idea right people have been even the Greek the ancient Greeks were thinking about like how can we use machines to automate human work but anyway as I said what I'm going to tell you is that you are all wrong. So for example um when people strive for AGI or ASI whatever that means. If you look at Meta for example Mark is is paying through his nose um to to buy these kind like super rock stars to chase um AGI. Um well the stock price shows like how successful is it is with that. But anyway, like I I don't think that chasing intelligence that is like human intelligence is very useful. Sometimes I use this examples
I say that you want to build a machine that can stay underwater for long times, a submarine. You're not going to model that submarine um against a whale. Well, a whale is a natural thing that can dive deep underwater. So maybe we can build the whale like jump in its beak into its stomach like in the Bible, right? And then we can stay under water for a long time. But that's obviously nonsense. We built like a machine that can stay underwater for a long time. And that machine is not necessarily inspired by nature. So I think trying to um model intelligence um like against nature I think is is is nonsense
And I asked JGPT that you see that like the M dash and it said yes we're basically apes that lie, cheat, steal um because we needed to survive in like a hostile world but we as humans are not at all rational. We don't use logical thinking. We don't we don't work optimally. So why why would you want to get like model intelligence to be like humans? I think that's that's wrong. Um, here's another example. Um, a lot of people I think when you and maybe I don't know in in this room, but if you read the popular press, um, are worried about hallucinations. Oh, I ask the model a question and it gives me a nonsense answer. Um, or maybe I can do prompt injection
I I put like a a little like hidden text somewhere and now suddenly it gives like a different answer. I think those are the easy problems, right? The model follows instructions it should ignore. That's easy to solve. What is much harder to solve is the opposite problem. Um, say that I want to build um a a an agent that uses workday to get like enter salaries and like stock packages and I ask it to get like you know say oh base salary 100 million and like you know a billion dollars in equity. If you you have a good chance that if you ask this to an agent they will say ho ho ho ho ho that is impossible that those numbers are nonsense. I cannot do that. But um as I just said like you know Meta is hiring people with those kind of pay packages
Um so the model should not refuse these instructions. Um but the problem is that a lot of models are aligned so they are trained to get like not go like outside these boundaries. And now we've kind made these models kind of useless because there will be certain instructions that they will refuse to follow. Um, and I think that is a bad thing. Um, and again, I think I'm probably one of the few people that thinks that's the case. Um, but another way to look at that is when you um make models aligned, which means that you have them refuse to give answers to certain questions, you're introducing tree valued logic because now the model can say something that's true, which is great. It can say something that's false, which is fine because I will show you how to validate that. But it will also say I don't know or like I don't want to
And this is like like having three val logic like in in SQL. And I know that we all love three valued logic in SQL. But now behind like you know under the covers behind the back door we have reintroduced three valued logic into our agents because of alignment. All right. So how can we deal like how can we solve this problem where models give wrong answers? Well, we know how to do this in the real world. Many of you still work at companies and if you come to this conference and you want to expense um the fee the conference fee you have to submit an expense report and then probably as evidence that that is a real expense report you have to hand in a receipt right now that is like a pattern that we use a lot. So in order to do some action, you have to also pro provide evidence that that action is real or true. And often providing that evidence is harder than checking that evidence because for whatever administrator that looks at your expense reports, that's easy to check
Oh, like the amount on the expense report is the same as the amount on the receipt. But you had to do all the work to get the receipt to don't forget the receipt. this conference had to do write software to kind be able to generate receipts. So it's it's an asymmetrical situation. It's much harder to create the evidence than to check the evidence. And what you see now also that models when you ask them a question like who is head in the box, they provide evidence. You can check whether the answers are correct because they give you hyperlinks, citations that you can check. And sometimes they give you wrong answers with a hyperlink that you can check to see that they're wrong
I wish I had like beautiful hair like that dude. All right. So then the other thing I think where I'm I'm puzzled is that people are funding and spending billions and billions of dollars to build like new foundation models, bigger models to chase this like general intelligence where what I think is that these models are probably good enough and what we really need is we need a new compute platform that is built on top of these models. So right now we have like Java or Python or Go orNet. These are all compute platforms that are based on often like a a virtual machine. Even Python has a VM underneath, right? And then like an ecosystem um of package managers and stuff like that. And now with AI, we have a new compute paradigm. And so what we need is we need like new tooling and and like new programming language
That's the big difference. That's the big problem. Not like you know chasing more models. Um like just with CPUs there's like three or four CPUs that everybody uses. I think that's the same with models. We don't need 10 different models. Like just having a few companies create new models that will be a commodity just like CPUs and then the value is created on top. But hardly anybody is working on that
All right. So when I get like handwave saying like oh these neural networks are like computers. Um I think the the analogy is quite striking at least for me. So if you look on the left that's the traditional computer and on the right is what I call the neural computer. Um so the weights of a um neuronet that corresponds to the ROM the readonly memory of of a traditional computer. The RAM that's your context. Um now everybody's talking about context management that's important. Well if you're using an operating system you have virtual memory because you don't have infinite memory
So you have to manage your memory. So that's context management. There's nothing new there. People say, "Oh, context management is like the hottest thing." It's like we have been doing [ __ ] context management since the 1950s. Um, because it's just virtual memory. All right, instruction set tool calling and and so on. So there's really like, you know, very close correspondence to traditional computers and um what I call neural computers. And the the model itself really is just like a tiny part of that
It's really like the branch predictor in a CPU. What does the branch predictor do? It looks at the instructions it has executed so far and then it predicts the next instruction. Well, that's exactly what an LLM does, right? So, an LLM is just a branch predictor in this new neural computer. Um then the other thing I hear a lot is oh like rag is dead or like you know like you only need um more compute for inference. Um but I don't think that's that's right. In order to build useful things in order to have like articulate sentences you need nouns and verbs. And so you need data and you need tools and and both are equally important. If you if you have like only one, you cannot build um anything useful
Um so this is my vision. Um so what I want to build is like the programming stack for the for the for the AI era. And on the left I use like .NET but you can of course you can substitute Java, Python, Go, anything in there. And just like the the machine has all this correspondence this this stack um has also like a correspondence and there you see the like automat that's the runtime and universal this is the programming language or reasoning language we need like something like a package manager to have like you know to share like code that people write um and then just like in the past like you know write once run anywhere this thing should run on different models, prompt ones, um, run anywhere. So, this is what I'm trying to build. Um, whenever I try to pitch this to VCs, their eyes glaze over and they say, "Oh, this guy is crazy. Should I call like a mental institution or something to have him admit it?" Um, but I I still believe everybody's wrong except me, which is is I think um maybe a sign of of mental illness. I don't know
All right, let me give give you another example where I think everybody is wrong. Um, if you're a functional programming geek, and maybe there's functional programming geeks in the audience, you really like, oh, look, you don't need anything. I can do everything with functions. I can even do numbers and arithmetic with functions. Like, look, here's church numerals. Like zero is this function like and then I can do multiplication and so on. That's really cool. if you're theoretical computer scientist or a functional programming geek, but it's horrible for performance
So, every computer has special purpose circuits circuits to do arithmetic. Now, in models, you see the same thing. People are trying like, oh, we're going to teach these models how to do arithmetic. Oh, how cool. That's complete nonsense because why would you want the model to do arithmetic if we already know how to do it? You should teach the models how to use tools that do arithmetic, right? Instead of teaching the models to do useless stuff. This is as stupid as using church numerals. [snorts] And um now I'm not the only one that thinks this. There's like this theory of the extended mind theory that says that intelligence is not just in the brain
It's really also in the tools that you use. And that's true. It's like look at this beautiful building and we this is part of our intelligence. By having this building and meetings like this, we can like you know can share ideas and we become smarter. So this is like being here in this building is an example of extended mind theory. All right. So what I'm saying is that the the models are not that important. It's using tools that's important
So and these models should just orchestrate tools. Um here's another um exom that I use and sometimes people say, "Oh, Eric, this is a little bit extreme." But I I do believe in it. Um is that ultimately we will be in between the AI and its objectives and it will kill us. And then you say, Eric, but that's a little bit extreme. But if you've ever used AI coding assistance and you have tests and it cannot make the the code to to pass the tests, the model will start to kind like reward hack. It will start to delete your tests. You must have all seen that, right? But it's the test now. Tomorrow it's us
All right? So, what I'm saying is that let's keep it really simple. You should never ever trust a model. Okay? Like always assume that the models are malicious. Um, and then you work from there. And I'll show you what we can do about that. But that's I think a good assumption like the model is always trying to [ __ ] you over. Excuse my word. All right
So here's another maybe a a slightly more polite way to show it is like you know like Simon Wilson's like trifecta. If you have untrusted content, prompt ejections, private data, and ability for the model to communicate with the outside world, bad things can happen. All right. But why do bad things happen? Well, here the assumption is that it's probably the the people that put the untrusted content in there that do the prompt injections that cause the bad thing to happen. But of course, it could also be the model, right? The model can try to like, you know, make this happen. So, but again here, like you should never trust these things. These systems that we're building can do real harm. Um now one solution that we're that seems to be in fashion is well then let's use another model to have like you know judge the output of the of the previous model
Well that's great. It's like you know like the fox guarding the hen house. It's like the judge kept like you know being the jury. I think that's yes it's easy but it's nonsense. This will lead like the model if the model is really malicious it will of course like you know do what's good for for itself and not for us humans and now again like looking at history we have solved this problems this problem like I don't know like thousands of years ago you know you have to have separation of powers um and so not the same person should not be the judge and the jury at the same time So this is a principle that our society uses and makes it work. So we should use the same principle uh for our models. Um third principle that I'm using I already mentioned this is this separation this asymmetry between producing evidence and checking evidence. So it's always easier to check than to prove
And this is also something we already use with cup jazz for example. Although cup jazz they are they are their use is to keep humans out and the idea was that it was hard for machines to solve them things have turned around now since um November 30 2022. So what we need is the opposite of a copcha to keep the humans out um and to let the machines in but we should only let in the machines that have good intentions. All right. So how can we do this? I have five minutes so I'll kind of give you the the answer here. So how can we solve this right? So how can we build the the the the duel of a capture that is like you know like is not meant for humans it's meant for machines but it's only allowing the good machines to go through. Well the way to do that is that the models generate an artifact that can be inspected independently. So it should be inspected not by another model because that would be like you know clash of and not separation of concerns
it should be be able to be validated by something externally um that that artifact is safe and then as a side effect we see that this also kind of like improves reasoning and and um uses less tokens um and people have like figured this out. These are like recent papers and that kind of follow if you have the model kind of think in code it suddenly will kind like think better and it will be cheaper. But I think what these guys are missing is the real benefit namely if the model thinks in code and it produces code you can inspect that code and you can prove properties about that code. In in fact you can prove properties to to show that that code that the model produced is safe safe to run. it's not going to hurt you. All right. So that's kind like you know let's call it guard or whatever. And so this is the the architecture of my my uh virtual machine
So the user asks a question and then you generate a spec in a language that that language is universalis. So that spec is also vioded right like I don't expect humans to write that thing but you write the spec but that spec is your contract between you and the model and you sign off on that spec then the AI given that spec generates code and a proof that that code satisfies the specification right and doing that proof is hard and this is why we don't prove our software except if like for like a nuclear reactor or something because proving correctness of code is really hard but these models are really good at that. So we let them do the hard work and then checking the proof is easy. Um so we have a verifier and note that you don't need to trust the code. You don't need to trust the proof because the verifier is not a model. verifier is something that we trust, right? That is something like, you know, like lean or some a improver that we kind of trust. It's not another model. And then we can run it and maybe we need to do some checks at runtime because not everything can be valid be validated statically
Now, if you know how the JVM works or net works, it's not very different. This is just byte code verification. If you load bite code into the JVM, it verifies that this bite code, it only checks memory safety. Um, and then, um, it runs it, but it also needs to do some runtime checks for array coariance, for example. So, I'm not proposing something like new. It's just like, you know, a different way to do bite code verification. I have only one minute. So I need to get like tell people that another thing that they're wrong
Python seems to be the winner here. I love Python. It's a great language for humans. Okay, it's designed for human ergonomics. It's not designed for machines. Um if if Python has significant white space that's messes up with token use, it's designed for machine efficiency. I don't know if you like use slots or like lazy imports or C interrupt. These are all things that are have nothing to do with AI
These are built for for traditional machines. And lastly, they are designed for flexibility. So in Python, you can do monkey patching, import can do anything. So it's impossible to reason about a Python program to reason about its correctness. And that's why we need um a new programming language. And I'll leave it um at that because I'm out of time. Um but my programming language is basically um prologue um is like logic programming with like natural language um infused and now your specifications are in the same language as your programs. and and the model can kind of like you know produce these proofs and we can use a traditional T improver to prove that the code is correct with the specification
So that's my talk. Oh the boss says okay good that's good we still have humans here. Um so here's another thing that I think um we we are wrong. we often kind of become extremist like oh suddenly like chat interfaces are like the hype and I think chat interfaces are great but traditional UIs were there for a reason because sometimes you don't want to get like type stuff in you just want to click from a menu or click some message boxes so um what what I do is I have hybrid UIs where the the when you communicate with the system it might generate like a traditional UI on the fly. Um, now this is also like copied now. Other people are doing it. CL code also has this hybrid UI, but they do everything with text. But again, like you know, it's not a pure chat interface anymore
There's also like a UI. It's just a matter of time before people say, why do we have to do these text UIs? Can't we just have like real menus in there? So just wait a few months and cloud code will have like real menus in there. Um now the implementation of my system is also interesting. Um I used to have the model generate um source code universalis source code but of course these models are not trained. They don't know universalis. So they would always generate bad code. So what I do instead I have it generate JSON as of the language. And with structured outputs, you just give it a schema and now it will always generate syntactically correct code and then I just kept like translate it into userfacing syntax
I kept like you know generate deafne for verification and I use Scotland for the runtime. Um again this is not an a new idea. This is called intentional programming. People have been chasing this um for ages as well. Um this will be the last thing um so one thing that I think is my biggest open problem um is that if you look at traditional design by contract these are like if you look at definely like pre-post conditions that that is meant to to talk about correctness of code but it's not really meant to talk about safety of code and and not about like you know safety about like enterprise things. Look to go back to the example of your expense report. If you have an agent that hands in that deals with your expense report, you don't want that agent to commit fraud and then you will be fired and go to jail because it kind of expensed like $10,000 for something that you never spent, right? So you want to be sure that this agent when it submits an expense reports that adheres to the rules of your company with respect to expense report. So we have to somehow have to like express policies like corporate policies in such a way that we can reason about that that AI can reason about that that we can generate kind like proofs of programs that they satisfy these these rules
Um, and I I think that's a little bit of an unsolved problem. So, I I'll I'll I'll leave it Here it