Episode 27 — Verify the Output, Not the Model: Formal Methods and the Future of AI Safety

Introducing Christian Szegedy

Sunil Baliga: Okay, welcome all, Token Drop Podcast, episode 27. Been six months already. We have a very special guest today joining us, Christian Szegedy. He was one of the co-founders at xAI. He spent many years at Google in a variety of roles — research scientist, really a renowned mathematician.

I want to get out of the way here so Sajjad and Sam can get to the questions, because they're very excited to talk to Christian today. So, welcome, Christian. I was looking at your background, and you, like me, started off in the chip world. I saw some of the things you'd done — in the chip world, we used to do formal verification of RTL to netlist, to make sure the two were equivalent. When you converted RTL to netlist, the actual physical design should be the same. It seems like that's carried through your career, in a completely different domain, which is AI. You're kind of checking to make sure the output of a generative LLM is actually, in some way, able to be formally verified. Is that right? Is that the theme that's carried you through?

From Chip Verification to AI Verification: Why the Theme Generalizes

Christian Szegedy: In some way, there's definitely that. If you say it's unrelated, I don't buy it completely — I think it's more like a generalization of that very specific instance. You could look at it like AI could be used for designing chips, and then we'd still want to verify it — so it contains, as a special case, the other problem. But yeah, chips were very special. They were super expensive to tape out, and still are, so any single mistake was much more costly in a chip. Recalling a chip was very expensive too — for example, the floating-point error in the Pentium. The costs were much higher, so there was much more danger there. One of the reasons we haven't put a lot more formal verification into software — which we could have already — is that the cost doesn't justify it.

But now I think everything changes, because AI makes everything... you have a lot of ways of breaking into systems. We'll have much more AI agents roaming the internet, trying various things, and as we've seen even over a short period, they can lead to various security breaches. I think formally verified software can alleviate some of those concerns.

Security Implications: AI Agents Breaking Into Systems

Sajjad Khazipura: Indeed, that's really what we've been hearing over the last few weeks — about OpenAI's agents breaking into other people's assets. That really speaks to, once again, as you generalize your theory of formal verification, it can find applications in security. I was wondering whether governments and regulated industries might require a stamp of formal verification for certain applications or certain classes of applications.

Do Regulated Industries Need a Formal Verification Stamp?

Christian: That has been the case historically. Even in the '90s, there were various standards — different levels of security for software. Software used in the military, for example, was the highest level, requiring formal verification. So that's nothing new — the question is which level we actually require that certainty, or that level of checking. Formal verification is not a magic bullet. It won't catch all your problems, because there are still specifications involved. But it does give certainty about certain properties of the program. Sometimes the bugs people exploit are extremely stupid still, and they could have been easily caught by formal verification.

Auto-Formalization: Can AI Write the Specs Itself?

Sajjad: That brings us to another interesting question. You hypothesized, quite a while ago, that AI would start generating proofs the way mathematicians perform them. I saw a famous exchange you had with Terence Tao about this. Given that AI has accomplished that goal — we can actually rely on AI to generate formal proofs — what about writing the specs itself? Will you still need humans to write the specs, or can AI get to writing specs as well?

Christian: Yes — actually, by the way, this auto-formalization idea, I wrote it up in 2019. This vision statement was basically a paper, published at CICM. I always proposed there's a kind of iterative process between auto-formalization and verification — one of the ways to train extremely strong reasoning systems is by letting the AI first formalize things, so you create the formal problems, and then check the solutions formally. That way you bootstrap higher and higher levels of intelligence.

It turned out I was mistaken to some extent in that belief, because we've reached an extremely high level of reasoning without having to resort to formal verification. We don't really know everything OpenAI has been doing to get to these results, but according to my information, they don't really use any form of verification during training. They could bootstrap their reasoning to this extremely high level with just informal checkers of correctness. That's an interesting measurement point.

On the other hand, it still shows us that the specification can be generated with very high certainty. So it's an interesting measurement, and I was a bit too pessimistic about the strength of informally-verified output. I think I have to revise some of my opinions. But I think it's good news for formal verification still, because it says we can probably get the specification right mostly with AI tools — we can't completely rely on them, but we definitely can get to a very high standard just by that.

One of the main reasons formal verification didn't catch up is that it's just too expensive to create the specification. Very few people have experience doing so, and it requires a lot of training. That cost is prohibitive — the verification cost itself is negligible compared to creating the specification. That's a human cost, and it's huge.

Sajjad's Tribute: Inception, Batch Normalization, and Adversarial Examples

Sajjad: You had quite a journey, Christian. As we were preparing for this discussion, we were looking at your profile, and you've had such a huge impact on the field. I looked at the Inception paper — even at that point in time when GoogLeNet came out, I was quite intrigued by such a large, complex network. I was wondering how someone designed a network like this — I was used to much simpler deep neural networks, just replicated layers, but this was a unique architecture.

