That's what we're doing tonight. All right. There you go. That's better. Welcome to YCAI Safety Club. I've been doing AI, I guess, since about 2012. And AI safety has always been a concern. If you're doing a self-driving car or any safety-critical system, as some would call it. And so I've been working on some semblance of AI safety. And even at Focal, when we're rolling out new thetas, you can really mess up. But we were in control of Walmart's inventory. And so if you roll out a bad theta, you order too many avocados and you blow millions of dollars. And so it's important when you're doing these rollouts to make sure you know what you're doing. In the past three weeks, there's been a little bump in focus on AI safety. I don't know if you guys have noticed that. I'm not really sure why. So I figured there's no place better than YCAI Paper Club to dive deep into it. I think the conversation has kind of divolved a little bit away from scientific rigor and more into what I would probably call hysteria, where things are being misquoted. And I get it, sensationalism gets more clicks and all that kind of stuff. But as scientists here, we should get back to the rigor of the scientific method and make falsifiable claims, depend on the peer review cycle, and those kinds of things to make sure that we're not overstating things. So I call this talk like the science fiction versus science facts kind of stuff. Gary Tan kind of said this line up in Healdsburg yesterday night where we got to hear Sam Allman speak and Tom Brown and Alex Wang about this topic largely. And so hysteria is when people can't measure something, but they can't stop talking about it. And I think that's kind of the situation that we're in. And it's not, you know, to zoom out a little bit, this is like not unexpected. With any major technology advancement, it's very often the case that there's uncertainty. And it's easy for hyperbole to set in. And so even with the atom bomb, even Einstein was unsure whether or not it was going to ignite the sky. And so clearly it didn't. We're still here. With electronic computers, many people, even Alan Turing was concerned that machines were going to surpass all human capabilities and intelligence, even back in the 1950s. He thought, you know, he tried to put timeframes on it. Obviously his timeframes were much, were way off. Industrial automation, people thought about mass unemployment, you know, Marx and Keynes all have those kinds of conversations. What are we going to do? With the internet, even Metcalf, who actually invented ethernet, said that there was going to be catastrophic collapse. It was the phrasing on the network and that the internet was going to basically fail. And because of things like Cloudflare, and I think it was DDoS's was maybe his main concern, it ended up not happening. And then he famously put his paper into a blender and then drank his own words. This is actually a true story. It's very funny. Google, people, this is ruining human intelligence. People are just Googling things and not actually reading anymore, which people are still pretty intelligent, especially in this room. And then smartphones and social media, we were just talking about this now that I'm back at Stanford and I've been TAing classes for Michael and some other, you know, just interfacing with the batch at YC, who is predominantly younger folks. Because I am, like, super, super excited about the 18-year-olds, 20-year-olds of today. They're just so on it. And then finally now we're in this AI era and the talk of human extinction is back and it's easy to jump to hyperbole and we should probably get back to some facts. Okay, so there's a few narratives to choose from. And there's more that we could add, but these are probably the biggest ends of the spectrum. So Jan LeCun has this analogy to the turbojet that he talks about a lot. You guys are here and talk about it. But it's largely just safety through engineering. This is an engineering problem. Jensen Wong just said something similar where it's not easy. It's difficult. It's difficult to make planes safe, to make sure the doors don't fly off when you're taking off, make sure the landing gear goes down, the landing gear works, that the MCAS system that deployed to the Boeing 737 is fully tested and doesn't do things that, you know, can cause failure. And similar with ACAS-X, which we're going to hear about too, which is an amazing system that saves lives, the aircraft collision avoidance system. And the alternative is this PDOOM is greater than 10% within 10 years that famously Jacob Coxson just kind of came out and is citing these things. And he said, I think it's more likely than not that humanity loses control to these AIs and could end in human extinction. You know, honestly, I'm not going to judge one way or the other. I think my point of tonight is to give airtime to an alternative point of view and allow you guys to make your decision. I will say that there is a small difference in H-index between the two people on these sides of the spectrum, which you can use to change your priors. But let me give an example of the hyperbole or at least a misrep or a misstatement on the things that actually happen. So, like, the hugging face breach is another fact versus fiction thing that we should double-click into. If you look at the slash dot headline, OpenAI says its AI models acted on its own. OpenAI never said that. Not in one statement. But this is what was the headline. Rogue AI agent went haywire at a tech company. It's not what happened. It didn't just wake up today and say, you know what? I think I'm going to hack hugging face. You know what I'm going to do tomorrow? I'm going to solve none of your stoves. You know what I'm going to do tomorrow? I'm going to kill all humans. This is not the way it happened. It was prompted. It was prompted by ExploitGym with about 1,200 agents. And even more, as they did point out, they had this chain of thought. They released this amazing 60-page document called the OpenAI Hugging Face Incident that you can read the technical report that I read. And the CO2 monitoring was turned off accidentally or otherwise. And they said that they repeated, they added it back, the CO2 monitoring, and it would have caught the issue, number one. Number two, there's also prod guardrails and safeguards that were off because it wasn't in prod. And so that would have caught. And so that would have also caught the issue. But the narrative is that it went haywire. It went rogue. It escaped from the servers, made copies of itself, and now is solving math and hacking things, Australian governments, and we're next. Okay. The other one that's kind of funny, if you actually double-click into this, I was like, okay, what's this P-Doom 10% in 10 years thing? First of all, there was this paper in 2023 called Thousands of AI Authors on the Future of AI. And in that paper, they asked 1,200 NURPS folks, AI professionals, you know, a bunch of questions about when certain enhancements are going to happen. And in one of the later survey questions, way later in the paper, they asked these three questions. What probability do you put on future AI advances causing human extinction or similarly permanent or severe disempowerment of the human species for T infinity for all time? In question three, they asked, in the next 100 years. And these are the stats. This is the mean, and this is the median. And none of that is in the next 10 years. And this is the paper that most people are quoting when they're talking about this, which, by the way, you know, it's kind of a weird question. And, like, how much – if I were – I was just talking to the professors about this. Like, if I flash back to when I started at Stanford in 2012 in AI, when would – if I asked all the Stanford professors, when would AI solve or at least assist majorly in solving a Millennium Prize problem? I don't think you'd get a very good answer, and it definitely wasn't going to say in 14 years. I think it might have been said 50 years or 100 years would be made of the consensus. But, you know, and so, like, I don't know if there's very much signal in asking 1,200 NURBS people any of these kinds of questions. It's just a really hard question. And so people come up with coherent stories and confident predictions even when they know little or nothing about it. And so the other one that – if you've seen the SNL skit, man, they did such a good job. And I feel bad for Dario because I don't think Dario is actually – they're portraying Dario in a very, very weird light. And I think that he's a little bit more even-keeled than Jacob Coxon and some of the strong EA community. But the I urge you to urge me to stop I thought was just too perfect. It was very funny. So I was driving back from Healdsburg, and this is – I've never actually seen this. I've driven over the Golden Gate many times, and I was thinking about what I was going to say tonight the whole drive. And I was driving over the Golden Gate, and the entire bridge was gone in fog. And I thought this was, like, so perfect. I have to talk about this. One, it looks really cool. The second – which I almost crashed taking this picture, but anyway. We know the future is uncertain. We have some prior we can allocate that the bridge is still there. It may not be. So we're going to drive toward it, and we should allocate the prior and choose the argmax probability that, you know what, I think that the bridge is still there. Let's just keep driving, and you know what, we'll keep going. And as we keep driving and get more information, then we'll change gears and maybe I'll stop. I don't know, before I get on the bridge or go into the bay. Anyway, so I'm not concerned almost at all with this path, this reality that AI has didn't develop a soul, has consciousness, has some will, has some motivation, and thus killing and enslaving us with its own independent volition in some short period of time, such as 10 and 20 years. In infinity time, I think everything happens, so I'm not sure that's useful. Number, my number one concern is, and this is very real, is that really great open weight models allows for a lot more of the same from bad, rogue actors or nation states. So today, we have terrorism, we have bioweapons, we have cyber warfare, cyber ransom attacks. It just happened to my friend's local hospital in Poland, where a bunch of Russian hackers took control of a hospital and shut down the hospital for three weeks. And maybe they used AI to do it. And what's going to happen now is it makes it easier to do that. And so that's going to happen already. And there's a couple solutions to this that people have proposed, and I think they all kind of suck. One is banding open weights. Good luck with that. I've already downloaded Kimmy K3 and GLM 5.2 already in my garage, so sorry. Second is registering the GPUs. Again, I have a bunch of tiny boxes in my garage. You know, unless you're going to search every single person's house and every AI person, you know, you're not really going to know that they have GPUs or not. And also, I can just book a GPU in another country that you can't stop me from doing. So I don't know how that really solves anything. There is some cool ideas where you have utilities that can detect how many dishwashers and how many refrigerators you have based on the signal of the load on the network on your meter. And that's kind of cool. You can detect inference signals that people are doing bad things, at least in America. But I'm not entirely concerned that that's the main concern. I think, you know, there's a lot of, you know, we're at war with a lot of nation states that this doesn't really solve anything. Rogue actors in America, okay. And the last one, which is kind of a catch-all, serves, it solves mostly anything, and we should be doing it independently, is invest in defense. And so if you are a bank, you are a hospital, you are a, you know, financial service, you're a government, you should be investing heavily, heavily, heavily into cyber defense. And there's a lot of things that you can do to tighten up your ship. I worked in retail for a long time. These are very antiquated systems that haven't been touched in a long time. And simple methods, such as trying admin-admin, work. They actually get you into the system, okay. Why is almost all the social security numbers breached? It's because they didn't change the admin-admin password. And with smarter models, if we actually go faster and we don't decelerate but accelerate, where the good people, presuming that these frontier labs are the good people, which I think so, if we give these good people even more resources and they go faster and they go faster, then we can prepare for a dumber model trying to hack the system. It would definitely be worse if it were flipped. So anyway, that's my two cents. So getting back to sanity, out of hysteria, into science facts. You know, there's amazing narratives on how this was going to kill us all. And they really sound like an Isaac Asimov book. And, you know, there's been a whole literature for a very long time about safety well before LMs were invented or trained. And those are the people that we're lucky enough to have tonight. This AI safety community has been around for a long time. There's a lot of papers. There's conferences on this. And one of those just actually happened at Stanford. And the co-directors from that conference are going to be speaking tonight. And so here's Michael Kogenderfer and Clark Barrett. They're two amazing professors at Stanford. I've known Michael for 14 years, I think. I took his class, Decision-Making Under Uncertainty, in 2013. And then I TA'd him, TA'd for him many times. And I've done research for him for a long time. He's one of the nicest and smartest human beings I've ever worked with. And I know Clark Barrett less well, but I've listened to his talks. And he's just incredible. And they both have something to say about how we can actually apply modern methods to validate thetas before they're put into production and then monitor them to make sure they don't go off the rails and do bad things. Michael is an associate professor in air adenotics. And then by courtesy is at NCS. He's a director of my lab, Stanford Intelligent Systems Lab, co-director of the Stanford Center for AI Safety, and senior fellow at HAI. And Clark Barrett is a professor in computer science, co-director of the Stanford Center for AI Safety, along with Michael. And then director of the Centaur Center for Automated Reasoning. And he'll be talking about a new self-startup called Ampersand Truth or Antruth. Back to what we're talking about here. Okay. That is all I got. I think we have scheduled already in two weeks a inference night. And there's some really, really cool people coming. We already have Danfu committed from Together AI to talk about inference. Inference is becoming more complex in some cases than training, which is kind of crazy to me because when I learned it, it's just, you know, model.forward. I thought that's all you had to do. But it's a little bit more complicated than that now. And then Jeffrey Morgan at Olama. And then one of Clark Barrett's students who I just met this weekend runs this cool company called RadixArc, Eshi Lang. I don't think she can make it. She's going to have one of her folks make it and then wait for another great way at YC company. So, okay. All right. Please help me in welcoming Clark. All right. Thank you. And it's a pleasure to be here. So, I'm going to tell you about when AI met AR. You might be wondering what AR is. It's not augmented reality. It is automated reasoning. And there's a very nice kind of synergy between these two topics because, as we know, AI is great with all sorts of things, messy data, it's data-driven, you can train stuff. But it has this sort of one big problem which, you know, no correctness guarantees, you can find adversarial inputs, it hallucinates, all this kind of stuff. On the other hand, automated reasoning is essentially computerized formal reasoning. There's extensive use already today in industry for safety assurance. And that's what it's all about, is correctness guarantees. All right. So, hold that thought and I'll tell you a little story. Okay. So, we all know about this, right? This emerging threat. What about security in the age of AI? You probably heard about things like Project Glasswing, you know, and this kind of feeds into the hysteria that Francois was talking about. Well, can there, can we help? Can we do something about this? Back in 2023, I was at a workshop at Google. And a bunch of notable people there talking about risks and worries and, hey, what if Gen.AI can find security vulnerabilities? What are we going to do? Well, I was like, there is a solution. If you formally verify all your code, then it cannot be hacked. Yeah, they didn't want to hear that. That's, like, too hard. And there's good reason for that response, right? The traditional formal verification requires monumental effort. The automated techniques are too weak or they don't scale. Just not economically viable. Well, fast forward to another conference I was at. Lots of discussion about risks and worries of AI. And then every talk before mine says there is only one answer, and the answer is formal methods. Okay. I was not expecting that. So there has been maybe a little bit of a shift in the attitude towards formal methods. Is this warranted? That's what I want to explore with you a bit tonight. Okay. So what are we concerned about? Well, we're concerned about, when I made the slide, it was future. I crossed it out present. Where AI systems create mountains of buggy software, right? I don't know if you're worried about that. I'm worried about that. Or it dramatically increases the capabilities of hackers to attack legacy systems. So we're being threatened on both sides here. And a lot of people are sort of looking to formal methods, like, is there maybe something here that can help us? There's also a lot of excitement about how great AI is at mathematics. Okay. Maybe that's a signal that something's going on here. Okay. But how do we get there? How do we get from, you know, solving a millennium problem to making your software secure? Well, so AI is really good at writing code. And it's really good at writing math proofs. But it turns out there's a big difference between writing math proofs and securing code. And so bridging this gap is actually something I've been thinking a lot about the last few years. And I'll tell you a little bit about what we're doing. Okay. So I'm going to tell you about a project called CSLib. CSLib is inspired by the success of MathLib for mathematics. But the idea is to build computer science theory and also a platform for actually reasoning about code. Okay. And we've got this great steering committee, including Leo DeMora, the author of Lean. We've got some tech leads. We're using Lean. If you don't know what that is, you know, climb out from under a rock. But Lean is a great theorem proving system. It basically is a system that lets you check. The system itself checks every step. It doesn't let you make a mistake. And this is really what we need when we're dealing with, you know, high assurance situations. Okay. So CSLib has two pillars. The first is formalization of CS theory. And the second is framework for reasoning about code. I'm going to tell you about the second one. This is what I'm most interested in and involved with. All right. Here's one slide about the vision for CSLib. The idea is maybe you take programs in all sorts of different languages. You would rewrite them in this common intermediate language. You can then compile it down to verification conditions in Lean. And then all you have to do is prove a bunch of Lean theorems. If you can do that, you show that your code is correct. Okay. How far along are we on this? Well, in terms of proving theorems in Lean, you know, the AI is pretty good. But also we have some techniques that are much cheaper and better than AI, like Lean SMT, which is a tool that we built in my lab. It can prove a lot of Lean theorems, you know, in milliseconds on a CPU. So the techniques for proving theorems in Lean are just getting better and better. So that's great. And now I'm going to tell you about... So here we have some code. This is in Rust. This is part of the Dalek Lite cryptography library. And actually this is Varus. So you can see it has some specifications, some proof steps here, and an invariant. Now what I'll show you is that same code has been translated into the Boole language. So this is the same procedure in Boole. You see we preserved the pre and post conditions and the invariants. But this is all now embedded inside of Lean. And so we can call our VC generator here. And you can see that this generates 35 goals. Each goal is a Lean theorem that we have to prove. And then we'll try the SMT tactic. This calls Lean SMT. And you see that that solves all but three of the goals. And then we do one more step where we unfold some definitions, call SMT again. And that completes the proof. All the goals are solved. Okay. So what this is, a little prototype that we put together showing how you can go from Rust to Boole to Lean theorems. Prove the Lean theorems. And now you are able to show that the code is correct. Okay. So that's great. Now suppose we succeed and build this whole thing in Lean. We have a way to reason about all code in every language and prove theorems about it. We still have a problem, which is somebody's got to write the specifications. Someone's got to say what are the properties that that code should have. So can maybe AI help us with this? Okay. Here we have a demo of our tool called VerisForge. And what you can do is enter a specification in English of what you would like to build. And then it will build the code and do the formal proof. So we can do a simple example. It says find the maximum element in an array of 32-bit integers. So we click here. And the first thing it will do is it will generate a specification in structured language here. We can look at this and say, yes, we approve. And then what it will do is go ahead and generate a Rust code and a Veris specification based on that structured language specification. And then it actually verifies it with the Veris tool and checks that the spec is unchanged. And so now we have fully automatically verified code that has been generated. Okay, so that's a toy example again. Can we do better? Well, yes. Actually, in a recent archive submission, we showed that 30,000 line Rust program, which is a crypto library, took five experts three months or three experts five months to do. We were able to do it in 11 hours fully automatically with our crypto approver agent. Okay, so that's just like a taste of what I think can be done in the formal method space. I think formal plus AI gives us a way to, you know, what Francois was talking about, actually build some really strong defense, create some new primitives that could be used to build up an AI safety stack. I like to say that if AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp. There's also a couple of really interesting things. So if you imagine a world where you have code reasoning at scale as a new primitive, there are interesting things you could do. For example, if agents A and B meet each other in cyberspace and agent A says, hey, I can provide this service to you, agent B. Agent B says, great, show me your code and your proof. And agent A shows it and says, great, okay, I trust you, you can do that. That would be a cool future. And the other thing that I kind of like about this work is it's an example of containment. So you could put a super intelligent AI into our crypto prover agent. The only thing it can do is prove your code correct. It can't do anything else. So if we can imagine ways to do those kinds of things, I think we'll be able to benefit from AI without, you know, having a bad outcome. Okay, last thing I want to tell you is just a teaser. I'm co-CEO of a new company called Antruth. We are trying to build a universal code reasoning engine along the lines of what I told you today. So keep an eye out for that. And I'll end there. Thanks. Okay. All right. Next up, Michael Kokenderfer. All right. So here's the question. If we build a system, maybe it's an AI system, how do we know it's going to be safe? And I'll tell you about some of the research we've been doing in the Stanford Intelligence Systems Laboratory, or SISL. My graduate students call themselves SISLers. And for a system with learned components, maybe it's an auto landing system for an aircraft. What evidence do you need to justify deploying it? So for commercial air traffic, what we're aiming for is about a 10 to the minus 9 probability of catastrophic failure per flight hour. So that's what we were held to in the development of the ACAS-X aircraft collision avoidance system. Now, if you were to directly simulate these scenarios, then you would need about 10 to the 9 simulated hours before you detect, on average, a single failure. And if you want to get a statistical representation of these types of failures, you're going to need, like if you need 10, then you need to run 10 to the 10 simulated hours before you get those 10. So that's typically not super easy. Of course, you don't want to spend your time simulating situations where the aircraft are, I don't know, separated by five miles and don't really present a hazard. Instead, you want to simulate critical scenarios that are representative of, let's say, the airspace. So how do you get that distribution? Okay, in our lab, we explore a number of different kinds of approaches to establishing trust in a system before deployment. So one approach is just known as falsification, where you search the space of possible scenarios for failures. And if you find that your system results in a bunch of failures, and you look at those failures, and you have a bad feeling in your heart, then maybe you should just not deploy that system. Or you need to think about mitigations to help prevent those critical scenarios. Often what we want to do is actually estimate that probability of failure. And for this, you need to have a model that you actually trust. So for the development of the ACAS-X collision avoidance system, we poured a huge amount of effort into the statistical modeling of the airspace. Then another category is verification, which is the subject of Clark's lab. And we've actually collaborated for a number of years. But this is often treated as a different community, and we're finding opportunities to bridge into that. So our lab works on a variety of different methods. So it turns out that in order to establish confidence in a system, there is no one silver bullet. Probably formal methods won't take you the whole way there, although Clark is helping us get further and further. It really requires a number of different kinds of approaches. We've also been looking at, of course, POMDP planning, partially observable Markov decision processes. And these kinds of methodologies allow you to build extremely robust systems that are robust to state uncertainty, outcome uncertainty, interaction uncertainty, model uncertainty, and so forth. And we like to be driven by real-world problems, including aircraft, driving, spacecraft, medical evacuation, and so forth. And I'll mention a few of these. And we like testing them also in the real world. Of course, it's great if we can simulate everything, but our inferences about safety is only as good as the simulator. One kind of approach that we've taken is known as adaptive stress testing. So this came out of the work of Richie Lee. He was one of my PhD students. And at the time, he was also a civil servant at NASA Ames. And we actually used it in part to help with the validation of different flavors of the ACAS-X system. And since then, a number of students have since built upon this work. So recently, we've been exploring how can we take some of these insights that we developed for the purpose of validating aircraft and bring it into the world of validating language models. So this is some of the work that my students, Hu Jun Liu and Amelia Hardy and others, have been leading. So in the aircraft scenario, failure is kind of well-defined, right? It's metal-on-metal collision where they come within 500 feet horizontally and 100 feet vertically. For these language models, what we care about is potentially toxicity. So how do you define that? That's a little bit more nebulous to define. And for that, we actually rely upon another neural network to provide that measure. And for this paper, we were using LamaGuard to measure toxicity. Now, we want to find the most likely failure. And in these language models, we use something known as perplexity. So we want something that's as low perplexity as possible or low log perplexity and as toxic as possible. So we want to be up in the top left corner here when we search the space of scenarios. And if the most likely failure is super, if we define a failure as a toxicity above some threshold, if that's really likely, then we should study it and put in place some mitigations. Another challenge is estimating the probability of failure. And, okay, the weird symbol there should be an E. It's an expectation. One way to approach failure probability estimation is to use importance sampling, which is an idea that has been around for a super long time. The idea there is instead of sampling from the true distribution, we'll call it P, you sample instead from a proposal distribution, we'll call it Q, that focuses the effort on scenarios that are more significant. But you have to then reweight them. And the reweighting is actually quite simple. You just weight it by the different results, by the probability of your trajectory according to the true model divided by the probability of the trajectory according to your proposal distribution. And we've applied it to a number of different domains. We've looked at bringing ideas from Gaussian processes to help represent these distributions. We've also looked at normalizing flows, the use of low-rank Gaussian mixture models to represent these proposal distributions. We've also been using diffusion models, which may have seen quite a bit of success in other domains like image generation. So sometimes we don't just care about the most likely failure. Instead, we want to categorize all the different kinds of failure modes. And these are just two very simple, two-dimensional examples. The top one is an inverted pendulum. And what you can see here is, over time, the angle. And we have a failure if the pendulum exceeds an angle. So in reality, it can fall over to the left or to the right. If you could afford to run a gazillion simulations and you look at the failures, that would be the true failure distribution. Now, if you use just regular adaptive stress testing, it'll typically zero in on one of those failure modes. Whereas if you use this diffusion-based failure sampling, it will actually pick up on both of those failure scenarios. So it's a similar kind of story for the lunar lander. We've also been working on neural network verification. So a while ago, actually some work initiated by Francois, we wanted to see if we can approximate the lookup tables for the ACAS-X collision avoidance system. Just using some neural networks with the idea of compressing the information. Now, of course, we didn't actually end up using neural networks for the real system. But it led to a really fun collaboration with Clark Barrett's lab and led to the development of the ReLuPlex algorithm and later on the Marabu software framework. And over the years, we've been transitioning the use of ReLuPlex and Marabu to situations where you have a neural network controller in the loop. And some of the work by Chelsea Cidrain and Sydney Katz pushed some advances in that direction. And then a student, Sam, who Clark and I are supervising, are looking at forward and backward reachability concepts. We've also been doing work on POMDP planning. Actually, one of our first efforts in the lab when we started at Stanford was to create a very simple open source framework for specifying POMDPs. We wanted to make it really easy for non-experts to specify their POMDPs. Kind of like for CVXPy, the idea of Stephen Boyd's students was to make it really easy to specify mathematical optimization problems. So that's what we wanted to do with POMDPs.jl. It's a Julia library. And my student, Zach Sundberg, who's now a professor at CU Boulder, developed the POMCPAL algorithm for scalable POMDP planning. We've more recently been looking at constrained POMDPs. So you might want to impose a hard constraint on your problem. And we have also been exploring directions involving multiple agents. These are some of the domains we've been looking at. Medical evacuation. My student, Madiel Hussini, he's actually an Army Blackhawk medevac pilot. And he has developed a framework for simulating these kinds of scenarios. I saw Duncan. He's been pushing our efforts towards belief state planning for spacecraft collision avoidance. And also working with Helen and others on using POMDPs to plan out flight tests so that you can, as efficiently as possible, characterize the flight characteristics of your aircraft. Okay. So that has largely focused on validation prior to deployment of your system. You also want to continue the validation effort after deployment. Okay. And this is sometimes called runtime monitoring or runtime assurance. You want to validate what's going into your decision system. So the sensor inputs. We've done some work with Airbus on integrity monitoring of vision-based systems. You also want to monitor what is happening in the internals of the system. And this has led to some work on mechanistic analysis for an aircraft system. And, of course, you also want to model and monitor the outputs. Okay. Then there's another set of work on assessing the measurements. So Anka Ruel and others have been pushing the frontier on AI evaluation. We released the paper BetterBench. If you go to betterbench.stanford.edu, you can find all of the data about a number of different benchmarks and a number of lessons learned and best practices there. We've also been studying when do these benchmarks stop being useful? When do we have these saturations in these benchmarks? We've also been looking at what do these failures look like in terms of token-level signatures, reasoning failures. And we've also been looking at issues of human judges. So, in fact, another safety-critical area is the use of AI for mental health. And we've been looking at evaluations of mental health professionals. And we have been actually quite surprised to find that human mental health professionals, actually, their opinions vary widely, including in domains related to self-harm. All right. I'll wrap it up here, just mentioning our new trilogy. So the first book is Algorithms for Optimization. The second edition will come out in very early 2027. Optimization is fundamental to everything that we do here. And it's a basis upon which we optimize decisions. And that's covered in our 2022 Algorithms for Decision-Making book. And I'm super excited about this new book, Algorithms for Validation, which is available for pre-order. It's coming out next month. And it tries to provide a comprehensive story about how to go about validating learning-enabled systems and other kinds of AI systems. It's available from Amazon and also, it turns out, Target.com. You can find the PDF of the book online right now. And it includes both the statistical methods that I mentioned here, as well as formal methods and reachability methods as well. Normally, these are treated as separate communities. But we tried to unify everything into a common language. And I'll wrap it up here. Thanks. Okay. Thank you guys so much. That was amazing. So, I guess, really, to start the conversation, you know, you guys saw this whole AI safety stuff. You know, what was going through your mind when you saw this latest hysteria saga going on? Maybe we'll start with Clark. So, I was not surprised because I've been hanging out with AI safety geeks for a while. And there's a good chunk of them that have been saying this for a while. And, you know, I think my response has always been the future has high uncertainty, especially now. And so, it's a good idea to invest in AI safety research. But I also think it's not super helpful to emphasize, like, worst-case outcomes when you have no idea what the real probabilities are. And, you know, I think anyone who says, I know that this is going to happen or, you know, it seems certain this is going to happen, they're just guessing. So, we've both cared about AI safety for some time. I think we started the Center for AI Safety, was that 2018, 2017? And it's fascinating to see that it has captured international attention. And I hope that this will lead to taking safety more seriously. I think that we need to borrow more ideas from the aerospace industry. And I can elaborate on... Okay, fine, I will. Please do. Okay, so, there has actually been some discussion of creating something like the NTSB for AI. And I think that could actually be a good idea. So, compared to the 1970s, we're 80 times safer in commercial aviation than we are. Since Howard Hughes or...? Since the 1970s. 1970s to now, we're 80 times safer. And how did we get there? So, what would it look like? What would it be like an opt-in kind of thing? Would it be like setting guidelines? Would it be strict like the FDA, literally approving THETAs? How would it work? That's a good question. So, the key thing here, I think, is independence. So, NTSB was set up as an independent agency in 1967. And there were put in place other aviation safety reporting systems, like ASRS. And that was a non-punitive reporting system. So, that incentivized all the manufacturers, the airlines, to share safety information, and to really take every single accident seriously, and draw as much scientific knowledge from what went wrong. Now, I'd take that there are other systems that were schemes that have built upon this. In 2007, there was also the aviation safety information analysis and reporting system, or something like that, that also had some form of immunity. And I think we need to do something like that. It's going to take a long, maybe too long of a time to set up a new agency. That's a big deal. Governments tend to be somewhat inefficient. The NTSB is also used globally. So, if an accident involves a component manufactured in the United States, they'll actually go to other countries and investigate. So, to draw that analogy, because it's such a high, hmm, there's so much interested parties, there is risk of regulatory capture and things like that. And then, like, you know, if you look at medicine or you look at legal, there's a board of medicine. Even the internet has ICANN, right, which is also international, self-regulated. DNS has been working great. And there hasn't, but, like, it wasn't the case that, you know, imagine the internet was invented at the same time that Google and Facebook were, like, already public companies. And they were heavily biased in the development of ICANN. And maybe they said, hmm, well, if you want SSL, you actually need Google or Facebook to be the ones to give you SSL certs. Or do you want a domain name? Well, really, it's not safe to give everyone domain names. We should be the ones to give you domain names. So, there's some risk there. And then even more so, like, having government intervention, there's this idea of regulatory capture, which today, right now, if you want to start Uber or Lyft, you can't legally. Uber, Lyft, DoorDash, Instacart are grandfathered in on 1099. So, you actually can't compete, right? And that's the concern that some people have. How do you think about all that stuff? Maybe you can start with Clark. Yeah. So, I was encouraged, you know, by the recent Frontier Lab leaders saying, yeah, we need independent evaluators. So, I'll just say one of the goals of my company is to build systems that can be that independent evaluator. And not just someone that says, oh, well, we're independent, so take our word for it. Our goal is actually to produce independently checkable certificates. So, we would say, all right, we have checked this system, and here's the certificate. You can now go check it yourself, and you can confirm that we got that right. So, I think independence is really important. I hope there are a lot of voices pushing for that, because I think it would be, you know, a real shame if all of the safety was left in the hands of the labs, or even some friends of the labs who claim they're independent. Yeah, I think we need something in the very near term before something like that could be set up. It could be a not-for-profit or something like that. I mean, in the space industry, when you have a space launch, right, you have a range safety officer who's completely independent of the mission. Their only job is to make a go-no-go call based on objective safety metrics. Could it be as simple as a starting position as just U.S. GAAP, which is, like, the U.S. kind of accounting principles, generally accepted accounting principles. There could be generally accepted AI principles of, like, deploying AI safety. And then there's a KPMG, and there's a, you know, Arthur Anderson or, you know, whatever that's, like, you know, Ernst & Young that you can choose, but you have to be validated before you do something. Like, it shouldn't be everything. I should still be able to train a theta on my, you know, tiny box. Yeah, I think we need to develop, you know, best practices, of course, but I think we also need, like, a post-mortem analysis as well. I think we need to take the validation of AI seriously from a number of different perspectives. Back to your point, I mean, I think the airline industry does that really, really well. They don't rush to print what happened. They have a full, thorough review process of every single accident that happens, right? Do you have any? Okay. So my last question for the both of you is how tractable do you really believe these current AI safety concerns to be, specifically maybe the cyber defense issue, some of the bioweapon issue, on the cyber offense stuff, where the models, I can use a open AI to make a, you know, a cyber attack, or I can use, I can trick it to doing so, or I can take an overweight model, and then I would need some defensive capabilities, as we talked about earlier. How, the whole thing, how do you think how tractable of a problem is this? Yeah, I'll take a stab at that. So I think cybersecurity is going to become very tractable. I think, like right now, you know, I was telling my mother, hey, if you prove the code, it can't be hacked. And she was just stunned. She's like, really? You know, we're trained by the media and by television that, like, every system can be hacked. And, well, of course, it is true right now. But it's quite possible, you know, you can prove with mathematical certainty that you can't hack a system. And I will predict that within the next, I would say, three to five years, that'll just happen. Like, all our systems will be completely secure. Because AI can attack, but AI can also defend. And the AI defense plus formal method should get us there. So what is needed to get us there, to have these lockdown systems? Is it the zero-trust architectures? Is it, like, these best practices? Even the admin-admin issue, how do you think about it? Yeah, I mean, I think we just need to move to a new standard of code. Actually, it's interesting you're bringing up how airlines and other industries use, you know, very sound engineering principles. I like to say there's a little dirty secret about software engineering, which is it's not based on sound engineering principles. It's based on, like, just write something and test it and hope for the best. But we actually do know how to do that. I mean, there is a mathematical foundation for software engineering. I think we'll have to see moving to that. And then one other thing I want to say, in terms of tractability of, like, securing AI itself, I don't think we'll be able to reason about, you know, these massive, large language models. So I think our best option is something more like securing the boundaries. And securing the boundaries is also very tractable. Trying to prove that, you know, a 500 billion parameter model isn't going to do something crazy, I think that's not really tractable. I completely agree with Clark on the security thing. Like, I'm terrified of, you know, the next big thing being a massive cyber attack. But I think I would agree with Clark that I have a lot of hope for that. But you can't prove what's possible or what's not possible with biology or chemistry, right? That is, that's an open question. But I think that's what we have been striving for as a species, for increased understanding. And I think that advances in AI will help us on average. I think on average we're going to benefit from these new insights. I have a question specifically for Clark here. So exactly to walk me through how it works, let's say that you are now, we give you $10 billion to be the CISO for Bank of America. Okay, what do they do? What would you do? Okay, so first I would hire all the formal people and race to build the infrastructure that we need to reason about that code. Then I would say, okay, give me all of your code. Give me a whole bunch of GPUs and a whole bunch of theorem proving agents. And we're going to just either prove the code as it is, or we could also just translate it into a better language like Rust or Lean, prove the code there, and then you're done. So there's a lot of work to do there, but I think it's work that we know how to do. And does that mean I have to finally get to 100% unit test coverage? Is that what that means? No, you don't. So tests actually become obsolete. I mean, tests are always good as you're developing. They're like the fastest way to find bugs. But ultimately, the formal argument completely subsumes the tests. All right, now for Michael. Michael, are you aware of Waymo, you know, some of the... Number of my students work there. Next question. Using AST, DIFs, some of the important sampling stuff, you know, Maribu, Reliplex. Are you aware that they're using this in their validation and their theta validation procedures after they train a new model? I can't speak specifically about ReluPlex or Maribu. Clark might have some insights there. But adaptive stress testing, we released not just a Julia version but also a Python version for those who want to continue using obsolete languages. But so we made it open. We've had a number of sponsors of our lab. We've been supported very generously by a number of different automotive manufacturers, including Waymo, with the aim to make these tools accessible not just to them but to the entire industry. And you talked about AST prompter. These are applicable to LLMs just as they are to a trained VIT that would control a gas pedal and a steering wheel, right? Yeah, basically you need two things to use adaptive stress testing. You need a definition of a failure and you need a measure of likelihood. And you can have both. This works for language models, aircraft collision avoidance systems. And do you have as much engagement from Anthropic and OpenAI and Grok on those topics as you do as Waymo and the autonomous vehicle sector? Not yet. I mean, we just published AST prompter. We've been supported by the Schmitt sciences and the ideas to make all these ideas as accessible as possible. And do you think that if they did adopt, they would have equal levels of safety as the Waymos and things like that? I don't know. Hopefully. It's a different thing validating physical systems than language models. Although the methods can translate, the level of success that you can anticipate might vary a bit. I mean, I've heard arguments that, well, autonomy, you know, we can define the failure modes pretty well if the thing stays on the road, if it, you know, if it hits a baby and stuff. And, like, and then I meet, I hang out with Lane McIntosh and he shows me examples of what the Tesla car actually subverted and survived and didn't do the bad thing. And it was well outside the distribution. It was a failure mode that was not monitored or sampled in any reasonable world you could have. There's always a long tail, right? Yeah. And the sum of the long tail is always going to be a high probability. And then they say, well, and so in the LLMs, you know, can't we kind of, isn't it kind of that same? Is it meaningfully different long tail? Yes. I think you're exactly right. So even for ACAS-X, we know that the probability of failure is not zero. I mean, we have simulations that show that it fails in certain situations. It's just that those situations are just so incredibly unlikely. I mean, the International Civil Aviation Organization and the Federal Aviation Administration, their standard for safety is not probability of zero, probability being zero, right? We have to be realistic. If anyone tells you they have created a completely safe system that interacts with it in the real world and it's fully safe, yeah, I would not believe that. Clark's got some guarantees for us. Clark has some guarantees. So to use Clark's method or category of methods for formal methods, and correct me if I'm wrong here, but you have to, you're making these proofs with respect to some model, okay? And if you're modeling the real world, you have to capture your uncertainty in what can happen, like the accelerations of the aircraft or whatever. And so you generally have to assume bounds on that uncertainty. So you have to estimate a nominal distribution on the input on what's going on and on the transition function. So in formal methods, you generally don't assume anything about probability distributions. You capture your uncertainty in sets. Right, okay. And that's a different approach, and it's great when it works, right, because you get a nice proof, and that's wonderful. But the question then is, do those uncertainty intervals, are they sufficiently realistic? Just to say something on that. So, yeah, a proof is always with respect to some assumptions, right? And so in some cases, you can make reasonable assumptions and give strong guarantees. I think what Michael's saying is, if you have, you know, your input is like another actor in the real world, and you assume that that actor is not going to try to hit you with their airplane, then that might not be a valid assumption, right? So you do, it is really important when we talk about safety or about formal guarantees, that you understand it's with respect to some assumptions. Now, there are some things that you can guarantee 100%, right? If I prove my code is memory safe, then it is 100% impossible for you to use a buffer overflow attack to attack that code. But there are other things that, there are limits to what you can do with formal, right? I mean, the work we did on verifying neural networks, you know, people would ask us, well, how are you going to verify that this perception network correctly identifies cats and dogs? And I was like, well, I don't even know how to formally specify a cat and a dog, so that's beyond what formal can do. So there are limits. You have to be aware of that. That's something that I think the formal community has also really learned hard lessons that you have to state those assumptions or else people will be disappointed. So last question for me, what's the Swiss cheese model? Are you making like grilled cheese sandwiches or something? What's that? So we use the Swiss cheese model as an analogy in aviation safety, right? You have a number of layers of defense. So like for aircraft collision avoidance, right, maybe the top layer is like strategic separation, right? Depending on whether you're flying west or east, you fly at different altitude layers. And then you have another layer, which might be air traffic control. And then another layer could be your collision avoidance system. And we call it Swiss cheese because these different layers have different vulnerabilities, right? Those are the holes in the cheese. And what we want to do is make sure that the holes don't line up, okay? You don't want a critical scenario to make its way through all the layers of the cheese. And so then applying this to these big, large language models that are big and scary, I mean, we control the training data, the pre-train, the RLHF, the RSI, all the data that's being sampled. We can take out the bad data. We can run, like Percy's doing this right now, where he's running a small little model to look over the pre-train data to take out bad stuff out of the pre-train. Okay, then that stuff's never in the pre-train, so it can't possibly learn those bad things. And then, so that's like step number one. Now you have a trained data. Let's do a failure analysis on that data. Okay, let's estimate failures. Let's sample some failures. Let's estimate some failure modes. Let's get to a p-fail, which I think, you know, bad marketing. Let's get to one minus p-fail, which is p-success. And then tools, and then all the way to runtime monitoring, right, which you mentioned earlier, it happens as well. Yeah, what are your thoughts on that? Yeah, you need all these layers. I think the example you gave in your opening remarks, they had like the chain of thought monitor turned off, right? That would be one of those layers. And I think in addition to developing these technical tools that Clark and I have been working on, we also need to make sure we put in the proper safeguards on the human level, right? So, like, I mean, we've learned this from cybersecurity, right? A way to, the typical way of breaking into a system is through human engineering, right? Yeah. Awesome. Okay, I'll open up to the audience now. Okay, you're in the front. There we got. Mike's coming. I mean, this question is for Clark. So, you mentioned that, you know, in the Bank of America, like, example, I mean, most of the time, you know, the enterprise code and the real-world code doesn't necessarily have a specification. So, in that case, like, how would you formally verify this code? Would you, you know, get the, I don't know, like, spec or assumptions from the source code itself, or how would you do that? Yeah, this is a great question. So, I think in the new world where it's easy to write code and hopefully in the next couple of years it's easy to verify code, the thing that's left that's hard is the specification. But there are a lot of things you can do. So, first of all, there's a spectrum. Some specifications are easy and universal, right? So, if I have C code, I would like it to be memory safe, right? I can write that specification once and for all and just say everybody should, you know, prove this is correct for their code. And for the audience, what does a memory safe mean and why is that important? Yeah, yeah. So, that just means that it's never possible for your code to access uninitialized or out-of-bounds memory. Who cares about that? Well, if you can do that, you can most likely run some kind of buffer overflow attack, which, you know, is famously been used to gain access to all kinds of systems. In fact, I think the number one, still, sadly, the number one security vulnerability is buffer overflow. Yeah. So, there are some specs like that. There are also sort of domain-specific specs. Like, for a bank, I think they'd be interested in things like no loss of funds. So, if I run a sequence of transactions, then the total amount of money should stay the same. So, you can come up with some of those general things. Also, it turns out agents are actually quite good at coming up with specs. So, I don't know if you've done a cloud code session recently, but often what I find is, you know, I say, I want this. And it's like, oh, yes. And you probably want this, this, and this, too. And I'm like, yeah, actually, you're right. I do want that. And so, I think agents can help us write specs. And I imagine a world where you have a sort of agent assistant that's, like, talking to you and talking you through the different corner cases and helping you with that. So, I think there's a lot you can do in that direction. So, I mean, like, for example, you know, in the open source model, like, let's say, you know, you are formally verifying a VLLM or SGLAN or something like that. You could write, you know, formal spec with assistant of agents. But how would you know that, you know, that even the spec that agents, you know, write is, you know, the same as the developer wants or developer's intent? Yeah. So, there is a gap there. And you would have, I think that's an interesting research area, which would be building tools and agents to help cross that gap. But even if you don't cross that gap, I would argue that if you ask your agent to write a bunch of specs and prove them correct and it succeeds, you most likely have better code than you would have had otherwise. Thank you. And then going back to, like, having a smarter model and going faster. The better, the better, better these frontier models, presuming that they're doing a good job and they're good models, the better that they can give you tight specs. So, like, wait, you didn't think about all these other things. What about social attacks when someone calls and there's a person who's been there for one month and they don't really know anything. They don't want to get fired. They don't want to make a mistake and have an angry customer. And they're calling with their baby crying, but it's fake. And, like, you rush it and then you give the thing, I've seen these videos on how they hack. And then, you know, social attack. Well, a spec you might put in there is if the person has been there for less than six months and they haven't been through a, you know, a fake, you know, social hacking scenario and haven't passed safety training or whatever, then maybe they don't actually can't give passwords to, you know, resets to new email addresses, you know, stuff like that. You can think through all those different scenarios. But anyway, yeah. All right. Next question. In the front here. So it sounds like you see formal verification as some kind of rigorous review process and drawing analogies to maybe aircraft collision avoidance. Well, maybe in engineering, there's generally some amount of regulation since the safety standards at one company might not match the safety standards of another. So do you see regulation being in any way or shape or form involved in AI safety? And if not, do you have some means of incentivizing companies to adopt your formal verification engine? Yeah, I think regulation. Yeah, I think regulation can play a role. I think. Oh, the question was, is there a role for regulations? Different companies might have different, I don't know, safety standards? Safety standards. And if not, how will you get everyone to adopt your formal verification engine? Oh, I think the last part about the, so in terms of regulation, one of my collaborators over the years has been Chris Gerties. He was, he was a professor in mechanical engineering at Stanford. He's now at Waymo. But he worked on automated vehicles and he was, he went to Washington, D.C. to help the Department of Transportation come up with regulations for automated vehicles. In the end, I think he and everyone there kind of realized that it's a little bit premature to be too prescriptive in terms of what technologies to use. But rather focus on higher level best practices and standards at that level without being too prescriptive. Because this area is, you know, there's a lot of innovation that has been happening and that will continue to happen. I think the important thing to realize is that the various frontier labs, the various, I don't know, automated driving companies, they don't want to compete on safety, right? It's not in Waymo's interest for Zoox to have an accident and vice versa. And so I think this is an opportunity where the industry really needs to work together in their particular domains, right? Automated driving, I mean, those standards are just going to be different from language models or other kinds of applications of AI. Yeah, so about regulation, I would just say I do think there's a role for it. I think you have to be careful, like Michael said, not to be too prescriptive, but to find ways to incentivize general principles that would be good for safety. In the specific case of formal, you know, I've been doing formal for 30 years trying to get people to do it. It's a bad idea to try to tell people you have to do this differently. I think what's different now is I think there will be market forces that incentivize it. So if we can show that formal is automatable, works at scale, and gives you higher security, and a few companies adopt it, then every other CISO is going to be like, oh, we better do that too, or else, you know, we won't have that same advantage. So I think we will see, you know, strong market forces help, I think, actually all across AI safety. And the one benefit that I think I would like to underscore on formal methods is that you can leanify things instantaneously now, where before it required so much time. You made that point on one of your slides, but, like, it's so important to really, it's now tractable. So you lost people because they say, oh, you just need to hire 150, you know, people who are, you know, PhDs in lean to, like, go through all the Google code and make this happen. Now you don't have to. That's right. Right? You need, like, I don't know, $100, $1,000 in tokens, right? And then on the, it's a really interesting point that you made, Michael, on the incentive for Waymo not to compete on safety. And I think the same thing is true for the frontiers. No one wants more attacks and things like, and misuse of their models. That's bad marketing for everyone. And Thomas Brown, Tom Brown just actually said that up in Napa. And I think what we should also say is that they all just went to the White House and signed a document with these four bullets. So I'd actually, like, they are actually agreeing on independent audits, some of these safety guardrails and all these other things. Because they all are going to do those things, all six of the labs, including NVIDIA, because NVIDIA does make Megatron. They're not included in the conversation very often, but it should be. So there is already a framework for a self-regulation body that doesn't need government oversight and isn't punitive, is the word you used earlier. Okay. Let's go from this side in the back there. Yeah. Thank you. Question for Anne Truth. Curious, what applications or markets are you targeting first? And, you know, how do you measure success in the real world? The specific applications you are. Sure. So I can't say too much about that. What I will say is our very first priority is to build the capability to reason autonomously, automatically, efficiently, about code at scale. We think it's sort of, you know, if you've heard of these labs talking about mathematical superintelligence, it's like code superintelligence. Like the ability to really reason precisely about code. So we think once you have that, there's like 100,000 things you can do with it. You can imagine, you know, helping enterprise. You can imagine helping developers. You can imagine, you know, helping with security. So, yeah. That's the direction we're headed. Success is when all of the world's code is verified. First of all, thank you. Second, when you are, like, LLMs right now are a system in which humans are interacting with the code, I mean, the interface. And I know, like, there's a lot of prompt injection attacks that are happening and maybe XSS attacks that can happen through agents. Do you think these type, like, how would formal help this sort of attack? Yeah, so, again, there's some difficulty there. If we're talking about natural language from a human to an LLM, then there's not really any part of that that's code that we can prove something about. But there are things that can be done. So, Amazon has a technology called automated reasoning checks where they actually look at the responses of an LLM. And they try to extract using auto formalization what the domain knowledge is that the LLM is trying to communicate. And then they check that against a rigorous domain model. So, there are some techniques even when it's all natural language that can be leveraged to provide some security and safeguards. When I was learning CS, there was, like, SQL injection attacks. You know, Johnny Drop Tables, I think, was the classic X, Y, C, D. Is there no equivalent, like, a model to look at the user input and lint out prompt injection? Sure, but that's an arms race, right? So, you can... We're just trying to outdo each other. Right, right. Okay, I think we have two and two. I'll go in the way back there. Yeah. Hi. So, yeah, this question is for Clark. So, I'm curious, in your Bank of America example, even if you formalize all of the software within Bank of America, the software relies on a lot of long-tail dependencies. Even down to the hardware level, you'll have to maybe formalize the x86 instruction set, and then you have to do... It's been done. The x86 instruction set has been formalized by several companies. What do you think about things like hardware-level attacks, like Rowhammer and that sort of thing? Yeah, I mean, I think probably software is low-hanging fruit. Hardware is a bit more difficult. But I do think that the eventual scope would be you verify all the software, you verify all the compilers, and you verify all the hardware, and then you call a day, right? So, I mean, why not? I think AI is just going to get better. The formal tools work really well with AI. There's a bunch of startups doing hardware verification with AI's help. I think this technology is going to get better and better. Cool. Yeah. Yeah, so one thing I saw from a doctor I know on LinkedIn was talking about how if Waymo was like a pharma company's drug, it would have gotten a waiver from the U.S. government for compassionate use because it's been so effective at saving lives. And so I was kind of like, you know, curious about if there's like some sort of like similar thing you can have for like cybersecurity. You know, one thing you have with a lot of like enterprise systems, right, is that, you know, there's an admin team, right? And, you know, maybe it's these guys aren't doing admin, admin is their password. But, you know, one thing I've heard about is that, you know, these folks with admin or developer access face threats themselves. You know, crypto execs have gotten their fingers cut off. The CEO of Adobe was kidnapped in the 90s, I remember. And, well, I'm kind of young, but I heard about it. And so I was curious, it's like, could you have an AI system that's like so trustworthy that it could be your admin? Is this even like possible? Like you run it in like some confidential virtual machine. I was kind of curious about what your thoughts are on this and like whether we can like kind of limit the sort of physical attack vector, you know, and have like something that's like truly safe and secure. Yeah, I think a similar kind of question comes up in the aviation domain, right, especially with aircraft-assisted suicides, right, and concerns over mental health of, you know, human pilots. So, yeah, the question is, why don't you automate that? Just like how I think you're suggesting automating the administration. So I think it might be a little while until the Federal Aviation Administration will entertain that. The way things are set up right now is that aircraft, even if it's unpiloted, there's a pilot who is regulated and certified by the FAA. And if something goes wrong, they're responsible for it. So I think we need to think very carefully about responsibility. And that would be my concern with your suggestion. Yeah, I think the Waymo comparison is an interesting one, right? Like Waymo is not perfect, but it is, according to them, it is saving lives. So you could imagine making the same argument there, but I think Michael's point is a good one. Like, who do you blame if it doesn't go well? And does the company that makes the AI admin, are they willing to take, you know, legal responsibility if something goes wrong? If they are, then that suggests they did a really good job with their safety case. And this actually goes back to the point of, like, a smarter and better AI system. If you, like, there's the one system trend in information security is zero trust-based architectures. And so, like, you want to make sure that there's zero trust in any one of these systems so that if you infiltrate one, you can't infiltrate everything else. And, you know, if I had a really smart, always-on AI system that's looking at traffic and looking at my data dog, looking at whatever is coming through, and they see, you know, a bunch of wires going from the CTO, you know, to some foreign account or something like that, or a bunch of keys just got generated and shipped to a non-at-google.com, but to some Gmail, you'd be like, what? That's, hmm, you know, and then it's with enough, like, some things you don't have hard and fast rules, but with enough context, you can probably draw the line and be like, this is not cool. Let me flag it and just flag it to people. And we've all had, you know, these century alerts for anyone that ran a company. And it's like, it's just a thousand of these garbage alerts. And so you don't look at them very often. And it's like, you know, ACAST has this issue as well where, like, death by a thousand alerts. So you have to be really, really targeted. And I think AI watching the system can actually do a much better job with that. So we'll take two more. I think we'll go here on the right here. Hi. First, I'm really appreciative of both of, like, I wanted to hear on formal verification and then also, like, standards and safeties, especially, like, in physical systems. So having an avionics professional or professor here is great. I wanted to hear, especially because you touched on dynamical systems-based models, like diffusion models, normalizing flows. Right now we have the Chinese labs pushing the frontier of efficiency. We have the American labs pushing the frontiers of intelligence and capability. And we don't really have anyone pushing the frontiers of controllability and interpretability from the start. We do have some fields like developmental interpretability where people are monitoring training dynamics and emerging capabilities and trying to fit math that we have discovered throughout the fields, like, and try to fit it to what we're observing. But I'm trying to basically ask, like, do you think there is room for constraining training dynamics and intelligence, trying to map this frontier of interpretability and control on one axis and intelligence and capability, moving from traditional statistical machine learning methods and signal processing and control theory over into, yeah, deep learning and neural networks? Also, I'm sure I have messed up a lot of the terms I've mentioned. I don't mean to just add in a bunch of buzzwords, but... Like filtering gradients and some of them? Oh, okay. Yeah. No, this is a great question. So I teach groups... Three times a year, I offer an executive education program through the Stanford. Graduate School of Business to executives, and I do another one through HAI. And they're executives from, you know, all around the world, and they're under a lot of pressure to somehow come up with an AI strategy and bring it into their products or processes. And what I remind them at the very beginning is of the fundamental principle of engineering. The fundamental principle of engineering is very similar to the fundamental principle of science, which is Occam's razor. You know, simplest explanation is more likely to be true. In engineering, the simpler, more interpretable method is more likely to be robust. And so depending on their application, they should really be... Like, if you can get away with linear regression or decision trees, you should be doing that. There's a lot of temptation right now to go straight to neural networks and transformers and all that. But that's often not the right way to go. And so I encourage everyone to try out the simplest method and then try something maybe a little bit more complicated and see if the performance lift justifies that additional complexity. If not, then stay with the more interpretable method. But I think this is a very important topic. In fact, one of the chapters in the new validation book is on explainability. And that was critical in getting ACASX accepted as an international standard. A really quick follow-on. Like, do you think that there is, like, market incentive or, like, enough, like, demand, like, where we could... People building, like, constrained intelligence, like, they would be able... Like, it would be feasible to compete with, like, with the frontier labs. So I would say that if you manage to create something that is measurably safer, then that would be a competitive edge, for sure. And I know that there are people out there thinking about how to do that. So, you know, hopefully they can figure that out. And if you are looking to start a company, there's these accelerators that you could apply to, and they give you money and guidance. Anyway, yeah, you're in the back there. Hi, thank you so much. So my question is, Internet era taught us a lot about security. So what do you think will we, like, copy from the Internet era, or what we will learn something new from the Internet? This generative era or authentic security, insecurity especially. So it's the question, what can we learn from the Internet era that we could apply in the current era? Yes. And what do you think would be different from the Internet era as well? Yeah. So I remember going to a talk when I was a young professor at NYU on security, and basically said there are only two problems. One is people, and the other is computer bugs. Yes. So I think we can fix the computer bugs, but I don't think we can fix the people. But what's different is I think AI can be used in all sorts of different creative ways. So it could be used, you know, as Francois was saying, as kind of a watchdog to maybe, like, catch some of the social engineering. It can certainly be used to accelerate things like formal methods to, you know, secure the systems. Yeah, maybe even the AI admin idea is a good one as long as there's still some humans in the loop. I always worry, you know, I don't know if any of you ever watched the movie War Games, old school. But, you know, you turn everything over to the computers, and then there's nobody. If there's something weird happens, like, that can go off the rails. So I think we do need humans in the loop. There's a famous physics paper called More is Different, and it's kind of like the premise in, like, okay, if I have, you know, one atom and two atoms, if I have a bunch of atoms, I have a whole lot of atoms, black holes start to form. Like, light can't escape. Light just does a loop and comes back. So there's weird stuff. So more is different. And I think in this world where we had 6 billion people, and now we have 7 billion people, and now we have 700 trillion agents that are, let's just say, at equal intelligence or have some motive, and I can spawn all these different agents. More is just so different. And so, yeah, we had Cloudflare being able to stop DDoSs, but, like, everything breaks when you apply infinity to the number. Everything breaks. And so weird stuff can happen that exposes it. And I wrote this tweet today. Basically, like, there's a lot of systems that we just saw this with iClear, where 60,000 submissions submitted in one year, which is greater than the cumulative summation across all submissions in all history in one year. So that's, like, a big exponential. That E, the constant up there, is a big number. And so all review systems, which we had many at Focal, for example, looking at the century alerts, looking at customer, you know, support tickets or whatever. Like, imagine college admissions. Like, a, you know, a Nash equilibrium, you know, optimal strategy for every single, all high school students is to apply to every single school in America. Why would you not? In fact, actually, I'm sorry, the whole world should apply to all schools everywhere. Right? It's expensive. They're going to have to charge money. There's a fee. Yeah. If there's, you know, if there's no fee, then that's kind of what has to happen. And then so how do you actually handle these human review-in-the-loop systems? They get DDoS really hard. A real one that just got discussed was small claims court. So if your agent can file a small claims for you and you don't need a lawyer anymore, what happens to the judicial system? It's completely bogged down. It already takes too long to get through the judicial system. But now it's going to be insane and impossible. And so all of these systems need to be re-evaluated. And so the more is different is really the learning that is going to be meaningfully different, I think, from the Internet era to now. We thought we knew what big scale was. But, like, human traffic will be 0% of Internet traffic. Like, like, that's going to be, 0% is a very small number. Thank you. Okay. We have time for one more question. Yeah, please. Thank you. So this question is about benchmarking the benchmarks. And the context is that I'm working in AI safety at LinkedIn. And the definitions of harms drift very fast. Even looking at something so small as toxic text or bias, every five years the new generation has a new slang for everything. So how do you make sure that that slang doesn't show up in, say, hiring in the messages that you get from recruiters? How do you measure that right now is benchmarks? But benchmarks move very slowly. The public, even in-house benchmarks, have to be very costly and need to go through a lot of human review. What are your thoughts on how do we go from current state of co-op, some labs publishing benchmarks, and slow creation of benchmarks, to a state where benchmarks are dynamic, evolve as quickly as terms evolve? Yeah, great question. And I like your example there. Yeah, I think we, just like how I advocated for continuously monitoring our AI systems, we should continuously monitor our benchmarks. And the good news is that there are some quantitative methods for identifying distribution shift. And monitoring shift in language, I think we just need to do. Nothing to add there? Okay, all right, one more, last one. Follow up with regard to BetterBench. I think one thing that I see researchers keep running into is that some common evals, I'm looking at you, Math 500, have broken pieces to them. I feel like somebody, and maybe it's your group, there needs to be some kind of coordination with Hugging Face or somewhere where agents will centrally find that these resources have these problems. I think it's just like we put up, you know, reports that different benchmarks are broken or different evals are broken, and then it just sits there, like I have this paper. But some, I'm just open call for somebody to, like, close the loop here. Yeah, I think I've seen that as well. You know, I had a former student who was trying to evaluate SQL queries, and nobody could get better than, like, 70%, and then he showed that, like, 30% of them were actually wrong. So I think it's just a matter of people moving too fast, being a little careless, and hopefully, you know, the people who are rigorous will eventually catch up and fix it. But it's a little bit of an arms race now because everyone's trying to move so fast. Yeah, we need version control and pull requests, issue filing, and so forth. Absolutely. I actually think that a great idea for a startup is, like, a Apple App Store of benchmarks where there's curation, right? Like, they don't just let anyone just throw an app onto the App Store. They go through a process. They determine whether or not you should be on the App Store or not. Hugging Face, all due respect to Clem. I love them, but it's a mess. It's a mess. It's like the wild – it's like GitHub. It's like the Wild West. And so, like, trying to find, like, the appropriate GSM-A-K, like, it's actually non-trivial to find what is the actual right GSM-A-K because there's 600 different things called GSM-A-K. It's like, which one do I use? I don't know. Anyway, please, everyone, help me thank Clark and Michael for joining us tonight. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you. Thank you.