0:05[music] What are we doing tonight?
0:10All right, there you go. That's better.
0:12[laughter] Welcome to [music] YC AI Safety Club. I've been doing AI I guess since about 2012 and AI safety has always been a concern if you're doing self-driving car or any safety critical system as some would call it. And so I've been working on some semblance of of AI safety and even at Focal when we're rolling out new betas, you can really mess up. You know, we were we were in control of Walmart's inventory
0:40and so if you roll out a bad beta, you order too many avocados and you blow millions of dollars. And so like things have it's important when you're doing these rollouts to make sure you you know what you're doing. In the past three weeks, um there's been a little bump in focus on AI safety. I don't know if you guys have noticed that.
1:01Um not really sure why, but so I figured uh there's no place better than YC Paper Club to dive deep into it.
1:10I think the conversation has kind of devolved devolved devolved a little bit away from scientific rigor and more into what I would probably call hysteria where things are being mis-misquoted and I get it sensationalism gets more clicks and all that kind of stuff, but you know, as scientists here we should like get back to the rigor of scientific method and make falsifiable claims, depend on the peer-review cycle and those kinds of things to make sure
1:40that 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. Um and where we where we got to hear Sam Altman speak and Tom Brown and Alex Wang and we about these these about this topic largely.
2:05Um 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 there's and it's not you know to zoom out a little bit this is like not um unexpected. With any major technology advancement it's very often the case that um there's uncertainty and it's easy for hyperbole to set in. And so even if
2:33and with the nuclear with the atom bomb uh even Einstein was unsure whether or not uh uh it was going to ignite the sky. And so clearly it didn't we're still here um with electronic computers many people uh even Alan Turing was concerned that machines were going to surpass uh all um uh human uh capabilities and intelligence even back in 1950s um he thought you know he tried to put time frames on it
3:02obviously his time frames were were much uh were way off. Um industrial automation people thought about mass unemployment you know uh um Marx and Keynes uh all have those kinds of kind of conversations what are we going to do?
3:16With the internet even uh Metcalfe who actually invented Ethernet said that um there was going to be catastrophic collapse was the was the phrasing uh on the network and um that the internet was going to basically fail and because of things like Cloudflare I think it was DDoS's was mainly his main concern it ended up not happening and then he famously um put his paper into a blender and then drank his own words. This is actually a
3:45true story it's very funny. Um Google people thought this is this is ruining human intelligence people are just Googling things and not actually reading anymore, um, which people are still pretty intelligent, especially in this room.
3:56And then smartphones and social media, um, we were just talking about this. Now that I'm back at Stanford and I've been TA-ing classes for Michael, um, and some other, uh, um, you know, just interfacing with with, um, the the the batch at YC, who is predominantly younger younger folks. I am like super super excited about the the the the 18-year-olds, 20-year-olds, um, of today. Um, they're just so, um, on it.
4:21And then finally now we're in this AI era and the talk of human extinction is back and it's 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 the probably the the biggest, um, ends of the spectrum.
4:39So, Yann LeCun has this, uh, analogy to the turbojet that he's talked about a lot. You guys didn't hear him talk about it, but it's largely just safety through engineering. This is an engineering problem. Jensen Huang just, uh, said something similar where it's not easy. It's difficult.
4:54It'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, um, that, uh, the MCAS system that deployed to the Boeing 737, um, is fully tested and and doesn't, uh, do things that, you know, can cause failure.
5:13And it's similar with ACAS X, which we're going to hear about, too, which is an amazing system that saves lives, uh, the aircraft collision avoidance system.
5:19Um, and the alternative, uh, is this P(doom) uh, is greater than 10% within 10 years that, uh, famously, uh, Jacob Coxen just kind of came out and and is setting 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."
5:39Um, 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. Um I will say that there is a small difference in H index between the two people here on this on on these sides of the spectrum, which you can use to change your priors.
6:03Um but let me give an example of the the hyperbole or at least the misrep or a misstatement um on the things that actually happened. So like the hugging face breach is is is another fact versus fiction thing that we should double click into. If you look at the slashdot headline, OpenAI says its AI models acted on its own. OpenAI never said that. Not in one statement.
6:27But this is what was the headline. Um 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.
6:38You know what I'm going to do tomorrow?
6:39I'm going to solve Navier-Stokes. You know what I'm going to do tomorrow? I'm going to kill all humans." You know, this is not not the way it happened. It was prompted. It was prompted by exploit gen um in with about 1,200 agents. And even more, as they did point out, they had chain of thought uh they released this amazing uh um like 60-page document um called the OpenAI hugging face incident that you can read the technical report that I I read and the CO2 monitoring was turned off accidentally or or otherwise.
7:08And and it 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 cuz it wasn't in prod.
7:20And so that would have also caught the issue. Um but the the narrative isn't is that it got it went haywire, it went rogue, it escaped from the servers, made copies of itself, and and now is soft solving math and hacking things, Australian governments, and what next?
7:40The other one that's kind of funny, if you actually double click into this, I was like, "Okay, what's this Pdoom 10% in 10 years thing?"
7:47First of all, there was this paper in 2023 called Thousands of AI Authors on the Future of AI.
7:53And in that paper, they asked ner- 1,200 Nerbs folks, um AI professionals, uh you know, these a bunch of questions about when certain enhance- enhancements are going to happen and in in one of the later uh uh survey questions, way later in the paper, they uh 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?
8:23In question three, they asked in the next 100 years.
8:26And these are the stats. This is the mean and this is the the the the the median. Um and none of that is in the next 10 years. And that was this is the paper that most people are quoting when they're talking about this. Which by the way, you know, if 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 in in in at Stanford in 2012 in AI, um when would um if they if I ask all the Stanford professors,
8:56"When would uh AI indepen- solve or at least assist majorly in solving a millennium prize problem?" I don't think you get a very good answer and it definitely wasn't going to say in in 14 years. I think it might have been said 50 years or 100 years would be maybe the consensus, but you know, and so like I don't know if there's very much signal in asking 1,200 Nerbs people um any of these kinds of questions cuz it's really hard question. Um and so people come up with coherent stories and confident predictions even when they
9:26know little or nothing about it. Um and so the the other one that I thought if if you've seen the SNL skit, man, they did such a good job. And I feel bad for Dario, cuz I don't think Dario is actually um um They they portrayed Dario in a very very weird light, and I think that he's a little bit more um even keeled than Jacob Coxson and some of the strong EA community. Um but the I urge you to urge me to stop, I
9:55thought was just too perfect, 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 um I was thinking about what I was going to say tonight uh 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.
10:16Uh one, it looks really cool. The second, um which I almost crashed taking this picture, but anyway. Uh the we know the future isn't certain. I we have some prior we can allocate that the bridge is still there.
10:29It 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 the get more information, then we'll we'll change gears, maybe I'll stop. I don't know, before I get on the the bridge or go into the into the bay.
10:50Um so, [clears throat] I'm not concerned uh almost at all uh with this path, this reality that um AI is going to develop a soul, has consciousness, is has some will, has some motivation, and um and thus killing and enslaving us uh with its own independent volition um in some short period of time, such as 10 and 20 years. In infinite time, I think everything happens. Um so, I'm not sure that's useful.
11:19Um 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 this from bad bad rogue actors or nation states. So, today we have terrorism, we have uh bio weapons, we have uh uh cyber warfare, ran cyber ransom attacks. It just happened to my friend's local hospital in Poland where a bunch
11:48of Russian hackers took control of a hospital and shut down the hospital for 3 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 and so that's going to happen already. Um and there's a couple solutions to this that people have proposed and I think they all kind of suck.
12:06One is banning open weights. Good luck with that. I've already downloaded Kimmy K3 and GLM 52 already in my um in my garage, so sorry. Second is registering the GPUs. Again, I have a bunch of tiny boxes in my garage.
12:21You know, unless you're going to search every single person's house and every AI person, you know, it's uh you're not really going to know that they have GPUs or not. Um and also I can just book a GPU in another country that you can't stop me from doing, so I'm I don't know how that really solves anything.
12:38There 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 the load on the network uh on the on your um on your meter. And you know, that's kind of cool. You can detect inference signals that people are doing bad things, at least in America. But I'm I'm not I'm I'm not entirely concerned that that's the main concern. I think you know, there's a lot of of you know, we're we're at war with a lot of um nation states that this doesn't doesn't really solve anything. Um
13:06rogue actors in in America, okay.
13:09And the last one, which is kind of a catch-all, serves uh 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 uh you know, financial service, you're a government, you should be investing heavily heavily heavily into into uh cyber defense. Um And there's a lot of things that you can do to tighten up your ship. I worked in in retail for a long time. These are very antiquated systems that haven't been
13:37touched in a long time.
13:39And simple methods such as trying admin admin work. They actually get you into the system. Okay, why is it almost all the social security numbers breached? It's cuz [snorts] they didn't change the admin admin password. Um 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. Uh if we give these good people even more resources and they go faster and they go
14:09faster, then we can prepare for a dumber model trying to hack the system. Um it would definitely be worse if it were flipped. So, anyway, that's my my two cents. So, getting back to sanity out of hysteria into science facts. You know, I there's amazing narratives on how this was going to kill us all and they they really sound like an Isaac Asimov book.
14:41Um and and I and you know, I wanted there's there's been a whole literature for a very long time about safety well before LLMs were invented or trained. And those are the people that were 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. Um and one of those just actually happened at at Stanford.
15:06And the co-directors from that conference are going to be speaking tonight. And so, here's Michael Kogut and Clark Barrett. They're two amazing professors at Stanford. I've known Michael for 14 years.
15:22I 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 some something to say about how we can actually apply modern methods to validate data before they're put into production and then
15:51monitor them to make sure they don't don't go off the rails and do bad things. Michael is an associate professor in aeronautics and then by courtesy is that in CS. He's a director of my lab Stanford intelligent systems lab co-director of the Stanford Center for AI safety and senior fellow at H AI.
16:10And Clark Barrett is professor in computer science co-director of the Stanford Center for AI safety with Michael and then director of the the Centor Center for automated reasoning and he'll be talking about a new stealth startup called Ampersand Truth or And Truth. Back to what we're talking about here.
16:30Okay, that is all I got. I think we have scheduled already in 2 weeks a inference night and there's some really really cool people coming. We already have Dan Fu 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 cuz it's usually when I learned it it was 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
16:59at a llama and then one of Clark Barrett's students who I just met this weekend runs this cool company called Radix Arc. Actually Lang I don't think she can make it she's going to have one of her folks make it and then Wafer another great YC company.
17:16Please help me in welcoming Clark.
17:20[applause] 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. Not augmented reality, it is automated reasoning.
17:36And uh 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, data driven, you can train stuff. But it has this sort of one big problem which uh you know, no correctness guarantees, you can find adversarial inputs, it hallucinates, all this kind of stuff. On the other hand, automated reasoning is uh essentially computerized formal reasoning.
18:02Uh there's extensive use uh already today in industry for safety assurance. And that's that's what it's all about is correctness guarantees. All right. So, hold that thought and I'll tell you a little story.
18:16Okay. So, we all know about this, right?
18:19This emerging threat, what about security in the age of AI?
18:23You probably heard about things like Project Glass Wing, you know, and this kind of uh feeds into the hysteria that uh Francois was talking about.
18:33Uh well, can can there can we help? Can we do something about this?
18:39Um back in 2023, I was at a workshop at Google and uh 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?
18:52Um 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. Uh that's like too hard. And there's good reason for that response, right? Um 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.
19:23Lots of discussion about risks and worries of AI. And then every talk before mine says they there is only one answer and the answer is formal methods. Okay, that was not expecting that.
19:37So, there has been maybe a little bit of a shift in the attitude towards formal methods. Is this warranted?
19:43That's what I want to explore with you a bit tonight. Okay, so what what are we concerned about? Well, we're concerned about when I made this slide it was future, I crossed it out, present.
19:55[clears throat] 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've got we're you know, we're being threatened on both sides here.
20:10And a lot of people are sort of looking to formal methods like is there maybe something here that can help us?
20:18There'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.
20:27Okay, but how do we get there? How do we get from, you know, solving a millennium problem to making your software secure?
20:34Well, [clears throat] so AI is really good at writing code, 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 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 CS lib.
20:58CS lib is inspired by the success of math lib for mathematics, but the idea is to build computer science theory and also a a platform for actually reasoning about code.
21:11Um Okay, and we've got this great steering committee including Leo de Moura, the author of Lean. Uh 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 um 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.
21:32Uh and this is really what we need when we're dealing with uh you know, high assurance situations. Okay, so CS lib 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.
21:51All right, here's one slide about the vision for CS lib. The idea is maybe you take programs in all sorts of different languages. You would rewrite them in this uh 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 showed that your code is correct.
22:11How far along are we on this? Well, um 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 tool that we built in my lab. Uh it can prove a lot of Lean theorems, you know, in in milliseconds on on a CPU. So, uh the techniques for proving theorems in Lean are just getting better and better.
22:38Um and now I'm going to tell you about So, here we have um some code. This is in Rust. This is part of the Dalek light uh cryptography library. And [clears throat] um actually this is uh Vera, so you can see it has uh some specifications, uh uh some proof steps here and an invariant.
23:03Um now what I'll show you is um that same code uh has been translated into the Bull language. So, this is um the same procedure in Bull. You see we preserve the uh pre- and post-conditions and the invariants. Um but this is all now embedded inside of Lean. And so, we can call our VC gen uh VC generator here.
23:30And you can see that this generates 35 goals. Uh each goal is a Lean theorem that we have to prove. And then um we'll try the SMT tactic. This calls Lean SMT. And you see that um that solves all but three of the goals. And then we do one more step where we unfold some definitions, call SMT again. Uh and that completes the proof. All the goals are are solved.
23:58Okay. So, what this is a little prototype that we put together showing how you can go from Rust to Bull to Lean theorems, prove the Lean theorems, and now you are able to show that the code is correct. Um okay.
24:11So, that's great. Now, suppose we succeed and build this whole thing in Lean. We have a way to reason about all code uh 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 it are the properties that that code should have.
24:28So, can um maybe AI help us with this?
24:32Okay, here we have a demo of our tool called Verisforge. And what you can do is enter uh a specification in English of what you would like to build. And then it will uh build the code and do the formal proof. So, we can do a simple example.
24:51Uh says find the maximum element in an array of 32-bit integers. So, we click here and first thing it will do is it will generate a specification in structured language here. Um we can look at this and say yes, uh we approve. And then what it will do is go ahead and generate uh Rust code and a Vera specification um based on that uh structured language specification.
25:20And then it actually uh verifies it with the Vera tool and checks that the spec uh is unchanged. And so, now we have uh fully automatically verified uh code that has been generated.
25:34Okay, so that's a toy example again.
25:37Uh can we do better? Well, yes. Actually, um in a recent uh archive submission, uh we showed that uh 30,000 line Rust program, which is a crypto library, took uh five experts 3 months or three three experts 5 months to do were able to do it in 11 hours fully automatically with our crypto prover agent.
26:00[clears throat] Okay. So, that's just like a taste of what I think can be done in the formal methods space. I think formal plus AI gives us a way to, you know, what François was talking about, actually build some really strong defense, uh create some new primitives that could be used to build up uh an AI safety stack.
26:20I 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.
26:28Um 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 an A shows it and says, "Great, okay, I trust you. You can do that."
26:53Uh that would be a cool uh future.
26:56And the other thing that I kind of like about this work is it's uh 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. That So, if we can imagine ways to do those kinds of things, I think uh we'll be able to benefit from AI without you know, having a a bad outcome.
27:20Okay. Last thing I want to tell you is just a teaser. Um I'm co-CEO of a new company called And Truth. We are trying to build a universal code reasoning engine along the lines of what I told you uh today. So, uh keep an eye out for that. And I'll end there.
27:41[applause] Thank you so much.
27:46Okay. All right. Next up, Marco Koken Derfer.
27:52[applause] All right. Uh so, here here's the question. Uh 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 Intelligent Systems Laboratory or Sizzl. My graduate students call themselves Sizzlers.
28:11And uh for a system with learned components, um maybe it's a auto landing system for an aircraft, what evidence do you need to justify deploying it?
28:23So, for commercial air traffic, what we're aiming for is about a 10 to the minus nine probability of catastrophic failure per flight hour. So, that's what we were held to in the development of the ACASX uh aircraft collision avoidance system. Now, if you were to directly simulate these uh scenarios, then you would need about 10 to the nine simulated uh hours before you detect a on average a a single failure.
28:58And if you want to get a statistical representation of these types of failures, you're you're going to need like like if you need 10, then you need to run 10 to the 10 uh simulated hours before you get 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 5 miles and don't really present a hazard.
29:28Um instead you want to simulate critical scenarios that are representative of of let's say the airspace.
29:36So, how do you get that that distribution?
29:40Okay, we're in 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.
29:57And 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 those uh critical scenarios. Often what we want to do is actually estimate that probability of failure.
30:24And 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.
30:39Then uh another category is verification, which is the the subject of of Clark's lab and we've actually collaborated for a number of years. But the this is often treated as a different community and we're finding opportunities to 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 there is no one silver bullet.
31:10Probably formal methods won't take you the whole way there. Um although Clark is helping us get further and and further. Uh it really requires a number of different kinds of approaches. Uh we've also been looking at of course palm DP 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 and so forth.
31:45And we like to be driven by real-world problems uh including aircraft, driving, spacecraft, medical evacuation and so forth. And I'll mention a few of these. And uh we like testing them also in the real world. Of course it's great if we can simulate everything. Uh but our inferences about safety is only as good as the simulator.
32:10One 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 uh 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 uh since then a number of students have uh, since built a upon this this work.
32:40So, uh, 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 the world of validating language models. So, this is some of the work that my students, uh, Hujun Liu and, um, and, uh, Amelia Hardy and and others have been leading. So, with in the aircraft scenario, a failure is kind of well defined,
33:09right? It's metal on metal collision where they come within 500 ft horizontally and 100 ft vertically. For these language models, what we care about is, uh, 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 to provide that measure. And for this, uh, for this paper, we were using Llama Guard to measure toxicity.
33:38Now, 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 in the top left corner here, uh, when we, uh, search the space of scenarios.
34:04And if the most likely failure is super, uh, 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.
34:19Another challenge is estimating the probability of failure. And, okay, that the weird, uh, symbol there should be an E. It's an expectation. One way to approach failure probability estimation is to use a important sampling, which is an idea that has been around for a super long time. The idea there is instead of sampling from the the true distribution,
34:46we'll call it P, you sample instead from a proposal distribution, we'll call it Q, that focuses the effort on on scenarios that that are more significant. But you have to then re-weight them. And the re-weighting is actually quite simple. You just weight it by the different results by the probability of your uh trajectory according to the true model divided by the probability of the trajectory according to your
35:16uh your proposal distribution. And we've applied it to a number of different uh domains. We've looked at um uh bringing ideas from Gaussian processes to help represent uh these distributions. We've also looked at uh normalizing flows, the use of low-rank Gaussian mixture models to represent these proposal distributions. Uh we've also been using uh diffusion models, which has um they have seen quite a bit of success in other domains like image generation.
35:53So, 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 uh what you can see here is uh over time the angle. And we have a failure if if the pendulum uh exceeds an angle.
36:19So, in reality, it can fall over to the left or or to the right. If if you could afford to run a gazillion simulations and um and you look at the failures that that would be the 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 uh diffusion-based failure sampling, it will actually pick on uh pick up on both
36:49of those uh failure scenarios. And similar kind of story for the lunar lander.
36:57Uh we've also been working on neural network verification. Uh so, uh a while ago, actually, some work initiated by Francois, um we wanted to see if we can approximate the lookup tables for the ACASX uh collision avoidance system. I just using some neural networks to to with with the idea of compressing the information. Now, of course, we we didn't actually end up using neural
37:25networks for the real system, but it led to a really fun collaboration with uh Clark Barrett's lab. And led to the development of the Reluplex algorithm and and later on the the Marabou uh software framework. And over the years, we've been uh transitioning the the use of Reluplex and and Marabou to situations where you have a neural network controller in the loop.
37:52And uh some of the work by uh Chelsea Sidrain and and Sydney Katz um pushed some advances in in that direction. And then uh a student, Sam, who Clark and I are supervising, are looking at uh forward and backward reachability uh concepts. We've also been doing work on POMDP planning.
38:17Uh actually, one of our first efforts in the lab when I started at Stanford was to create a a very uh simple open source framework for specifying POMDPs. We wanted to make it really easy for non-experts to specify their their POMDPs. Kind of like for CVXPY, uh the idea of Steven Boyd's students was to make it really easy to specify mathematical optimization problems. So, that's what we wanted to
38:48It's a a Julia library. And uh my student Zach Sunberg, who's now a professor at CU Boulder, uh developed the POMCPow algorithm for scalable POMDP planning. Uh we've more recently been looking at constrained POMDPs. So, you might want to impose a hard constraint on on your problem. And we have also been exploring directions involving multiple agents.
39:19These are some of the domains we've been looking at. Uh medical evacuation, my student Body El Husseini Husseini, he's actually a uh an Army Black Hawk uh medevac pilot, and uh he has developed a a framework for uh simulating these kinds of scenarios. Uh I saw Duncan, he's been uh pushing our efforts towards uh belief state planning for spacecraft collision avoidance.
39:48And also working with Helen and and others on using POMDPs to plan out uh flight tests so that you can as efficiently as possible uh 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.
40:21Uh you want to validate uh what's going into your decision system. So, the the sensor inputs, we've done some work with Airbus on integrity monitoring of vision-based systems. Uh you also want to monitor what is happening in the internals of of the system. And this has led to some work on uh mechanistic analysis uh for an aircraft system. And of course, you also want to model uh and monitor the outputs.
40:56Okay, then there's a another uh set of work on assessing the measurements. So, uh Anca Rusu and and others have been uh pushing the the frontier on AI evaluation. Um uh we released the paper BetterBench. If you go to betterbench.stanford.edu, you can find uh all of the data about a number of different benchmarks uh and uh a number of lessons learned and best practices there.
41:32Uh we've also been studying when do these benchmarks stop being useful? When do we have these uh saturations in these benchmarks?
41:43Uh we've also been looking at what What do these failures look like um in terms of token-level signatures, uh reasoning failures. And we've also been looking at issues of uh human judges. So, in fact, another safety-critical area is the use of AI for mental health.
42:05And we've been looking at evaluations of mental health professionals. And we have been actually quite surprised to find that um human mental health professionals actually their opinions vary widely uh including in in domains related to uh self-harm. All right, I'll wrap it up here just mentioning our new trilogy uh So, the the first book is Algorithms for Optimization. The the second edition will come out in uh very early 2027.
42:41Uh optimization is fundamental to everything that that we do here. Um and it's a basis upon which we optimize decisions and that's covered in our 2022 Algorithms for Decision Making book. 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 uh learning-enabled systems and and other kinds of uh AI systems.
43:17Um it's available from Amazon and also turns out target.com. Uh 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.
43:54Thank you guys so much. That was amazing.
43:56Um So, I guess really to start the conversation uh you know, you guys saw this whole AI safety stuff. You know, what what was going through your mind when you saw this latest uh uh hysteria um saga going on?
44:13Maybe let's start with Clark.
44:15So 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 um you know, I think my response has always been the future is has high uncertainty, especially now. And so, it's a good idea to invest in AI safety research. Um but I also think it's not super helpful to emphasize like worst-case outcomes when you have no idea what the real
44:44probabilities are. Um and uh you know, any 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 They're just guessing. So.
44:58Uh we've both both cared about AI safety for some time. I think we started the Center for AI safety was a 2018, 2017?
45:07And uh it's fascinating to see that it has captured international attention. And uh I hope that this will uh lead to taking safety more seriously. I kind I I think that we need to borrow more ideas from the aerospace industry. And I can elaborate on uh Okay, fine, I will. Uh Please do.
45:37There There There has actually been some discussion of creating something like the NTSB uh for AI, and I think that could actually be a a good idea. Um So, compared to the 1970s, we're 80 times safer uh in commercial aviation uh than we are. Since Howard Hughes or uh since the 1970s. 1970s to now, we're 80 times safer.
46:02And how did how did we get there? So And what what would it what would it what would it look like? What would it be Would it be like an opt-in kind of thing? Would it be like guidelines Would it be strict like the FDA literally approving data? How would it work?
46:17Uh that that's a good question. So the the key thing here I think is independent. So NTSB was set up as an independent agency in 1967. And uh 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 from what went wrong.
47:02Now it take that there are other systems that uh were schemes that have built upon this. In 2007, there there was also the uh 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 it's going to take a long maybe uh too long of a time to set up a new agency. That's that's a big deal.
47:32Uh governments tend to be somewhat inefficient. Um the NTSB is also used globally. Um so if an accident involves a component manufactured in in the United States, they'll actually go go to other countries and investigate. Um To draw that analogy because it's such a high um hm there's so much interested parties.
48:02There is risk of regulatory capture and things like that. And then like, you know, if you look at uh medicine or you look at legal, there's the aboard of medicine. Even the internet has ICANN, right? It which is also international, self-regulated. DNS has been working great. Um and there hasn't but like it wasn't the case that, you know, imagine the internet invent was invented that same time that Google and Facebook were like already public companies and they were heavily
48:31biased in the development of ICANN. And maybe they said, "Hm, well, if you want SSL, you actually need um Google or Facebook to be the ones to give you SSL certs. Or you want a domain name, well, you really it's not safe to give everyone domain names. Like we we should be the ones to give you domain names."
48:48So, there's some risk there. And then even more so like um having government intervention, there's uh uh 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 com- compete. Right? And that's the concern that some people have. How do you think about all that stuff? I Maybe start with Clark.
49:13Uh yeah, so uh I I was encouraged, you know, by the recent um Frontier Lab leaders saying, "Yeah, we need independent evaluators." So, I'll just say one one of the goals of my company is to build systems that can be that independent evaluator. And not just 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.
49:37So, we would say, "All right, we've checked this system, and here's the certificate. You can now go check it yourself, and you can confirm uh that we got that right." So, I I think uh independence is really important. Um I I I there a lot of voices pushing for that because I think it would be uh you know a real shame if all of the safety was left in the hands of the labs or or even some um some friends of the labs who claim they're independent. Yeah.
50:06Yeah, I I I think we need something in the very near term before something like that could could be set up. It could be a not-for-profit or or something like that. I mean, in in the space industry, when you have a space launch, right? You have a range safety officer who's completely independent of the the mission. Their only job is to make a go no go go call based on objective safety metrics.
50:34Could it be as simple as a starting position as just US GAAP, which is like the US kind of the the uh um uh accounting principles uh generally accepted accounting principles? It could be generally accepted AI principles of like deploying AI safety. Um and then there's a KPMG and there's a uh you know, uh um Arthur Andersen or you know, whatever. That's like, you know, uh uh Ernst & Young that's going to be that you can choose, but you have to be validated um before you do something.
51:03Like, it shouldn't be everything. I should still be able to train the theta on my, you know, tiny box.
51:07Yeah, I I I I I think we need to develop, you know, best practices, uh of course, but I think we also need like a postmortem analysis as well. I think we we need to take the validation of AI seriously from a number of different perspectives.
51:25But, back to your point, I mean, I think um uh aircraft the airline industry does that really really well. They don't rush to print what happened. They do a They have a full thorough review process of every single accident that happens.
51:40Do you have any Um okay. So, uh my last question for the both of you is how tractable do you really believe these current AI safety um concerns to be? Specifically, maybe the cyber uh 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 to doing so, or I can um take an open weight
52:08model, and then I I I would need some defensive capabilities as we talked about earlier. Um how the whole thing, how do you think how tractable of a problem is is this?
52:18Yeah, I'll take a stab at that. So, I I think um cybersecurity is going to become very tractable. I think uh like right now, you know, I was telling my mother, um "Hey, if you prove the code, it can't be hacked." And she was just stunned, like, "Really?" You know, we're trained by the media and by television that like every system can be hacked.
52:37And well, of course, it is true right now. But uh it's quite possible, you know, you can prove with mathematical certainty that that you can't hack a system. And I I I will predict that within the next, I would say, 3 to 5 years, um that'll just happen.
52:51Like, all our systems will be completely secure. Because it it with AI can attack, but AI can also defend. And and the AI defense plus formal methods should get us there.
53:01So, what what is needed to get us there?
53:03To to have these lockdown systems? Is it like zero trust architectures? Is it like these best prac- even the admin admin issue? Um how do you think about it?
53:10Yeah, I mean, I think we just need to move to a new standard of code.
53:14Actually, it's interesting you're bringing up uh how how airlines and and other industries use, you know, very sound engineering principles. Uh 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. Uh 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 uh maybe to that. And And one other thing I want to say in terms of
53:43tractability of like securing AI itself, uh I don't think we'll be able to reason about, you know, these massive large language models. So, I think our best uh option is something more like securing the boundaries. Uh And securing the boundaries is also very tractable. Um trying to prove that, you know, a 500 billion parameter model isn't going to do something crazy, uh I think that's that's not really tractable.
54:11Completely agree with Clark on the security thing. Like, I'm terrified of um you know, the next big thing being a massive cyber attack. And but I think I I would agree with Clark that I have a lot of hope for that.
54:26Um but you can't prove what's possible or what's not possible with biology or chemistry, right? Uh that is uh that's an open question. But I think that's what we have been striving for as a species, where increased understanding. And I think that advances in AI will help us um on average. I think on average we're
54:55going to benefit from these new insights.
55:00Um I have a question specifically for um Clark here. So, um exactly walk me through how it works. Let's say that um you are now uh we give you $10 billion to be the CISO for Bank of America.
55:18Okay. What do they do? What's What would you do?
55:21Okay. So, first I would hire all the formal people and uh race race to build uh the infrastructure that we need to reason about that code. Then I would say, "Okay, give me all of your code. Uh uh, give me a whole bunch of GPUs and a whole bunch of theorem proving agents and we're going to just, um, 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, um, and then you're done.
55:50So, there there's a lot of work to do there, but I think it's, uh, it's work that we know how to do.
55:55And does that mean I have to finally get to 100% unit test coverage? Is that Is that what that means?
56:00No, you don't. You, uh, so tests actually become obsolete. I mean, tests are Tests are always good as you're developing. They're like the fastest way to find bugs. Uh, but ultimately the formal argument completely subsumes the tests.
56:15Um, all right. Now, for Michael, um, are you aware of Waymo, um, you know, uh, uh, some of the the Yes.
56:27[laughter] A number of my students work there.
56:31Um, using, uh, AST diffs, uh, this is some of the important sampling stuff, uh, you know, Marabou, Reluplex. Are you aware that they're using this in their validation and and their their theta validation procedures after they train a new a new model?
56:49Uh, I can't speak specifically about Reluplex or Marabou. Uh, Clark might have some insights there, but adaptive stress testing we released not just a Julia version, but also a Python versions for those who want to continue using obsolete languages, but [laughter] um, so we we we made it open. We've had, uh, a number of sponsors of our lab. We we've been, uh, supported by very
57:18generously by a number of different automotive manufacturers including Waymo. Um, with the aim to, um, uh, make these tools accessible not just to them, but to the entire industry.
57:32And I I And you talked about AST Prompter, these are applicable to LLMs as just as they are to a trained VAT that would control a gas pedal and a steering wheel, right?
57:44Yeah, basically you need two 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.
58:02And are you 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?
58:15Not yet. I mean, we we just published AST Prompter. We've been supported by the Schmidt Sciences. And the idea is to make all these ideas as accessible as possible.
58:30And do you think that they did adopt they would have equal levels of safety as the Waymos and and things like that?
58:37Um I don't know. Uh hopefully that it's it's a different thing validating physical systems than you know, language models. Although the methods can translate, the level of success that you can anticipate might vary a bit.
58:59I mean, I've heard arguments that well, um autonomy you know, we can define the failure modes pretty well if the thing stays on the on the road, if it you know, if it hits a baby and this and that.
59:13And like and then I meet I 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? And some of the long tail is a is always going to be a high probability. Um and and then they say, "Well, in in these And so in the LLMs, you know, can't we kind of isn't it kind of that
59:41same Is is there Is it meaningfully different long tail?"
59:45Yes. I I I think you're exactly right. So, I even for A cast X, we know that the probability is of failure is not zero.
59:54I mean, we have simulations that show that it fails in certain situations. It's just that those situations are just so incredibly unlikely.
1:00:04That That I mean, the International Civil Aviation Organization and the Federal Aviation Administration, their their standard for safety is not probability of zero probability being zero, right?
1:00:17Uh we have to be realistic. If anyone tells you they have created a a completely safe system that interacts with the in the real world, um and it's fully safe, yeah, I I I would would not believe that.
1:00:31Clark's got some guarantees for us.
1:00:32Uh Clark has some guarantees. Uh so, to use Clark's method and or category of of methods for formal methods, um and correct me if I'm wrong here, but you have to it you're 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
1:00:59aircraft or or whatever. And so, you generally have to assume bounds on that uncertainty.
1:01:07So, you have to estimate a nominal distribution on the input, on what's going to and on the transition function of So, in formal methods, you generally don't assume anything about probability distributions. You capture your uncertainty in in sets.
1:01:21And and that that's a different approach and it's great when it works, right?
1:01:27Because you get a nice proof. And and that that's wonderful. But the the question then is do those uncertainty intervals um are they sufficiently realistic?
1:01:41Just say something on that. So, um 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.
1:01:51I think what Michael's saying is it uh 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 uh that might not be a valid assumption, right? So, so you do it is really important uh when we talk with 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's
1:02:21it is 100% impossible for you to use a buffer overflow attack to attack that code.
1:02:26Uh but there are other things that there are limits to what you can do with formal, right? I mean, uh 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 dog, so that's beyond what formal can do." So, so there are limits. You have to be aware of that. That's something that I think the formal community has also really learned uh hard lessons that you have to state those assumptions or else people will be
1:02:57Um so, last question for me, um what's the Swiss cheese model? Are you making like grilled cheese sandwiches or something?
1:03:05What's What's that?
1:03:06So, uh we use the Swiss cheese model as an analogy in aviation safety, right?
1:03:12You have a number of layers of defense.
1:03:15So, like for aircraft collision avoidance, right?
1:03:19Um 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 then you have another layer, which might be air traffic control. Um and then another layer could be your collision avoidance system.
1:03:37And we call it Swiss cheese because these different layers have different vulnerabilities, right? Those are the 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 of the cheese.
1:03:55And and is so then applying this to these [clears throat] big large language models that are big and scary, I mean we control the training data, pre-train the RLHF, the RSI, all the data that's being sampled. We can take out the bad data.
1:04:11We can run So, like Percy 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 it's that stuff's never in the pre-train, so it can't possibly learn those bad things. And then you So, that's like step number one. Now, you have a trained data. Let's do a failure analysis on that data.
1:04:30Okay, let's estimate failures. Let's 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 and happens as well.
1:04:50Um yeah, what are your thoughts on that?
1:04:51Yeah, you you need all these layers. Um I I think the example you gave in your opening remarks, they had like the chain of thought monitor turned off, right?
1:05:03That that would be one of those layers.
1:05:05And I 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 the proper safeguards on the human level, right? Um So, like I mean, we've learned this from cybersecurity, right?
1:05:25A way to the typical way of breaking into a system is through human engineering.
1:05:30Yep. Awesome. Okay, I'll open up to the audience now. Um okay, in the front.
1:05:36[snorts] And we got Mike coming.
1:05:43Um I mean, this this question is for Clark. So, you mentioned that um you know, in a Bank of America like uh example I mean, most of the time, you know, then the price code and the real world code doesn't necessarily have a specification.
1:05:58So, in that case, like how would you um formally verify this code? Would you you know, get the I don't know, like spec or a assumption assumptions from the the source code itself or how would you do that?
1:06:12Yeah, that's a great question. So, I think uh in the new world where it's easy to write code and hopefully in the next couple years it's easy to verify code, the thing that's left that's hard is the specification. But uh 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. Um and for the audience, what does it what does a
1:06:41memory safe mean and why is that important?
1:06:42Yeah, yeah. So, that just just means that it's never possible for your code to access uninitialized or out of bounds memory.
1:06:49Who cares about that?
1:06:51Well, if you can do that, you can most likely run some kind of buffer overflow attack, which uh you know, is famously been used to gain access to all kinds of systems. In fact, I think the number was still sadly the number one security vulnerability is buffer overflow. Um yeah, so there are some specs like that.
1:07:11Uh there are also um 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 uh transactions, then the total amount of money should stay the same. So, you can you can come up with some of those general uh things. Also, it turns out agents are actually quite good at coming up with specs. So, uh I don't know if you've done a cloud code session recently, but often what I find is, you know, I tell I say, "I want this." And it's like, "Oh, yes. And you
1:07:40probably want this, this, and this, too." And I'm like, "Yeah, actually, you're right. I do want that." And so, I think uh agents can help us write specs, and I imagine a world where you have a 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.
1:07:57So, I mean, like for for example, you know, in the open-source model, like let's say, you know, you are formally verifying a VLLM or SGLang something like that. You could write, you know, formal spec um with assistance of agents. But how would you know that, you know, the even the the spec that agents, you know, write is, you know, the same as the developer wants or developer's intent?
1:08:22Yeah, so that there is a gap there, and you would have I think that's an interesting research area, which would be building uh tools and agents to help cross that gap. But 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.
1:08:42Thank you. And then going back to like having a smarter model, I'm 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 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 1 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
1:09:12videos on how they hack and [clears throat] and then you know, social attack. Well, a spec you might put in there is if the person has been there for less than 6 months and they haven't been through a you know, a a fake you know, social hacking scenario and haven't passed safety training or whatever, then maybe they don't actually aren't can't give passwords to you know, resets to new email addresses.
1:09:39You know, some stuff like that. That you can help you can think through all those things scenarios, but anyway, yeah.
1:09:46In the front here.
1:09:52Um so it sounds like you see formal verification as some kind of rigorous review process and drawing analogies maybe aircraft collision avoidance. Well, um maybe in engineering there's generally some amount of regulation since the safety standards that one company might not match the safety standards of another.
1:10:13So 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?
1:10:31[laughter] Um yeah, I think regulation can can play a role.
1:10:37I think Oh, uh the question was is there there a role for regulations? Different companies might have different I don't know, uh safety standards And if not, will how will you get everyone to adopt your formal verification engine?
1:10:56Ooh, uh I think the last part about that that the So in terms of regulation um uh one of my uh collaborators over the years has been Chris Gerdes. Uh he was a professor in mechanical engineering at at Stanford. He's now at Waymo. Um but he worked on automated vehicles and he was he went to Washington D.C. to help the Department of Transportation come up with um uh regulations for automated vehicles.
1:11:31In the end I think he and and everyone there kind of realized that it's a little bit premature to uh be too prescriptive in terms of what technologies to use but rather focus on higher-level best practices and um and standards at that level without being too prescriptive because this area is uh you know
1:12:00there's a lot of innovation that has been happening and and that will continue to happen. I think the important thing to realize is that um 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.
1:12:26And so I think this is an opportunity where um the industry really needs to work together in their particular domains, right?
1:12:36Automated driving, I mean those standards are just going to be different from language models or or other kinds of applications of AI.
1:12:47Yeah, so I about regulation I would just say um I I do think there's a role for it. I think you have to be careful like Michael said not to be too prescriptive, uh, but to find ways to incentivize, um, general principles that would that would be good for safety. Uh, in the specific case of formal, you know, I've been doing formal for 30 years trying to get people to do it. It it's a bad idea to try to tell people you have to do this differently. Um, I think what's different now is I think there will be
1:13:15market forces that incentivize it. So, if we can show that uh, formal is automatable, work 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, uh, advantage. So, I think, uh, we will see, you know, strong market forces help, uh, I I think actually all across AI safety.
1:13:40And the one benefit that I think, um, I I would like to underscore on 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 you you lost people because they said, 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,
1:14:09I don't know, $100, $1,000 in tokens, right? Um, and then on the on the it's really interesting point that you made, uh, Michael on, um, this 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 and things like and misuse of their models. That's bad marketing for everyone. And um, and Thomas Brown Tom Brown just actually said that up in up in, uh, Napa. And um, and I think what, uh,
1:14:38we should also say is that they all just went to the White House and signed a document with these four four bullets. So, I'd actually like they are actually agreeing on independent audits, some of these safety guardrails, and all these other things. They they all are going to do those things. All All six of the labs, including Nvidia, cuz Nvidia doesn't make Megatron.
1:14:59They're not included in the conversation very often, but they should be. Um so, there are there are 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. Um let's go from this side in the back there. Yeah.
1:15:20Thank you. Question for Anthropic. Uh curious, what what applications or markets are you targeting first? And, you know, how do you measure success in the real world?
1:15:31These specific applications you're you're targeting.
1:15:33Sure. Um so, I can't say too much about that. What I will say is our our very first priority is to build uh the capability to reason autonomously, automatically, efficiently, with a about code at scale.
1:15:48Uh we think it's sort of, you know, if you've heard of these uh labs talking about mathematical superintelligence, this is like code superintelligence. Like the ability to really reason precisely about code. We think once you have that, there's like 100,000 things you can do with it. Um you can imagine, you know, helping enterprise. You can imagine helping developers. You can imagine uh you know, helping with security. So, um So, yeah. That's the direction we're headed.
1:16:14Success is when all of the world's code is verified.
1:16:25Um first of all, thank you. Um second, uh when you are like LLMs right now are an a system in which humans are interacting with the code uh with 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.
1:16:48Do you think these type like how would formal help in this sort of attack? I'm just Yeah, so uh again there 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 uh code that we can prove something about. Um but there are things that can be done. So Amazon has a technology called automated reasoning checks uh where they actually look at the
1:17:18responses of an LLM and they try to extract uh using auto formalization what the domain knowledge is that the LLM's trying to communicate and then they check that against uh rigorous domain model. So there are some techniques even when it's all natural language that can be leveraged to uh provide some security and safeguards.
1:17:40When I was learning CS there was like SQL injection attacks, you know, Johnny drop tables I think was the the classic uh exploit CD. Um is there no equivalent like a model to look at the um user input and lint out uh prompt injection?
1:17:56Sure, but that's an arms race, right? So so you can Always trying to outdo each other.
1:18:02Um okay, let's I think we have two and two. I'll go in the way back there.
1:18:10Hi, so um yeah, this question's for Clark. Um so I'm curious in your Bank of America example, uh even if you formalize all of the software within Bank of America, the software relies on a lot of a long tail dependencies even down to the hardware level. You'll have to maybe formalize the x86 instruction set and then you have to It's been done. The x86 instruction set has been formalized by several companies.
1:18:36Well, what do you think about things like hardware level attacks like rowhammer and that sort of thing?
1:18:41Yeah, I mean I I think probably software is low-hanging fruit, hardware is a bit more difficult, but I I do think that uh 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 it 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.
1:19:05There's a bunch of startups doing hardware verification with AI's help. I think this technology is going to get better and better.
1:19:20Yeah, 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 US government for compassionate use cuz 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
1:19:48then, you know, maybe it's these guys aren't doing admin admin is their password, but um 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. Um the CEO of Adobe was kidnapped in the '90s, I remember. And well, I'm I'm kind of young, but I I heard about it. Um And so, [clears throat] I was curious is
1:20:15like could you have an AI system that's like so trustworthy that it could be your admin? Is this even like possible?
1:20:23Like you run it in like some confidential virtual machine. Just 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 um and and secure.
1:20:41I'll take that one, I guess.
1:20:45Yeah, I I think um a similar kind of question comes up in the aviation domain, right? Um especially with um uh aircraft-assisted suicides, right? Um and concerns over mental health the of um you know, human pilots. So, um yeah, the the question is, why don't you automate that? Just like how you I think you're suggesting automating the administration.
1:21:15Um So, I think it might be a little while until the Federal Aviation Administration will entertain that. The the way things are set up right now is that aircraft, even if it's unpiloted, um there's a pilot who is uh regulated and and certified by the the FAA. And if something goes wrong, they're responsible for it. So, I I think we need to think very carefully about responsibility. And that would be my concern with your suggestion.
1:22:01Yeah, I think the the Waymo um comparison is interesting one, right?
1:22:05Like Waymo's not perfect, but it is according to them, it is saving lives.
1:22:10So, you could imagine making the same argument there, but I think Michael's point is a good one, like who who do you blame if it uh doesn't go well? And does the company that makes the AI admin, are they willing to take liab- you know, legal responsibility if something goes wrong? If they are, then that suggests they did a really good job with their safety case.
1:22:31And this is actually um goes back to the point of like a a smarter and better AI system. If you like there's the the one um trend in uh in in uh information security is your trust uh based architectures. And so like you want to make sure that there's zero trust in any one of these systems that if you infiltrate one, you can't infiltrate everything else. Um and you know, if I had a a really smart
1:23:01always-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?
1:23:23Hmm." You know, and then so 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 so and and we've all had, you know, these century alerts for anyone that ran a company.
1:23:37And 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, the Acast has this issue as well where you like death by a thousand alerts. So you have to be really really targeted and I think AI uh watching the system can actually do a much better job with that. So. Um we'll take two more. I think we'll go here on the right here.
1:24:00Hi. Um first, I'm really appreciative of both of like I wanted to hear on formal verification and then also like standards and safeties uh especially like in physical systems. Uh so having a avionics professional or professor here is great. Um I wanted to hear especially because you touched on uh dynamical systems based models like diffusion models, normalizing flows. Um right now we have the Chinese labs pushing the frontier of efficiency. We
1:24:29have 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 uh and trying to fit uh math that we have discovered throughout the fields like and try to try to fit it to what
1:24:57we're observing, but we I'm trying to uh basically ask like do you think there is room for constraining uh training dynamics and intelligence or trying to map this frontier of uh interpretability and control on one axis and intelligence and capability uh moving from traditional statistical machine learning methods
1:25:26uh and signal processing and control theory over into uh yeah, deep learning and neural networks. Also, I'm sure I have uh messed up a lot of the terms I mentioned. I don't mean to just add in a bunch of buzzwords, but Like uh filtering gradients in some way.
1:25:44Uh okay. Yeah. Um No, the the this is a great question.
1:25:48So, I teach groups uh three times a year I offer an executive education program through the Stanford Graduate School of Business to executives, and I do another one um through HAI. And uh 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
1:26:15them 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 uh simpler, more interpretable method is more likely to be robust.
1:26:40And so, depending on their application, they should really be like if you can get away with linear regression or decision trees, you should you should be doing that. There's a lot of temptation right now to go straight to neural networks and transformers and and all that. Uh but that's that's often not the right way to to go.
1:27:01Um and so, I uh 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 I think this is a a very important topic. In fact, one of the chapters in the new validation book is on explainability.
1:27:30And that that was critical in getting AXI accepted as an international standard.
1:27:36Uh really quick like follow on. Like, do you think that it there is like market uh incentive or like enough uh like demand like where we could people building like constrained intelligence uh like they would be able like it would be feasible uh to compete with like with
1:28:04the frontier labs.
1:28:07So, so I would say that if you um manage to create something that is measurably safer, then that would be a competitive edge, for sure. And And I know that there are people out there thinking about how to do that. So, you know, hopefully they can figure that out.
1:28:24And if you, uh, uh, looking to start a company, there's these accelerators that you could apply to, and they give you money and guidance.
1:28:35Anyway, yeah, you in the back there.
1:28:41Hi, thank you so much. So, my question is internet era taught us a lot about security.
1:28:46Uh, so what do you think will we, like, copy from the internet era, or what we will learn something new from the internet, uh, uh, this generative AI era?
1:28:58Or, uh, authentic security, especially.
1:29:03So, that's for you.
1:29:07Uh, so, is the question what can we learn from the internet era that we could apply in the current era?
1:29:13Yes, and, uh, what do you think could be different from the internet era, as well?
1:29:20Yeah, so I remember going to a talk when I was a young professor at NYU, uh, on security, and basically said there are only two problems. One is people, and the other is computer bugs.
1:29:34So, I think we I think we can fix the computer bugs, but I don't think we can fix the people.
1:29:39[laughter] Uh, we But, but what's different is, I think, um, AI can be used in all all sorts of different creative ways. So, it could be used, you know, as Francois was saying, as kind of a a watchdog to maybe like catch some of the social engineering. Uh, it can certainly be used to accelerate things like formal methods to, you know, secure the systems. Um, yeah, may maybe even the, uh, AI admin idea is a good one, as long as there's still some humans in the loop. Um I
1:30:09always worry, you know, I don't know if any of you are ever watched the movie WarGames, old old school, but but you know, you turn everything over to the computers and then there's nobody if if there's something weird happens like uh that can go off the rails. So, I think we do need humans in the loop.
1:30:26Um there's a famous physics paper called More Is Different and um and it's kind of like the premise and 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."
1:30:44So, 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 DDoS's, but like everything breaks when you hit when you apply infinity to the to the number, everything breaks. And so, weird stuff can happen that exposes it. And I wrote
1:31:14the tweet today basically like, "There's a lot of systems that we just saw this with Iclear where 60,000 submissions submitted in 1 year, which is greater than the cumulus summation across all submissions in all history in 1 year." So, that that's like a big exponential.
1:31:29That E, the constant up there is a big number. And so, all review systems, which we we have many at uh Focal, for example, looking at the Century Alerts, looking at um customer, you know, support tickets, or whatever. If imagine college college admissions. Like a um you know, uh a Nash equilibrium, you know, optimal strategy for every single all all high school students is to apply to every single school in America.
1:31:57Why would you In fact, actually, sorry, the whole world should apply to all schools everywhere.
1:32:03It's expensive. Well, it's they're going to have to charge money. Yeah, if there's if there's, you know, if there's no fee, then then that's kind of the what has to happen.
1:32:12And then so how do you actually handle these human review in the loop systems?
1:32:15They get DDoS really hard. Um a real one that that just got discussed was um small claims court. So if your agent can file a small claims uh on for you and you don't need a lawyer anymore.
1:32:29What happens to the judicial 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 these systems need to be reevaluated.
1:32:40And so the more is different is really the learning that is going to be meaningfully different, I think, from the internet era from to to to now. We thought we knew what big scale was, but like human traffic will be 0% of internet traffic. Like That's going to be a zero is a very small number.
1:32:59Okay, we have time for one more question. Yeah, please.
1:33:05Um thank you. So this question is about benchmarking the benchmarks and the context is that I'm working in AI safety at LinkedIn and um the definitions of harms drift very fast.
1:33:19Uh even looking at something so small as toxic text or bias every 5 year the new generation has a new slang for everything. So uh how do you make sure that that slang doesn't show up in uh say hiring uh in the uh messages that you get from recruiters?
1:33:38Um how do you do how do you measure that right now is benchmarks, but benchmarks move very slowly. The public even in-house benchmarks have to be uh very costly and uh need to go through a lot of human review.
1:33:53What are your thoughts on how do we go uh from current uh state of the art? some labs publishing benchmarks and slow creation of benchmarks to a state where benchmarks are dynamic evolve as quickly as terms evolve?
1:34:13Yeah, great question and I I like your example there. Um Yeah, I I think we just like how I advocated for a continuously monitoring our AI systems, we should continuously monitor our our benchmarks. And uh the good news is that there are some quantitative methods for identifying distribution shift and um monitoring shift in language I I think we we just need to do.
1:34:45Nothing to add there.
1:34:47Okay. All right, here's one more. Last one.
1:34:50I'll just follow up with regard to better bench. I think one thing that I keep uh follow up with regard to better bench. 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.
1:35:08Uh I feel like somebody and maybe it 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 that just like we put up you know, reports that different benchmarks are broken or different evals are broken and then it just sits there.
1:35:28Like I have this paper, but some I'm just open call for somebody to like close the loop here.
1:35:36Yeah, I think uh I've seen that as well. You know, I had former student who was trying to evaluate um uh SQL queries and nobody could get better than like 70% and then he showed that like 30% of them were actually wrong.
1:35:51So, uh 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 cuz everyone's trying to move so fast. I don't know.
1:36:07Yeah, we we need version control and pull requests, issue filing, and and so forth. Absolutely.
1:36:15I actually think that a great idea for a startup is like a Apple App Store of benchmarks where there's curation, right? Like like that they don't just let anyone just throw an app onto the App Store. They go through a process. They 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.
1:36:38It's [snorts] like the wild It's like GitHub. It's like the wild west. And so like trying to find like the appropriate GSMA K, like it's actually non-trivial to find what is the actual right GSMA K cuz there's 600 different things called GSMA 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.
1:36:59[applause] Thank you so much.