Then after that, you came up with batch normalization, and that's had such a humongous impact on the industry. And then, all of a sudden, we saw you pivoting and talking about formal methods, verification methods. That paper you wrote — misclassifying a school bus as an ostrich — left an indelible mark on me. That's when I started looking at it and thinking: if this is true, there have to be other methods to augment neural networks. So thanks a lot — you really opened my eyes going through this. I realized the amount of work you've done in this space, and I wanted to introduce you to our audience to highlight the impact you've had on this field.

Christian: Yeah, thanks a lot.

What Does Formal Verification Even Mean for an LLM's Output?

Sunil: I have one question — maybe I'm not as in-depth technical as you two. I understood formal verification on the chip side: you have RTL, you have test cases, you run it through and see the output, then do the same thing on the netlist. What does formal verification mean in the LLM world? How do you check the output of an LLM to make sure it's actually correct? I don't understand that at all.

Christian: I should ask you, because you're working on that. I also don't fully understand it — this is a current research topic, and I think it's an area that will grow significantly in the next few years. Sunil, you're being very modest, and so is Sajjad — you're doing the trailblazing work on making this practical.

Sunil: It's still way behind my level of comprehension, to be honest.

Christian: Generally, I think it's not really one thing — there are multiple domains, and each requires different kinds of verification. Chip design, for instance, has formal verification, but the overall verification workflow is much more than that — you check design rules, you do very sophisticated timing analysis, and so on. All of those are actually verifying what the design does. Doing a SPICE signal-integrity analysis is extremely different from doing formal verification — completely different domains, but you need all of them.

With AI, verifying AI output will be even more heterogeneous than chip design. I left chip design sixteen years ago, but when I left, more money was being spent on verification than on actually designing the chips. I don't know if that's still true, but it's probably still a large amount. In the LLM world, or the AI world broadly, we don't even consider verification that much — and I think that's not responsible. You could even call it reckless.

I think this will change, first of all, because a lot of things that were completely impossible a year ago, or even half a year ago, are becoming possible today. As you mentioned, that exchange with Terence Tao — I tweeted that two years ago. People consider Terence Tao one of the best mathematicians, no contest, and the mathematical community treated him as someone knowledgeable about AI. But I talked to him and was shocked that he had zero clue where things were heading. Even three or four months before that, he was more or less in denial — saying AI does this "like a slightly worse student." I thought that was completely ridiculous, when you go, in one year, from an elementary school student to a high school student, and the next year to a mediocre university student — you can connect the dots and see where it's heading. And people, even Terence, didn't connect the dots.

I tweeted that I was shocked he didn't see this wave coming, about two years ago, and people were telling me, "who are you to criticize Terence Tao?" I didn't care. I told them: look at where things will be by June 2026. I was roughly a month off — things really started getting crazy in July and August, and it's gotten crazier since. We have capabilities today that were unimaginable even half a year ago to most people — not to me, because I could connect the dots. Ray Kurzweil saw it coming thirty years ago. But now we can see how fast capabilities are rising — and that means not just capabilities for protection and advancement, but also on the negative side: breaking things, making things unsecure.

So now we can do a lot of verification — we can have agents that create verification tools very quickly, work that would have taken humans decades. For a lot of purposes, we have to create those verification workflows and pipelines so we don't just take AI output as granted.

"Towards Guaranteed Safe AI": Which Leg of the Triad Breaks First?

Sam Pooni: I had a question for you — you co-authored "Towards Guaranteed Safe AI" with Bengio, Russell, and Tegmark. Three parts, right? A world model, a safety specification, and a verifier that produces a proof certificate. ClaimGuard is roughly that same triad, with an ontology as the world model. Which of the three breaks first outside of mathematics? Is it the one we'd think?

Christian: Could you repeat the last part? I didn't quite get it.

Sam: ClaimGuard is roughly that triad, with an ontology as the world model. Which of the three — world model, safety specification, verifier — breaks first, actually, outside of pure mathematics?

Sajjad: When you apply these techniques to the real world — insurance document processing, legal document processing — what would break first? Is it the verifier, or is it the specification? Is it harder to specify legal clauses, or harder to verify them?

Christian: To be honest, I have no idea — this is very hard for me to tell. It might even be dependent on the actual application domain. These are all pure speculation, but if you have a super fuzzy area — say you want AI to write a novel — I think formal verification probably isn't the most important part there; it's more like a grammar check. That's not the hard part. But in mathematics, it could be that you produce a slightly wrong argument, and it's over. So I can imagine these are all critical in different ways at different points, with different levels of criticality in checking.

By the way, in the discussion section of that paper, I was in disagreement with Yoshua Bengio — he was insisting he wants to formally verify the whole AI pipeline, training and everything. I was telling him I don't really see a way of that ever happening. I've always believed the more pragmatic path is checking the output of the AI alone, and maybe using that for training iteratively. I don't really believe in formally verifying AI models — that's a very, very hard thing to do, and we're just not there yet. Maybe with AI we'll be there in ten years, but AI accelerates everything so fast that ten years will feel like a thousand years. I have no idea when that could happen — it looks about as hard to predict as quantum computing. I don't think it'll happen in the next ten years either. I'd say verifying the outputs — that already gets you a very long way, and that's what we should be focused on in the next few years.

