How Formal Verification Stops AI Reward Hacking | Theorem

MTS (0:01)

Hello, everyone, and welcome back to MTS. Today, I am joined here in person with Jason Gross and Rajashri Agarwal. They are the co-founders of Theorem, and Theorem is an AI and programming languages research company working on formal verification, using mathematical proofs to check that software actually behaves the way that it's supposed to. So today, we'll talk a little bit about if this is a scalable way to make AI-generated software safer from proving that agent sandboxes are actually secure to verifying increasingly complex code as models get more capable. So welcome to MTS.

Jason Gross (0:37)

Thank you.

Rajashri Agarwal (0:38)

Thank you for having us.

MTS (0:39)

Thank you for joining. Let's talk a little bit about what Theorem is, what you guys are doing, and what exactly formal verification is, because we use this term a lot as an industry, and I guarantee that a lot of people who are even tweeting about it or talking about it on Twitter discourse aren't totally sure what it means. So maybe we can start with you, the non-CTO that says he's a CTO. Let me get your perspective.

Rajashri Agarwal (1:02)

All right. So I'll explain formal verification.

You can ask any question about a program, and there's a way to rigorously answer it, because a program is just transformation of some inputs into outputs. So if I can tell you whether any question that you have about this program holds for all inputs, that will be a proofy answer.

It's checked by this thing called a proof assistant, which means that there's this piece of technology where you can do this type of reasoning very precisely. Unfortunately, most people don't write code in a proof assistant like Lean or Rock. They write code in whatever language makes sense for the computation that they're doing. And so the goal is to shove a normal program into a proof assistant, and then phrase your question like you would, and then in this proof assistant to write the proof, which is this full, rigorous reasoning of how all these inputs are transformed. So that's what formal verification is. And once you've established this answer with a proof, that means that you have checked it in some efficient way for all inputs. So that means this answer doesn't change unless the code changes.

MTS (2:07)

And right now, so many of the languages that people are using, they're not writing in Lean. They're not writing with formally formal verification types of languages, which makes it really hard. And formal verification is increasing as a use case, as a problem that most people want within how they're actually creating code today. So I would love to get a little bit of your perspective, Jason. What maybe is the origin story behind Theorem? How did you guys identify that this is something you wanted, that needed more research to be done?

Jason Gross (2:36)

Yeah, I've been... I've sort of had a personal vendetta against bugs since I was very young.

MTS (2:44)

Personal vendetta, I see.

Jason Gross (2:46)

They've always irked me. And before... So I did my PhD doing formal verification. And one of the things that I learned there is that it is very hard to scale, in that if you want to verify software, you should expect to need to write somewhere between 10 times and 100 times as many lines of proof as you have lines of code. And because this needs to be written by an army of PhD engineers, which are more rare than your standard software engineers, this would grind any sort of production to a halt. And so it only makes sense to do for the most critical of systems, things like secure web browsers, like secure internet security type things.

And after that, Raj and I were running a small research lab. One of the things we were looking into was how do we verify the models themselves? I had this dream that was like you can prove something about the model's output, you can study the proof and learn, you're like, I don't know what it means to say that the model is doing good stuff. But maybe if you have some proxy of it, that's just like the, if the model looks at its own output and says this is good, and then you get a short proof that it only does good stuff, you learn something about what the model thinks is good.

And the thing that I learned from doing this project is that this also doesn't scale and is not going to get us to where we need to be with regard to AI hacking, with regard to the various threat models for AI. And so we pivoted into having AI verify the software that it generates.