Why AI Needs Formal Verification - Alex Skidanov + Christian Szegedy

Captions as YouTube publishes them, usually machine-generated, so product and people names can be misheard.

1. 0:09

   Um, I'm Mali. I'm a writer at Near. Uh, many of you in the room know Alex Gdanov as one of the co-founders of Near. Um, and we're honored to welcome Christian Seedy, who is a legend in the field of formal verification. Um, raise your hand if you know what formal verification is.

2. 0:29

   Okay. So, let's start there. Alex, could you tell us what is formal verification? Sure. Um, so I think the easiest way to think of formal verification is if you have a mathematical theorem, right? So, people have been proving math uh for I guess as long as they've been intelligent. Uh, if you think of a proof, the proof would be imagine you're reading a paper that has a proof of a mathematical theorem. You read it step by step. uh it's uh it's very hard to

3. 0:58

   carry out every step and understand that not none of the steps have mistakes and as a matter of fact there were quite a few theorems in the history uh that did have subtle mistakes that are very hard to catch and formal verification allows you to convert a theorem into uh formally verifiable statements written in a uh some computer language that can be verified by a system and then you know that for as long as the theorem

4. 1:22

   itself is properly stated uh the proved given is definitely proving that the theorem is correct. Right? And I think a very good um sentiment towards the power of foreign verification is a recent blog post by Terrence Ta famous mathematician where he compares uh the past where if he's working on a very complex proof he would be at the very best working with three or four other mathematicians whom he definitely knows will not mess it up.

5. 1:51

   While today with formal verification he can be working with a very large team and as long as they're exchanging those files with the formal proofs they know that every step along the way is correct and you can accept proofs from from anyone from anyone in the world.

6. 2:04

   Christian do you have anything to add to that? Do you have anything to add to that definition? Yeah. So basically format verification is about making verification of CRM algorithmic so that programs can check whether your proof is correct. So it can apply to a hardware system, a software system, a protocol.

7. 2:25

   Um, and Christian, you've been in this field for a long time. Um, can you tell us about kind of the trajectory through the field and how um, how the research has changed uh, since you got started in it? Yeah. So format verification has been used for highly security critical applications like military grade applications in operating system etc for like 20 30 years now but it's super

8. 2:55

   expensive. So people cannot easily do verification at a large scale because it was it involved a lot of human effort by very high level experts and now I think with AI this is changing dramatically. In the past year the effort level of verifying some complicated mathematical statement went down like at least 100x.

9. 3:20

   So we need 100 times less human interventions to verify or create a computer verified proof of a complicated mathematical statement than it was a year ago. And this is all thanks to AI. Um yeah, so basically it's it's getting potentially more ubiquitous it become as it becomes cheaper um or easier to uh formally verify more kinds of systems.

10. 3:48

    Um, is that right? It could. I mean, we'll see. It has to prove its worth. Um, Alex, you've been working on formal verification recently. Can you tell us a bit about uh the use case you're focused on or what problem you're trying to solve?

11. 4:04

    Yeah, so it's it's worth saying that comparing to to Christian here, I I've been working for very very little time. Uh the first time we met with Christian was uh Ilia and I we met I think at least seven years ago and you guys already had a lab at Google right working on I think it was 2017 so it's nine years ago yes yeah so uh yes but since recently I've been working very actively on uh applying formal verification to uh to formally verifying smart contracts uh because

12. 4:33

    so smart contracts are code and code is law but code has bugs right and if your if your code has a bug that allows anyone to drain the whole smart contract. uh then uh you know it's not a very u valuable smart contract and for verification allows to change it uh in a way that if you can properly state uh the statement of uh of the fact that the you know the contract cannot be drained

13. 4:57

    then you can prove it and if you can prove it uh and you can and you can assert that the contract deployed is in fact the the code that is uh that was proven then you know that if you deposit money into the contract under no circumstances can that money be taken away from you. So, so that sort of allows you to to actually have that promise of the blockchain that we had from the very early on that uh you know you actually can have code that is law.

14. 5:21

    Uh obviously it comes with a lot of caveats such as you actually do need to state the statement properly. The statement itself could not be saying what you think it's saying and then even though it's formally proven, you still lose your money. uh and you do need a lot of infrastructure around it that that that proves to you that the co that the code you're interacting with is in fact the the code that was proven uh etc. But it's a until recently I think that was practically unfeasible to prove

15. 5:47

    uh very complex statement about the code and and now it's becoming very real. So it's a very exciting time. [snorts] So maybe we'll see formal verification on mirror soon. Yeah, hopefully. Cool. or let's say certainly. Um so the theme of this week is AI. So I want to talk about um basically what does formal verification have to do with AI? Christian, you hinted at it, but um what's changed recently that um that brings formal verification to the world of LLMs.

16. 6:19

    So, so yeah, I mean I think one of the biggest bottlenecks in AI generated code today is the fact that we don't really know whether the code was correct or not. So a lot of people spend like sometimes more time at figuring out how to verify their code, how to how to make sure that the computer generated code is correct than than actually writing that code would be. So that's very annoying and I think

