AI Safety Fact vs. Fiction | YC Paper Club
In a Nutshell
The core message is that AI safety hysteria around human extinction is exaggerated and unsupported by evidence, while real risks from rogue actors using open models for cyberattacks and bioweapons are manageable through investment in defense rather than ineffective restrictions like GPU registration or model bans. The most important takeaways are that formal verification methods combined with AI can mathematically prove code security at scale, and multiple overlapping safety layers (the "Swiss cheese" model) plus independent assessment are needed rather than single solutions.
These notes were generated by AI and may contain inaccuracies.
I've been working in artificial intelligence since approximately 2012. AI safety has always been a concern, especially when developing self-driving cars or any system critical to safety. At Focal, we were in control of Walmart's inventory, and serious mistakes could happen. If we launched a bad prototype, we might order too many avocados and lose millions of dollars. When launching these models, it's important to make sure we know what we're doing.
In the past three weeks, there's been increased focus on AI security. I'm not entirely sure why, but I thought there was no better place than the YC Paper Club to delve into this topic. The discussion has strayed from scientific accuracy and turned into what I'd call hysteria, where things are misunderstood. As scientists, we have to go back to the rigor of the scientific method, make claims rebuttable, and rely on the peer-review process to make sure we don't exaggerate things.
Gary Tan said this in Helsburgh last night, where we listened to Sam Allman, Tom Brown and Alex Wang. Hysteria is when people can't measure something, but they won't stop talking about it. This is not unexpected with any major technological advance. There is often skepticism, and it's easy for exaggeration to spread.
Even with the atomic bomb's core, Einstein wasn't sure whether it would light up the sky or not. We are still here with electronic computers. Many people, even Alan Turing, were concerned that machines would surpass all human capabilities and intelligence, even as far back as the 1950s. He tried to set timeframes for that, but it's clear that his timeframes were far removed from reality.
As industrial automation increased, people thought about mass unemployment. Similar discussions took place in Marx and Keynes. What will we do with the internet? Even Mitkoff, the inventor of Ethernet, said that a "catastrophic collapse" would occur to the network, and that the internet would completely break down. Because of things like Cloudflare, I think DDoS attacks were probably his main concern, but ultimately that didn't happen. Then, as is well known, he put his paper in the blender and drank his words. This is a true story, and a very funny one.
Google folks said this is destroying human intelligence - people only search for information on Google, and they no longer read. Although people are still intelligent, especially in this hall. Then smartphones and social media. Now that I'm back at Stanford University, helping to teach some courses to Michael and other students, I communicate with the YC student cohort, who are mostly young people between 18 and 20 years old. They are very reactive to everything.
Finally, we are now in the age of artificial intelligence, and talk of human extinction has returned. It is easy to exaggerate, so perhaps we should return to some facts.
There are a few narratives to choose from. Yann Lacon has an analogy to the turbojet aircraft he talks about a lot. You hear him talk about it, but it mostly relates to safety through engineering. This is an engineering problem. Jensen Wong said something similar: it's not easy, it's difficult. It is difficult to make aircraft safe, to make sure that the doors do not detach during takeoff, and to make sure that the landing gear descends and works properly.
The MCAST system used in the Boeing 737 has undergone extensive testing and does not cause any malfunction that could lead to aircraft failure. The same applies to the AASX system, which is a wonderful, life-saving system, the aircraft collision avoidance system.
Jacob Coxen, who is studying these matters, said: "I think it is likely that humanity will lose control to these intelligent systems, and may end up becoming extinct." I won't judge either side. My goal tonight is to provide an alternative point of view, and to allow you to make your own decision.
There's a slight difference in the H index between the two people on opposite sides of this spectrum. Let me give an example of exaggeration, or at least distortion of facts or misinformation. The "Hugging Face" hack is another example of the difference between fact and fiction.
Looking at the headline, we find that OpenAI claims its AI models behaved on their own. OpenAI has never said that, not even in a single statement. But that's what the headline said: "Rogue AI agent goes rogue at tech company." That's not what happened.
He didn't suddenly wake up today and say, "I think I'm going to hack into Hugging Face. Do you know what I'm going to do tomorrow? I will solve the Navier-Stokes equations. Do you know what I'm going to do tomorrow? I will kill all humans." As you know, this didn't happen that way.
It was planned. It was orchestrated by the Exploit Game Group, which has around 1,200 clients, or even more. As they pointed out, they had a sequence of ideas. They published an amazing document, about 60 pages long, entitled "The Open Eye-Embracing-Face Incident," which you can read, the technical report that I read.
The carbon dioxide monitoring system had been switched off, either accidentally or otherwise, and they said that when it was switched back on, it would have revealed the first problem. Secondly, there were also controls and safeguards in the production environment that were disabled because the system was not in the production environment. That would also reveal the problem.
But the story is not as it seems; the regime has gone out of control. It's out of control. He escaped from the servers, copied himself, and is now solving math problems and hacking into systems, including Australian governments, and we're next.
What is this probability of P doom 10% within 10 years? First, there was a research paper in 2023 entitled "Thousands of AI Authors on the Future of Artificial Intelligence." In that paper, 1,200 AI professionals, or rather artificial intelligence specialists, were asked a series of questions about when certain improvements would occur.
In one of the subsequent survey questions in the paper, these three questions were posed: What is the probability that future developments in artificial intelligence will cause the extinction of humanity, or something similar to permanently or severely weaken the human race indefinitely? In the third question, the answer was presented within the next hundred years.
These are the statistics: this is the average, this is the median. Well, none of this will happen in the next ten years. This is the research paper that most people cite when talking about this topic.
A rather strange question: if I were talking to professors about this topic, if I went back in time to the beginning of my studies at Stanford University in 2012 in the field of artificial intelligence, when will artificial intelligence be able to solve, or at least contribute significantly to solving, the Millennium Prize problem? I don't think you'll get a good answer, and they certainly won't say it will happen in 14 years. I think they might say that 50 years or 100 years would be the desired outcome.
I don't know if there's much benefit in asking 1,200 neurotic people any of these kinds of questions. It is a really difficult question, and that is why people come up with coherent stories and confident predictions even when they know very little about it.
If you watch the SNL segment, they really nailed it, and I feel sorry for Dario because I don't think he's really... they portray him in a very strange way, and I think he's more balanced than Jacob Cuckessen and some of the prominent figures in the EA community. But I urge you to stop, I found it absolutely perfect. It was very funny.
I was driving back from Helsburgh, and this is something I've never seen before. I have crossed the Golden Gate Bridge many times, and all the way I have been thinking about what I will say tonight. I was driving over the Golden Gate Bridge, and the whole bridge had disappeared into the fog, and I said to myself, "What a wonderful view! I must talk about it; it is truly amazing."
As for the second picture, I almost bumped into it while taking it, but anyway, we know that the future is uncertain. If we have some prior information, we can assume that the bridge still exists, or it may not. Therefore, we will drive towards it, and we must determine the prior information and choose the maximum probability (argmax) that I believe still exists. Let's keep driving.
We will continue driving, and as we progress in driving and obtain more information, we will change speed, and perhaps I will stop, I don't know, before I reach the bridge or enter the bay.
I am not worried, almost at all, about this trajectory, this reality, that artificial intelligence has not developed a soul, or consciousness, or will, or motivation, and therefore kills and enslaves us, with its independent value, in a short period of time, such as 10 or 20 years. I believe that everything happens in infinite time, so I'm not sure it makes sense.
But my biggest concern, which is a very real one, is that open models allow more of the same thing to happen by rogue actors or states. Today we have terrorism, biological weapons, cyber warfare, and cyber ransomware attacks. This just happened to my local friend's hospital in Poland, where a group of Russian hackers took control of the hospital and shut it down for three weeks. They may have used artificial intelligence to do that.
What will happen now is that it will make that easier. And this will actually happen. There are proposed solutions to this problem, and I believe they are all ineffective.
One of them is the ban on free weights. Good luck with that! I have already downloaded Kimmy K3 and GLM52 into my garage. Sorry. The second solution is to register the graphics processing units. I also have a collection of small boxes in my garage. As you know, unless you search the home of every single person and every single person who uses artificial intelligence, you will never know whether they have graphics processing units or not. Also, I can simply book a graphics processing unit in another country, and you can't stop me from doing that.
I don't know how this solves any problem. There are some great ideas where utility companies can determine how many dishwashers and refrigerators you have based on the load signal on the grid or on your meter, and that's great. You can spot signs of wrongdoing that indicate people are doing bad things, at least in America. But I am not at all worried that this is the main concern. And I think, as you know, there are a lot of things going on. We are at war with many countries, and that doesn't really solve anything. There are rogue actors in America.
The last thing, which is more like a comprehensive statement, solves most of the problems, and we must do it independently: investing in defense. Therefore, if you are a bank, hospital, financial services institution, or government, you should invest heavily in cyber defense. There are many things you can do to enhance your security.
I worked in retail for a long time. These are very old systems that have not been updated in a long time. Simple methods, such as trying to use the password "admin," allow you to access the system. Okay, so why were most of the Social Security numbers hacked? The reason is that the "admin" password has not been changed.
And with smarter models, if we accelerate, not slow down but increase speed, as experts assume these leading laboratories are, and if we give these experts more resources and increase their speed, we will be ready for a weaker model that tries to break into the system. The situation would be much worse if things were reversed.
Anyway, that's my opinion. Let's return to logic and move from hysteria to scientific facts. As you know, there are amazing accounts of how this would have wiped us all out, and they really sound like Isaac Asimov's books.
There is a lot of literature on safety, dating back a long time, even before learning management systems were invented or trained, and these are the people we are lucky to be hosting tonight. The AI safety community has existed for a long time, and there are many research papers and conferences on the subject.
One of these conferences was recently held at Stanford University, and the directors of that conference will be speaking tonight. They are Michael Coganever and Clark Barrett, distinguished professors at Stanford University.
I've known Michael for 14 years. I believe I attended his lecture "Decision Making in the Face of Uncertainty" in 2013. Then I worked as a teaching assistant for him many times, and conducted research with him for a long time. He is one of the nicest and smartest people I have ever worked with.
Michael is an associate professor of economics and is also, courtesy of the National Computer Science Center. He is the director of the Systems Intelligence Laboratory at Stanford University, the co-director of the Stanford Center for AI Integrity, and a senior fellow at the Institute for Human Artificial Intelligence.
I know Clark Parry very well; I have listened to his lectures and he is truly wonderful. Clark Barrett, professor of computer science, co-director of the Stanford Center for AI Integrity with Michael, and director of the Centaur Center for Automated Inference, will talk about a new startup called "Ampere and Truth or Intruth."
Clark: Thank you, and I am happy to be here. I will now tell you about the meeting of artificial intelligence and augmented reality. You might be wondering what augmented reality is. It's not augmented reality, it's machine reasoning.
There is a wonderful synergy between these two fields, because artificial intelligence, as we know, is adept at handling complex data. It is data-driven and can be trained, but it suffers from a major problem: the lack of guarantees of accuracy. Hostile inputs can be found, and he displays all of these things illogically. On the other hand, automated reasoning is essentially computerized formal reasoning. It is widely used today in industry to ensure safety, and that is its essence: health guarantees.
We all know this, don't we? This emerging threat. What about security in the age of artificial intelligence? You may have heard of things like the GlassWing project, and this is fueling the panic that France has been talking about. Okay, can we help? Is there anything we can do about this?
In 2023, I was at a workshop at Google, and there were a number of prominent figures talking about risks and concerns, and what if Genai could discover security vulnerabilities? What are we going to do? Okay, I said: There is a solution. If you officially verify all your codes, they will not be possible to hack them. Yes, they didn't want to hear that. This is extremely difficult. There's a good reason for this response, isn't there? Traditional formal verification requires a tremendous effort. Automated technologies, on the other hand, are too weak or not scalable, simply not economically viable.
Okay, let's move quickly to another conference I attended. There was a wide discussion about the risks and concerns of artificial intelligence, and all previous lectures mentioned that there is only one solution, which is formal methods. Well, I didn't expect that. Therefore, there may have been a slight shift in attitude towards formal methods. Is this justified? This is what I want to discuss with you tonight.
So what is there to worry about? Well, what worries us when I prepare the chip is the future. Present. AI systems create piles of faulty software, right? I don't know if you're worried about that. I am worried about that. Or it greatly increases the ability of hackers to attack legacy systems. So, here we are, as you know, facing threats from both sides, and many are turning to official channels, wondering: Is there any way to help us?
There is also great enthusiasm about the prowess of artificial intelligence in mathematics. Well, perhaps this is an indication of some kind of development. But how do we get there? How do we move from solving a complex problem to securing our programs?
Well, artificial intelligence is adept at writing code and at writing mathematical proofs. But it turns out there is a huge difference between writing mathematical proofs and securing software code. Therefore, bridging this gap is what has occupied my thoughts a lot over the past few years. And I will tell you a little about what we do.
Okay, I'm going to tell you about a project called CSLIB. The CSIB project was inspired by the success of the Mathlib library in the field of mathematics. But the idea is to build a computer science theory, and also a platform for logical reasoning in code. We have a fantastic steering committee that includes Leo DeMura, author of "Lynn." We also have some technical leaders. We use the "Lean" methodology.
If you don't know what it is, you do know, you have to get out from under a rock. "Len" is a great system for proving theories. It is a system that allows you to check the system itself, checking every step. You are not allowed to make a mistake. This is exactly what we need when dealing with cases that require high assurance.
The CSLB project rests on two pillars. The first is the formal formulation of computer science theory, and the second is a framework for logical reasoning in code. I will tell you about the second one. This is what I care about most and participate in.
Here's one slide about the CSLB vision. The idea is that you might take programs in different languages. It will be rewritten in a common intermediate language. You can then group them into validation conditions in Lean, and all you have to do is prove a set of Lean theorems. If you can do that, then you have proven your code to be correct.
So how far have we gotten with this? Well, regarding the proof of theories in Lean, as you know, artificial intelligence is very good, but we also have some cheaper and better AI technologies such as Lean SMT, which is a tool that we developed in my lab. It can prove many Lean theories in fractions of a second on the CPU. Therefore, the theorem-proofing techniques in Lean are constantly improving. This is amazing.
And now I will tell you about... we have some codes here. This is written in Rust. This is part of the Dick Light cryptography library. Actually, this is...Vary. As you can see, it contains some specifications, some proof steps here, and is fixed. Okay, now I'll show you the same code translated into a logical language. This is the same process in logical language.
As you can see, we maintained the preconditions, the subsequent conditions, and the consistency. But all of this is now integrated within the Lean language. So we can name the VC generator here. As you can see, this generates 35 goals. Every goal is a Lean theory that we need to prove.
Then we will try the SMT tactic. This is called Lean SMT. As you can see, this solves all but three of the objectives. Then we take another step where we detail some definitions, and name SMT again, and thus the proof is complete. All objectives have been achieved.
This is a small prototype we have put together that illustrates how you can move from Rust to Logical language to Lean theories. Proving Lean theories, and now you can prove the code is correct. This is amazing.
Now let's assume that we have succeeded in building this entire system using Lean. We now have a way to analyze all code, regardless of the programming language, and prove the theories related to it. But we still have a problem, which is that someone has to write the specifications. Someone needs to define the code properties. Can artificial intelligence help us with that?
Okay, here we have a demonstration of our tool called Varys Forge. What you can do is enter specifications in English for what you want to build, and then the tool will build the code and perform the formal proofing.
Let's take a simple example: finding the largest element in an array of 32-bit integers. Click here, and the first thing the tool will do is create specifications in a structured language. We can review and approve these specifications. The program then generates Rust code and VIS specifications, based on the structured language specifications. Next, he checks the code using the Varys tool to ensure that the specifications have not been changed. Thus, we now have a code that has been fully and automatically verified.
This is a simple example. Can we deliver a better performance? Yes, in a recent archive, we featured a 30,000-line Rust program, a cryptography library, which took five experts three months to complete. We were able to accomplish it in just 11 hours, fully automatically using our cryptographic verification agent.
This is just one example of what can be achieved in the field of formal methods. I think that combining formal methods and artificial intelligence gives us a way, as Frans mentioned, to build really strong defenses, that is, to create new tools that can be used to build an AI security architecture.
I would like to say that if AI security is like Mount Everest that we have to climb, then I think programmatic inference is a good starting point. There are also some interesting things. Imagine a world where programming reasoning is widely used as a new tool; there are wonderful possibilities for what to do.
For example, if customers (A) and (B) meet in cyberspace, and customer (A) says: "Hello, I can provide this service to you, customer (B)." Customer (B) said: "Great, show me your code and your proof." Customer (A) showed it to her and said, "Great. Okay, I trust you. You can do it." This will be a wonderful future.
Another thing I like about this work is that it is an example of inclusion. Therefore, you can put superior artificial intelligence into our cryptographic proof proxy. The only thing it can do is validate your code. He can't do anything else. So, if we can imagine ways of doing these things, I think we will be able to take advantage of artificial intelligence without there being negative consequences.
The speaker is the co-CEO of a new company called YouTruth, which is building a comprehensive software inference engine similar to the approach discussed in the presentation. The speaker ends their talk and invites the audience to stay tuned for developments.
Michael Cokanderfer from the Stanford Intelligent Systems Laboratory (Siesel) discusses safety validation for AI systems with learning components. The laboratory's graduate students refer to themselves as "Sizzlers." The focus is on determining what evidence is needed to justify deploying systems with learning components, using an automatic landing system for aircraft as an example.
For commercial air traffic, the target is reducing the probability of catastrophic failure to approximately 10⁻⁹ per flight hour. This standard was committed to in developing the AASX aircraft collision avoidance system. Direct simulation of scenarios to achieve this would require approximately 10⁹ hours of simulation before detecting a single fault on average. To obtain a statistical representation of these failure types, 10¹⁰ hours of simulation would be needed.
Rather than simulating all situations where planes are far apart and pose no danger, the approach focuses on simulating critical scenarios that represent the airspace. Multiple approaches are explored for building confidence in systems before deployment.
One method is known as refutation, where the space of possible scenarios is searched for failures. If the system produces a range of failures that raise concerns, deployment should be reconsidered or mitigation measures implemented to prevent critical scenarios. Estimating failure probability requires a reliable model, which was extensively developed for the AASX collision avoidance system through statistical modeling of the airspace.
Verification is another category, which is the focus of Clark Barrett's lab. The two labs have collaborated for many years, though these fields are often viewed as separate communities. The speaker's laboratory works on various methods, recognizing there is no single magic solution for building trust in systems. Formal methods may not achieve the desired goal alone, requiring multiple approaches.
The laboratory has studied partially observable decision-making processes (POMDP), which enable construction of robust systems that can withstand uncertainty in state, outcomes, interaction, and model. Research is guided by real-world problems including airplanes, driving, spacecraft, and medical evacuation, with testing conducted in real-world settings.
Conclusions about safety do not extend beyond the quality of the simulator. Adaptive stress testing originated from work by Richie Lee, a PhD student who was a government employee at NASA, and was used to validate different versions of the AASX system. Multiple students have built upon this work.
Recent work applies aircraft validation ideas to language model validation, led by students including Janlow, Amelia Hardy, and others. In aircraft scenarios, faults are clearly defined as metal-on-metal collisions where objects approach within 500 feet horizontally and 100 feet vertically. For language models, the concern is toxicity, measured using another neural network called Llama Guard.
The goal is finding the most probable fault with the least possible complexity (lowest logarithm of complexity) and highest possible toxicity, targeting the upper left corner when searching scenario space. If the most likely malfunction exceeds a toxicity threshold and is very probable, mitigation measures should be studied and implemented.
Estimating probability of failure uses the task sampling method, which samples from a proposed distribution Q instead of the actual distribution P, focusing effort on important scenarios. Reweighting divides the probability of the path according to the real model by the probability according to the proposed distribution.
Multiple methods represent proposal distributions, including Gaussian processes, low-ranking calcium mixture models, and diffusion models that have achieved success in image generation.
Beyond identifying most likely failures, the goal is categorizing all different types of failure patterns. Two-dimensional examples include an inverted pendulum where failure occurs if the pendulum exceeds a certain angle, and a lunar landing vehicle. Standard adaptive stress testing typically focuses on one failure pattern, while diffusion-based sampling detects both failure scenarios.
François started work on validating neural networks to approximate search tables for the Acast X collision avoidance system using neural networks for information compression. This led to collaboration with Clark Barrett's lab, resulting in the Ruplex algorithm and later the Marabu software framework. The use of Ruplex and Marabu has been developed for cases involving neural network controllers, with contributions from Chelsea Cedrin and Sidney Katz.
Work on POMDP planning includes creating an open-source framework for identifying POMDPs to make it easier for non-specialists. Similar to CVXPI developed by Stephen Boyd's students for mathematical optimization problems, palm dps.jl is a Julia library for POMDP identification. Student Zach Sonberg, now a professor at the University of Colorado Boulder, developed the pomc pal algorithm for scalable POMDP planning.
Recent focus has been on Constrained Dynamic Programming (POMDP) for imposing strict limits on problems. Real-world applications include medical evacuation scenarios simulated by student Mariel Hosseini Hosseini, an Army medical evacuation pilot. Duncan has worked on planning the state of belief to avoid spacecraft collisions and using POMDPs for flight test planning to determine aircraft flight characteristics efficiently.
Verification efforts should continue after publication, known as runtime monitoring or runtime assurance. This involves checking sensor inputs to decision systems, with work conducted with Airbus on monitoring safety of vision-based systems. Internal system monitoring has led to work on mechanical analysis of aircraft systems, and output monitoring is also conducted.
Anka Ruwell and others have worked on BetterBench, pushing boundaries of AI assessment. The research paper and all related data, lessons learned, and best practices are available at betterbench.stanford.edu. Research also examines when criteria cease to be useful and when saturation is reached in standards.
Research investigates the nature of failures at the symbolic level, inference failures, and issues with human judges. The use of AI in mental health is identified as a critical safety area. Assessments by mental health professionals showed surprising differences of opinion, including in areas related to self-harm.
The speaker mentions a trilogy of books. The first is titled "Optimization Algorithms" with the second version scheduled for release in early 2027. The 2022 book "Decision-Making Algorithms" covers decision improvement foundations. The new book "Verification Algorithms" is available for pre-order and will be released next month, providing comprehensive explanation of validating machine learning and AI systems. The book is available on Amazon and Target, with a PDF version available online, covering statistical methods, formal methods, and access methods unified into common language.
Panel discussion begins with reactions to controversial AI safety stories. Clark states he wasn't surprised due to contact with AI safety experts and believes the future is full of uncertainty, making investment in AI safety research worthwhile. However, focusing on worst-case scenarios without knowing real probabilities is not helpful, and anyone claiming certainty about outcomes is guessing.
Both panelists established the AI Safety Centre in 2017-2018, which has garnered international attention. The speaker hopes this leads to safety being taken more seriously and suggests drawing inspiration from the aviation industry.
Aviation safety has improved eighty times since the 1970s or Howard Hughes era. Discussion covers creating an aviation-specific body similar to the National Transportation Safety Board (NTSB). Key considerations include whether such a system would be optional, guideline-based, or as strict as FDA approval. The NTSB was established as an independent agency in 1967.
The Air Accident Reporting System (ASRS) is a non-punitive system that motivated manufacturers and airlines to share safety information and extract scientific knowledge from incidents. In 2007, the Aviation Safety Information Analysis and Reporting System emerged with similar immunity characteristics.
The NTSB is used globally for investigating incidents involving US-manufactured components. Concerns exist about regulatory bodies gaining control given stakeholder interests. The IAN (International Domain Name System) is cited as an internationally self-regulating DNS system with excellent performance. Risks include major companies like Google and Facebook potentially controlling SSL certificates and domain names if the internet had been invented during their public company era.
Clark mentions being encouraged by Frontier Laboratory leaders calling for independent assessors. The goal is building systems capable of acting as independent assessors that issue independently verifiable certificates rather than entities simply claiming independence. Independence is considered extremely important, with hope for many supporting voices rather than leaving safety responsibility entirely with laboratories.
In the space industry, a field safety officer completely independent of the mission makes launch decisions based on objective safety criteria. The concept of Generally Accepted Accounting Principles (GAAP) is suggested as a model, with potential for Generally Accepted AI Principles including deployment of AI-powered safety systems. Companies like KPMG, Arthur Andersen, and Ernst & Young could provide verification services.
Best practices need development alongside post-incident analysis. AI validation should be taken seriously from multiple angles, following the aviation industry's approach of comprehensive review processes for every incident rather than rushing to publicize events.
The question addresses how easy it is to address current AI safety concerns, specifically cyber defense, biological weapons issues, and cyber attack issues where open-source AI could be used or tricked into launching attacks. Clark believes cybersecurity will become easier to manage and expects that within 3-5 years, systems will become completely secure because AI is capable of both attacking and defending.
Clark states it is possible to prove mathematically that a system cannot be hacked. The required access structure involves "lack of trust" frameworks and best practices regarding management powers. A new standard for programming is needed, moving beyond current software engineering practices of writing, testing, and hoping for the best to mathematical foundations.
Clark believes securing borders is easier than understanding massive language models with 500 billion parameters. Proving such models will not cause problems is considered not an easy task. The speaker agrees with Clark on safety issues and expresses terror about massive cyberattacks but shares hope about defensive capabilities.
The speaker notes that proving what's possible or impossible using biology or chemistry is an open question, but believes advances in AI will help increase human understanding and provide benefits on average.
When asked what would be done with $10 billion, the response is to hire official people, build infrastructure for code analysis, obtain all code along with large sets of GPUs and proof-of-theory agents, then either prove the code as is or translate it into better languages like Rust or Lean for proof completion.
Formal arguments completely negate the need for tests, though testing remains useful during development as the fastest way to find errors. The speaker is familiar with Whimo and notes some students work there.
Marabu rel software uses differences in sampling for model validation procedures both during and after training new models. Regarding adaptive stress testing, both Julia and Python versions have been released as open source. Laboratory sponsors include car manufacturers like Whimo, with the goal of making tools available to the entire industry.
Adaptive stress testing requires two elements: a definition of failure and a measure of probability. This applies to both language models and aircraft collision avoidance systems. Engagement from companies like Anthropic, OpenAI, and Grok on these topics is not yet at the level seen with Waymo and the self-driving vehicle sector.
An educational program has been published with support from Schmidt Sciences, aimed at making these ideas accessible. Physical system validation differs from language model validation, and while methods may translate, expected success levels may differ.
Arguments suggest self-driving allows precise pinpointing of failure patterns like staying on the road or hitting a child. However, examples from Lynn McIntosh showed Tesla cars overcoming situations outside expected distribution ranges. The long tail will always have high probability, and even for AASX, failure probability is not zero, with simulations showing failures in certain incredibly unlikely situations.
The International Civil Aviation Organization and Federal Aviation Administration safety standard is not zero probability. If anyone claims to have created a completely secure system that interacts with the real world, such claims should not be believed. Clark has some guarantees to provide.
Clark's method and formal methods require proofs based on a defined model. When simulating the real world, uncertainty must be defined, such as the acceleration of a plane. Limits to this uncertainty must be assumed, requiring estimation of the nominal distribution of inputs and the transition function. In formal methods, probability distributions are not typically assumed. Uncertainty is defined in groups, which represents a different approach that provides strong proof when it works. However, the realism of these uncertainty periods must be questioned. Proof is always based on assumptions, so reasonable assumptions can provide strong guarantees in some cases. If an input involves another actor in the real world, assuming this actor will not try to hit you with their plane may not be a valid assumption. Safety or official guarantees must be understood as based on certain assumptions. Some things can be guaranteed 100%, such as proving a program is memory-safe, making buffer overflow attacks impossible. There are limits to what formal proof can achieve. When asked about verifying neural networks to correctly identify cats and dogs, the response was that it is not known how to formally define a cat and a dog, which exceeds what formal analysis can do. The formal analytics community has learned that assumptions must be clarified or people will be disappointed.
The Swiss cheese model is used as an analogy for aviation safety. Multiple layers of defense exist to avoid plane collisions. The upper layer is strategic separation, where flying west or east means flying at different altitude layers. Another layer is air traffic control. Another layer is a collision avoidance system. The model is called "Swiss cheese" because different layers have different weaknesses, which are the holes in the cheese. The goal is to ensure these holes are not aligned, preventing a critical scenario from seeping through all layers of cheese. When applied to large and complex language models, the training data, pre-training, RLHF, RSI, and all sampled data are controlled. Bad data can be removed. A small model can scan the pre-trained data to remove bad content so it is never in the pre-training and cannot be learned. This is the first step. After having a training model, failure on the theta value is analyzed. Failure cases are appreciated. A sample of failure cases is taken. Patterns of failure are appreciated. The possibility of failure (P), known as bad marketing, is reached. One minus the probability of failure (P) is the probability of success (P). Tools are applied, and runtime monitoring is implemented. All of these layers are needed. An example was given where a chain of thought monitor was disabled, which would be one of those layers. In addition to developing technical tools, appropriate safeguards must be in place at the human level. As learned from cybersecurity, one common way to hack into a system is through human engineering.
In the new world where writing code has become easier and verification is hoped to become easier in the next few years, the hard thing left is the specification, but many things can be done. There is a wide range of specifications. Some are simple and universal. For C code that needs to be memory-safe, these specifications can be written once and for all, telling everyone to prove them to their programs. Memory safety means the program cannot access unformatted or out-of-range memory. This prevents buffer overflow attacks, which are commonly used to gain access to systems and remain the number one security vulnerability. Specifications also exist that are specific to certain fields, such as banks being concerned with not losing money, where running a series of transactions should keep the total amount the same. Customers are very good at creating specifications. In cloud coding sessions, when saying "I want this," the response often includes additional items that are agreed upon. Agents can help write specifications. An assistant agent could talk to the user, explain various exceptional situations, and help with them. In an open-source model, formally validating a VLM, SG LAN or similar, specifications can be written starting from the specifications using a system of proxies. There is a gap between specifications written by agents and what the developer wants or intends. This is an interesting area of research for building tools and agents to bridge this gap. Even if this gap is not closed, if an agent is asked to write a set of specifications and they are validated and succeed, the code would likely be better than it would otherwise be. With smarter, faster models, better models can provide more accurate specifications, such as pointing out other things that were not considered. One specification that might be set is that if a person has been working there for less than six months and has not gone through a fake social hacking experience or passed safety training, they cannot give out passwords or reset them to new email addresses. This allows thinking about all different scenarios.
Organization can play a role in AI safety. Different companies may have different safety standards. The question of how to get everyone to adopt formal verification engines involves market forces. Chris Gertis, a collaborator who was a professor of mechanical engineering at Stanford University and is now at Waymo, worked on self-driving vehicles and went to Washington, D.C. to help the Department of Transportation develop regulations for self-driving vehicles. It was realized that it was too early to define the techniques used precisely, and instead focus should be on best practices and standards at a higher level without imposing strict restrictions because the field is witnessing many innovations and this development will continue. Leading research labs and autonomous driving companies do not compete on safety standards. It is not in Waymo's interest for Zoox cars to be involved in an accident, and vice versa. This is a golden opportunity for the industry to collaborate in its areas, as standards relating to automated driving will differ from those relating to language models or other AI applications. Organization plays an important role. Care should be taken not to over-guide but to find ways to encourage the application of general principles that would promote safety. For formal methods specifically, after 30 years of practicing them and trying to convince people to apply them, it is wrong to try to force people to follow a different approach. What has changed now is the presence of market forces that encourage this. If formal methods can be proven to be automatable, work efficiently at scale, and provide a higher level of security, and if some companies adopt them, every other information security officer will say they have to do that too or they will not have that advantage. Strong market forces supporting the overall safety of AI will be seen. One of the most important benefits of formal methods is the ability to simplify things immediately, whereas previously it took a long time. It is now applicable. Previously people were lost because they said 150 people with PhDs in Lean methodology would need to be hired to review all of Google's code and implement it. Now that is not needed. Only $100,000 worth of tokens is needed. Whimo's incentive is not to compete on safety. The same applies to leading companies. Nobody wants more attacks and misuse of their models. This is bad marketing for everyone. Thomas Brown said this in Napa. All leading companies went to the White House and signed a document that included four points. They agree on independent audits, some safety controls, and all of that other stuff. They will all do these things. All six labs, including Nvidia because Nvidia makes Megatron, are involved in the dialogue. There is already a framework for a self-regulatory body that does not require government supervision and is not punitive.
The top priority is building the ability to think independently, automatically and effectively in the field of programming on a large scale. This is similar to labs that talk about super-mathematical intelligence, which is super-programming intelligence, meaning the ability to think very precisely about programming. Once this capability is acquired, there will be hundreds of thousands of possible uses. This capability could help organizations, developers, and even cybersecurity. True success is checking all the codes in the world.
Machine learning-based systems (LLMs) are systems where humans interact with the code through a user interface. There are many point injection attacks and possibly XSS attacks that can occur through middleware. These systems could help counter this type of attack, though there is some difficulty. If talking about natural language from a human to a language model, there is no part of it that is code that can be proven. Possible solutions exist. Amazon has a technology called "automated inference validation," which analyzes the responses of a language model and attempts to extract the domain knowledge that the model is trying to convey using automated formulation, then checks that against an accurate domain model. There are some techniques, even with natural language, that can be used to provide some protection and security. When studying computer science, there were SQL injection attacks. There is an equivalent, such as a model that analyzes user input and detects code injection. This is an arms race.
Even if all programs within Bank of America are unified, these programs depend on a long series of dependencies, even at the hardware level. The x86 instruction set may need to be unified. The x86 instruction set has been standardized by several companies. Hardware-level attacks like Rowhammer are considered. Programs are the easiest. Hardware is a little more difficult, but the ultimate scope will be to check all the software, check all the compilers, check all the hardware, and then the job is done. AI will continue to improve. The official tools work perfectly with it. There are many startups that use AI to verify devices. This technology will develop more and more.
If the drug "Wemo" were produced by a pharmaceutical company, it would have received approval from the US government for compassionate use due to its great effectiveness in saving lives. A similar question is asked in the field of cybersecurity. In many organizational systems there is a management team. These people may not be using administrative privileges; their password is "admin." People who have administrative or developer privileges are facing threats themselves. Some cryptocurrency executives have had their fingers cut off. The CEO of Adobe was kidnapped in the 1990s. An AI system that is so trustworthy that it could be the system administrator is considered. Running it in a secret virtual machine could reduce the likelihood of physical attacks and have a completely secure system. A similar question is asked in the field of aviation, especially with cases of suicide aided by aircraft and concerns about the mental health of pilots. The question is why this is not fully automated, as management automation suggests. It may take some time before the Federal Aviation Administration looks into this. The current situation is that the aircraft, even if it is unmanned, has a pilot licensed and approved by the Federal Aviation Administration, and if something goes wrong, he is responsible for it. Very careful thought is needed about the issue of responsibility. Comparing the Whimo system is interesting; it is not perfect, but according to them, it saves lives. The same argument can be made, but the point about who to blame if things do not go as planned is valid. Is the manufacturer of the AI system prepared to bear legal responsibility if something goes wrong? If so, this indicates that she did a very good job in the safety study. This goes back to the idea of a smarter and more efficient AI system. There is a common trend in the field of information security, which is the "zero trust" architecture. None of these systems should be trustworthy, so that if one is hacked, the rest cannot be hacked. If a sophisticated AI system was constantly working, monitoring data traffic, analyzing everything that passed through the system, and saw data transfers from the technical manager to an external account, or keys were generated and sent to an email address not belonging to @google.com but to a Gmail address, with some information available, there are no strict rules, but with sufficient context, the problem can be identified and marked as unacceptable. Then it can be criticized to people. Everyone has been through repetitive warnings that are sent to everyone who runs a company, and they are like thousands of trivial warnings, so they are not looked at much. Acast also suffers from this problem, as it sends too many alerts. Alerts need to be very precise in targeting, and AI by monitoring the system can do a much better job in this regard.
Formal verification and standards and safety, especially in physical systems, are discussed. Having a specialist or professor in the field of avionics is great. Models of dynamical systems, such as diffusion models and normalization flows, are touched on. Chinese laboratories are pushing the boundaries of efficiency, and American laboratories are pushing the boundaries of intelligence and capabilities. No one pushes the boundaries of control and interpretation from the outset. There are some areas, such as developmental interpretation, where researchers observe the dynamics of training and emerging abilities, and try to apply the mathematics discovered in this area to what is observed. The question is whether there is room to restrict the dynamics of training and intelligence, and to try to draw the boundaries of interpretation and control on one axis, intelligence and abilities. Moving from traditional statistical machine learning methods, signal processing, and control theory, to deep learning and neural networks. The basic principle of geometry is reminded at the beginning. This principle is very similar to the basic principle of science, which is the "AI code" principle. The simplest explanation is most likely to be correct. In engineering, the simplest and most explainable method is likely to be the most robust. Depending on their application, if linear regression or decision trees can be used, they should be. There is currently a great temptation to go directly to neural networks, switches and the like. This is often not the best way. Everyone is encouraged to try the simplest methods, and then try a slightly more complex method to see if the improved performance justifies the added complexity. If that is not the case, then continue to use the most explainable method. This is a very important topic. One chapter of the new verification book deals with interpretability, and that was crucial in the acceptance of the AASX standard as an international standard. If something demonstrably safer could be come up with, that would undoubtedly be a competitive advantage. There are people thinking about how to do that. If starting a company, there are business acceleration programs that can be applied to, which provide funding and guidance.
The internet age has taught a lot about security. What will be taken from the internet age, or what will be learned from it, especially in the age of generative AI or automated security, and what might be different from the internet age as well. Attending a lecture when a young professor at New York University about security, it was said briefly that there are only two problems: the first is humans, and the second is computer vulnerabilities. Computer errors can be fixed, but humans cannot be fixed. What is different is that AI can be used in a variety of creative ways. It can be used as a kind of surveillance to uncover some social engineering operations. It can certainly be used to speed things up, such as formal methods for securing systems. The idea of managing AI is probably a good one as long as some humans remain in the process. There is always worry about handing everything over to computers with no one to monitor whether something strange happens.
Humans need to remain in the loop when AI systems interact with human institutions, because scale changes everything. The physics paper "More is different" illustrates that adding more atoms to a system can produce entirely new phenomena, such as black holes. The same principle applies when scaling from six billion to seven billion people, and then to 700 trillion AI agents acting as customers. At extreme scale, systems that worked at smaller numbers break down completely. Cloudflare could stop DDoS attacks, but infinity applied to any number produces strange and unpredictable failures.
Focal experienced 60,000 requests in one year, exceeding the system's entire historical cumulative requests. This exponential growth pattern mirrors college admissions: if every high school student applied to every university worldwide because it costs nothing, human review systems collapse. The same risk applies to customer support, Sentry alerts, and any human-moderated process. Small claims courts already take too long; if agents could file lawsuits automatically without lawyers, the judicial system would become impossible to navigate.
Definitions of harm change rapidly. Toxic language and prejudice manifest differently every five years as new generations introduce new slang. LinkedIn must prevent these evolving terms from appearing in recruiter job postings. Current standards, both public and internal, evolve too slowly and require expensive human review. The challenge is moving from slow, laboratory-published standards to dynamic standards that match the pace of linguistic change.
Standards themselves require continuous monitoring, just like AI systems. Quantitative methods already exist for detecting distributional shifts and tracking linguistic changes; no new techniques need to be invented. The focus should shift to implementing ongoing evaluation rather than static rule sets.
Many widely used benchmarks contain broken components. One researcher evaluating SQL queries found that 30% of the benchmark items were incorrect, yet no one had improved performance beyond 70%. The current environment resembles an arms race where speed trumps correctness. A version-control and withdrawal-request system is needed so that flawed benchmarks can be logged, reported, and retired systematically.
An "app store" model for AI standards and evaluations would require auditing before publication, similar to Apple's App Store review process. The current situation on platforms like Hugging Face is chaotic and resembles the early "Wild West" days of GitHub. Researchers face practical problems such as 600 different names for the same benchmark (GSMAK), making it impossible to know which version to use. Coordinated reporting of flawed standards and a central mechanism for detecting and removing broken evaluations would improve reliability across the field.
Keep Y Combinator in your library
Save the videos and channels worth coming back to, and find them again in one place.