Batch Norm vs. Layer Norm: A Personal Note

Sam: On a personal note — batch norm lost to layer norm in transformers. Do you take that personally, actually?

Christian: I was surprised, because people asked me, when they wrote the layer norm paper, whether that was a good idea. I thought it might work, but I didn't really know — I thought it was fundamentally weaker than batch norm. I never take things personally, or I try hard not to, especially around measurements in AI. If you don't learn very early in machine learning that you should never attach your ego to a result — one should be extremely paranoid about one's own opinion, all the time. Even in chip design, you learn that if you take your ego too seriously, that's already a problem. Chip design may be even worse, because one single mistake can go straight through the whole line, and then it's over. You have to be extremely paranoid about your own thinking — the default assumption should be that your own thinking is wrong. That makes certain things easier in life, and other things much harder — if you want to start a company and fundraise, that attitude can be a disadvantage, because you're always very self-critical. But if you have to engineer a system that's reliable, or that at least works, you'd better take that stance.

Is Formal Math Really Recursive Self-Improvement?

Sam: The one thing that excites me — whenever I think about formal math, it's the first domain I was exposed to with real recursive self-improvement. Your whole notion of a math AI and AGI lab — that doesn't call itself one. Is that the case, actually? Formal math is a domain with real recursive self-improvement, right?

Christian: I don't know — why would that be self-improvement? I don't get it.

Sam: Because you keep refining, right? Over time, until — say, when a model grades its own homework perfectly. Formal math, when used, is the one domain where a model can grade its own work.

Christian: I see — you can call it that, but I don't think it typically is. That's not recursive self-improvement. I think what people typically refer to as self-improvement today is when AI is used to improve AI at a fundamental level. If you just say you have a way of bootstrapping some data, like AlphaZero, you wouldn't call that self-improvement — you'd call it more like self-taught learning, long-term learning, something like that. I wouldn't mix that with recursive self-improvement — that's when the capabilities you got in your model help you create a much better model. For example, if your AI model runs AI experiments, that's what I'd call self-improvement.

Mathematics could be used for self-improvement, for sure — you can mathematically capture almost everything, so you can capture AI mathematically, and that could be used for self-improvement. I believe that will be the case, or at least I hope so. Mathematics and formal verification could lead to a much safer and more efficient form of self-improvement than something more heuristic in nature. Both are possible, but with math and formal verification, it could be both safer and more efficient.

Sam: A lot of people have told me they could do that refinement as a weekend job, and by Monday have a more refined view. That's why I asked.

Christian: I can believe that — that's roughly right. You can do refinements and bootstrap processes, and self-taught learning is also a real notion, but I wouldn't call that self-improvement. Self-taught isn't the same as self-improvement. The strong self-improvement people are chasing is more like doing AI research with AI — that's the whole idea.

Lightning Round: Lean or Natural Language by 2035?

Sunil: Sajjad, we only have a couple more minutes — anything you'd want to ask?

Sajjad: We had a couple of lightning questions. One: Lean, or natural language — what will mathematicians use in the year 2035?

Christian: I think it'll be natural language, but in the background, everything will be checked by Lean, and if you need something, you can export it. That's been my stance for ten years.

The One Open Problem AI Needs to Solve First

Sajjad: And then: one open problem you hope AI will solve quickly.

Christian: Open problem where — mathematically, or generally?

Sajjad: Generally. Right now we're challenged by the ability to use AI broadly on account of reliability. What would AI need to solve first?

Christian: That's a hard question to pin down. I don't really know — AI is already solving a lot of problems all the time. I think interpretability and safety. We're running more and more AI agents everywhere, but you can't give much guarantee about their behavior. If you think about it, say you run thousands of AI agents, or even a million, and they do whatever they do — some of them do the wrong thing, maybe not something slightly wrong, but something like infiltrating data — and you're completely on the hook, because they did something you're responsible for. How do we make a world work where, if just a small percentage of agents do the wrong thing, they don't cause huge harm? I think that's the main question — how do we create an era where you can actually use these agents safely. We don't really know yet. I think verification ideas can help. Whether they solve everything, I don't know — I doubt they solve it on the whole.

The Frontier of Explainability: The "Something Else" Problem

Sajjad: What about on the explainability front? What are you seeing as frontier research in explaining what an LLM actually did?

Christian: There is some research, but I think it's lagging a lot, because it doesn't really make money. The real problem is that even when people — auditors, governments — want certain legal guarantees of correct behavior, especially for safety-critical applications like cars, airplanes, or military systems, that doesn't cover what else happens. Your AI system could do exactly the right thing you asked for, and at the same time do something else as well. How do you specify that it shouldn't do something else, when you don't even know what that something else is? That's really the hard part, in my opinion.

Wrap-Up

Sunil: Okay, we've run out of time. Thank you so much, Christian, for joining us — I personally enjoyed the conversation a lot, it was really interesting for me. Thank you.

Christian: Me too.

Sunil: If you could just hang on for a moment, let me stop recording, and you guys can continue.