17. 6:52

    format verification can help a lot there because we could start with format specifications that are easier to understand and then the AI could also be directed to give uh very uh guarantees of correctness of the generated code. So that will completely change the way that this AI uh generated code uh is assessed. we can we we only need to assess the correctness of the specification basically the code that describes what we want from the software

18. 7:24

    rather than uh having to assess the actual code and then I mean AI itself is also code so it would apply to AI itself a bit but I think AI is much harder to verify because AI is uh very statistical in nature so even humans have a hard time of debugging models and we don't know how to do that at all.

19. 7:49

    So basically formal verification can help um you know verify AI systems but also it could potentially help in the process of verifying AI systems more efficiently. So, so yeah, I think what is realistic in the short run or medium run within a year or two is that we can verify the produced artifacts, but much much harder is it to verify that the AI system itself is correct?

20. 8:17

    Yeah. So, what what specific properties um are realistic to verify in an AI system? Like I imagine it provides different challenges than a hardware system, for example. Yeah, I mean people try to verify various aspects of like robustness to certain adversarial examples etc. But generally I think also also it's it's possible to verify that the inference that the technical stack of the AI is

21. 8:45

    correct like it really infers the right uh the right model that for example if you do quantification then it stays within a certain bound. A lot of these can be verified but whether your AI system actually uh does any harm to human or does it really like semantically doing the right thing I think that's very I don't have any idea how to verify that and um I mean if if we can imagine applying formal verification to more kinds of

22. 9:18

    systems then like even beyond AI um what about the whole internet like we see evidence that AI is getting better at identifying bugs in code and potentially exploiting them. And you know, we know that both human written code and um AI generated code has some certain number of bugs per line. And if AI can get better at finding that then do we see a bigger security risk for all code everywhere and can formal verification

23. 9:49

    maybe help? So basically uh verification is also an attack mechanism. So when you try verifying something you can get like either an guarantee that that you don't have certain kind of bugs or you can get an output where the AI system basically the verifier agent tells here is a way to circumvent here is a way to create an input so that it highlights some bug so that your behavior expected behavior is not met. So basically verification is

24. 10:24

    not just about f uh like making your software very bug free. It also it will also highlight a lot of the existing bugs in existing software. Mhm. So if you don't use verification to uh to prove the correctness of your software then somebody else will try and and might find vulnerabilities in it and most likely they will. Mhm.

25. 10:46

    So, so there's also interesting uh point I was just discussing with a friend of mine while waiting for this panel that uh generally uh foreign verification has been around for a while and one of the reasons why um you know like there are several companies that work in the field and one of the reasons there's no you know um takeoff for them is that when you go to actual companies that have code that has you know that is deployed

26. 11:10

    in critical systems and obviously the closest to me would be blockchain you know if you have a smart contract which is operating on billions of dollars. Uh a lot of uh those companies or people they do not understand the value behind for verification because the code is already audited. The code might already even go through some level of forification but uh the statements would be like let's say at the function level you know they will say you know total supply will not change after a

27. 11:34

    particular function. Uh and uh at a higher level there's skepticism uh in the sense that because models get better and better they also get better and better at reviewing code. Right? So maybe we don't need for verification. Maybe we're going to get so good at auditing code and so good at producing code on the first pass which doesn't have bugs that we're not even going to need it. Uh and I think the argument to

28. 11:55

    that would be that uh in a sufficiently complex system I think the bugs are always going to have chance of being caught. Uh and an interesting way to think about it is that you know if you have a model of generation X which is producing very high quality code but could still have some bugs completely uncatchable by model of generation X, model of generation X plus2 will still be able to to find them, right? Right.

29. 12:14

    And so until we formally verify it's going to be uh that sort of cat and mouse um thing. So for verification eventually we will have to formally verify everything. The question is how soon we will be able to to do that. Yeah. So is that like a a corporate security issue, a customer fund security issue, a national security issue? Like what will what do you think could be the the chat GBT moment for formal verification? What will make it feel urgent or worth investing in?

30. 12:44

    So, so I think if you use a Christian's example that sometimes uh you know when you try to formally verify a statement the agent can either formally verify it fail to verify it or it can actually find you a reason why it is not formally verifiable like it will say hey I cannot prove you the statement is like like I cannot prove for you that the money cannot be drained because here is the way to drain them and therefore the statement is wrong right and then you immediately see that there is a bug

31. 13:07

    right and so yeah I think the like a pretty good moment will be if they if if actually someone gets to system which is extremely capable at doing that then you can just go through all the deployed contracts today and just find those issues right and then that would be a hopefully it's going to be someone with values who will you know show it to the to the corresponding uh teams and fix it but that will be I think the moment when everybody will realize or like it could be a moment when everybody realizes the

32. 13:33

    importance of uh and it doesn't have to be blockchain right it could be you know hey guys here's a here's a sort of uh critical zero day vulnerabilities in Linux kernels kernel that were patched after we found them, but you know, they were found by a formal verification system. [snorts] What do you think, Christian? What might be the the adoption moment for formal verification? You said we might only be a couple years away.

33. 13:59

    So, so about the adoption model. Yeah. Like when what could um what could make formal verification catch on as a more universal? Yeah, I think I mean it's easier to bootstrap format verification for mathematics first in my opinion, but once we once that is done I uh I think it could be applied to software and another for engineering sciences. So basically now we also have kind of verification when you build build a new building then you don't do it without quantifiable evidence that

34. 14:37

    that building will not collapse that was not always that way I mean several hundred years ago people just build buildings and they hoped for the best and now that same thing we are doing with software and I think with format verification you will have be able to measure more and more of these constraints So for example uh like the type systems in C++ or Rust they they give some guarantees of certain behaviors. So they are already a very low level of formal verification

35. 15:09

    uh when you have a typed language and format verification is just that the typing is so strong that you basically can make any possible statement about anything and then and there are a lot of uh uh shades between them and I think we will get more and more uh verifying like uh uh protocols blockchain protocols as well. So whenever money is on the line I think people will have to verify it at some point and also when you have like exposed to the internet uh and you are

36. 15:42

    somewhat critical you will at some point you will have to verify at least your interfaces and then this will go deeper and deeper in my opinion. So probably it will be adapted at the most critical places first. So you mentioned math uh given that almost nobody here raised their hand uh when when we asked them if they know what for verification is can can you give people a short overview of what is the state of foreign verification in math how how far have we gotten in the past you know in the

37. 16:10

    yeah so it's kind of so it was like two years ago it so five years ago nobody tried to verify too much there were very few like a few dozen people at in the whole world who who were working on verifying mathem mathematical statements formally and it was very hard and to do the simplest ones and then they started to gain a bit of traction and now with AI last year it suddenly started to get faster and faster. So it's basically now a lot of people come to me and ask can I work

38. 16:42

    with on formally verifying math because it's such an obvious idea and I said yeah it's it's obvious now I mean when I started to work on it like 10 years ago it was far from obvious but now it's it's becoming mainstream and I think this year we will get to the point that there will be much much more AI generated formalized mathematics than human formalized mathematics and we will have

39. 17:07

    a significant fraction of all of mathematics formalized this year. Yeah. W Alex, you mentioned Terau earlier. I think he gave an interview recently where he said that um AI and formal verification together could also help um groups of mathematicians tackle more complex problems in a more decentralized way. Do you want to talk about that? I think that's Yeah. So, so he was giving examples uh and it's all it's all it's all googable.

40. 17:35

    So I I encourage people just to find the original uh of the statement but he was giving examples of people just going to chat GPT and Chad GPT is very good at giving you an informal proofs. Uh it's getting better and better at just proving statements. uh I I don't know if it if it can prove anything at the frontier but uh for many uh for for for many things that are very advanced for um

41. 17:59

    chat GPT can already prove them but an informal proof again can have a bug right and so then there are tools uh there are several there are several tools already on the market which are open to open to be used by everybody where you can just feed a proof written by chpt and it will do its best to formalize in lean and if it doesn't formalize it doesn't mean it's wrong but if it does formalize you know it is correct Correct. And so you can iterate and you can eventually arrive at a proof

42. 18:23

    that uh that is correct. And before it would have taken a lot of time and now people can just iterate and uh I I think another very interesting example he was giving is that before if you started already going on some path and you made some progress uh the cost of you of abandoning that path and going another way was very expensive. But now that the whole proof is given to you by ch GPT, you can you can easily change the very first assumption you made and completely you do the whole proof and it's the cost

43. 18:48

    for you is just waiting for another generation uh from the model. So it's it's definitely increasing the agility of people to play. So I I might add that so formalization is not really like asking GPD for a format proof and it gives me a format proof. So formalization is is seems something like write me a Unix kernel or something. So it it basically the problem that language models out ofbox cannot handle is that you actually have to devise a whole code base and that's

44. 19:18

    that's a lot of work. So typically you don't let GPT spit out the whole code base. It will do it agentically if you set it up in the right way and that's the that's the thing that is also necessary for formal verification. Right. So, so effectively the Yeah. So, so going from the natural language statement of the problem to the formalization of the problem is very hard, right? But then going from the natural language explanation of the solution to the problem to the formalization of the solution that is fully automated by by things like Gaus and harmonic and uh whatnot, right?

45. 19:51

    I mean, it's it's still a hard programming problem. So, it's as hard as if you have a very detailed description of your software. you still have to go there and write the software and test it thoroughly. The same thing with formalization.

46. 20:04

    Yeah. Yeah. Or rather like when when they do succeed then we know it's correct, right? Yeah. But it's not like it spits out the proof for a form proof. It's more like it has to write this whole code base of for example a a typical like large CRM. It takes like 4,000 40,000 lines of lean code which is basically code and that's the proof. Yeah.

47. 20:28

    Cool. Um, unfortunately we're out of time. Feels like we just scratched the surface, but thank you both very much and thank you all for joining us. Watch for some interesting work from Christian and Alex in the next few months.

48. 20:40

    One one last comment, guys. If you if you like what you hear, Google Lynn, find any lean playground, LIN courses, and just familiarize yourself. That's going to be that's going to be the future. Lean is the future. All right. Thank you. Thank you.