NEAR AI Office hours #24 w Alexander Hicks from Ethereum Foundation

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

1. 0:05

   near one we close to won't stop us now together we me Define the game when near we'll find the flame empowered Minds rise and S use your own AI we explore hold the future hand in hands in this Tech okay hello everyone welcome to the next episode of near office hours today we have uh Alex Hicks from etherum foundation and it's going to be a very exciting topic about formal verification Alex you want to say a couple of words

2. 0:55

   about yourself and the formal verification efforts at ethereum uh yeah abut thanks for having me on and what a great introduction song I'd never heard it before um so so yes a bit about myself um I joined this foundation in June this year so I've only been here for a couple months uh and my job description there is essentially to try and find ways to use form verification and AI to make it more secure um and so one thing that

3. 1:25

   we're particularly interested in at the moment is trying to formally verify these big general purpose risk five uh zero knowledge virtual machines so we have a big project um that we've launched with a kind of big $20 million budget over two years uh there'll be a lot of Grants and a lot of bounties associated with this and a lot of work that will get done and and hopefully some some good results so that at the end uh we can you know people can use these and be sure that they're not going to I know lose all their money um

4. 1:57

   amongst other things and and part of that in in the AI angle there as well is whether we can figure out the ways to use um AI in the same way that you know AI has become very useful for programming in mainstream programming language like python rust C++ and and if we could get you know AI tooling to be as effective for maybe not proof generation in terms of formal proofs but maybe for

5. 2:22

   maintenance and maybe Auto formalizing uh specifications out of codes and and comments and markdown files and and things like this uh so that's something that's very much on on my radar as far as trying to apply AI um and another angle which is the the angle that I already had in mind um before joining J foundation and and that I was thinking about a lot was around kind of formation

6. 2:47

   for AI because all these models we have now are really complex and you can kind of prompt them for whatever you want and you'll always get some kind of answer um trying to figure out whether the answer that you're getting is kind of correct in any sense or consistent with any kind of logic is is something that's also a big interest of mine um because if we're going to have you know maybe kind of

7. 3:10

   user owned AIS uh as would would put it in one of his talks uh then it seems to make sense that you'd like some assurance that what you're getting out of the AI is actually kind of aligned in any sense with with what you actually want to get out of it yeah yeah it's very exciting and uh to give some background on our end uh out of uh I think 12 people today in at neari three people are very big uh very into formal verification we we you of

8. 3:42

   and discuss it I quite frequently do some uh some drills but we don't we don't we don't use it actively yet I think we uh the focus of uh Biga projects right now uh is on uh on other things however we might have some announcements that reducted uh we will see but I personally I personally spend a lot of time with formal verification and I run I run this project where I annotate a lot of data and I'm working on

9. 4:12

   annotating uh I'm about to launch a project to annotate some formal verification data so this is something you mentioned how how do we how do we make models better at formal verification so I'm I'm I'm about to launch some experiments in that area and I guess one the first question I have which is uh around zkm so so I I looked at the website there's a website it's verified dzk m.org where where

10. 4:38

    people can more detail uh something that is not at least I didn't quite understand is whether the goal is to prove the implementation of the vkm or if the proof is to build the construction itself of the zero knowledge uh Machinery if the yeah yeah so it should really be both um hopefully it should be both and and I think we've got kind of we've set oursel a kind of twoyear timeline to do this and I think we should be able to get

11. 5:12

    both because one thing that's missing at the moment is that you have the KMS that exist that are now coming into production and people are going to run you know maybe rollups on these and and a lot of other applications um so we want to make sure that they're nice and secure and they're built on top of you know risk 5 is at this point a fairly well inded ISO and it's fairly stable um

12. 5:34

    if you're running a rollup on this for assume you've got the evm you know maybe you know you could run some new applications on it as well and things like this and for the evm that's not super stable you get new codes in everything then then but we have like some formal specifications and then there's all of the cryptography so the you OB start with the actual circuits and rization and then you have the the prover and the verifier that's on chain and for these we also have specifications but they're

13. 6:01

    really you know a mix of papers and a mix of code which are both quite informal from the point of view of form verification and so something that we actually need to figure out to be able to verify that the implementations are actually correct is first actually have kind of formal specifications for the entire stack um which is which is something that especially for the kind of cryptography we don't really have yet it's something that we're starting to to

14. 6:26

    work on and in maybe even kind of early 2025 we have some early results on that on trying to formally specify some of the polinomial commitment schemes and some of the polinomial iops um so that then we can actually look at the code and verify the code against these specs in the same way that we're going to verify um maybe RM against some of the existing evm formal specifications in in K or lean and and in the same way that we have existing semantics for risk five

15. 6:57

    and so we can you know look at a RIS five C KVM and check that you know the CPU that the VM is supposed to be is actually a risk five CPU and and not you know something else entirely in which case who knows what's going on there um so so so yeah we we do definitely want to look at the actual implementations make sure that the implementations are correct but for that we need obviously

16. 7:20

    to have all the specifications in place to to be sure that what we're checking is the right thing right and my understanding is that not only you need the specification you need need you need that specification to be um converted into something would understand right so so like like I I assume risk risk five I I I'm not very familiar with risk five but I understand was them very well I

17. 7:43

    assume they like at least on a very high level uh like similar right to an extent and if I'm thinking of proving that a particular implementation is correct against wasm right that means that I need to like within Lan somewhere I need to affect ly implement the whole wasm transpiler or rather virtual machine so that L understands what particular wasm code would be would be doing right yeah yeah so you need you need to have those semantics in place and the nice thing with this five there is that there are

18. 8:16

    actually official semantics that the maintained bodyb RIS five project and these are written in a language in a specification language called sale um which is developed by a bunch of people in kind of primarily Cambridge um and from sale you can get extractions into um SE improvers like Hall Isabel and as part of this project we're also getting an extraction to lean and so once we have those semantics that we can get into all of the improvs that we'd like then actually what you can do is you can take um a specification of

19. 8:49

    anization you know let's say air if you want to to have a stock based ekm like many of them are and you can show that the terization you have it will be a an encoding that preserves the semantics of the virtual machine and and from that you obviously get a sense that whenever you're trying to prove some execution trace of that virtual machine um the schematics are correctly encoded and therefore what you're proving is actually what you think that you're proving uh which is which is quite important if you if you want to avoid

20. 9:21

    having uh either kind of proofs of programs that don't make sense uh whether that's try to prove the execution of programs that haven't actually been executed or or whether you do actually execute something and you're not actually able to prove that you've done so um both of these would obviously be very problematic yeah yeah that's sound I never heard of Zale before that sounds uh very exciting I I don't know if there something like that exists for wasum today but that would

21. 9:47

    be um you would definitely be able to write wasum specification is sale I don't know if there is one but I think like wam has been pretty good at like having some more of a mathematical specification so it shouldn't be that bad um it' be worse looking into it if you're trying to formally verify a bunch of things and you're using wum then then I think it would be worth putting a bit of effort into it yeah um so

22. 10:15

    the an interesting uh thing about ZK zero knowledge in general or I will I will go in even a little backward so when we were building back back before we launched it uh we had a very good cryptographer in our team and every now and then I would be and naturally building a blockchain fair amount of cryptography and I was never an expert in it but you know I have some like Layman understanding and it was fascinating always when I would be pretty certain that something that I I think is correct I would bring it to

23. 10:48

    the to the to the cryptographer on the team and he would completely destroy it and he will you know show me W where where my construction breaks right and uh with with zero uh with ZK the problem is that the cryptography is even more complex than you know like hypothetical like you know signatures or or or like basic things we use like you know key generation BLS which are somewhat easier to understand for a person and I was always fascinated with the fact that like maybe in the whole

24. 11:21

    world you know there's like maybe low hundreds if even that many of people understand the cas efficiently well to actually reason about it right but we but we put so much trust in it uh and from this perspective obviously if there was improve you know like if it says if there was a assertion or like hypothesis saying you know under those cryptographic assumptions you know the information will not be revealed and then the proof you don't need to

25. 11:46

    understand right the beauty of Lan is that if if you understand the hypothesis and the the code compiled you know that the proof is correct right you don't need to understand it I think that would significantly increase the uh the applicability of of zero knowledge technology in general to many use cases right because today we effectively trust people uh you know who think at the level that is way beyond my comprehension for example right because

26. 12:15

    they said trust me I'm a forg that's that's a correct instruction right and and similarly implementation wise I remember there was a there was a bug in Z zcash back in the day that was found by someone right but zcash was built also so by by cure one people in the industry right so they they missed that like something wasn't zeroed out so I think those are really important yeah I think the bug in zcash

27. 12:39

    if I remember correctly like came from an actual typer in the paper with one of the superscripts like one of the superscripts to indicate like the group element there was just one typer and then it just destroyed soundness um and you have yeah you've had kind of quite a few vulnerabilities I think especially not even with the kind of proof system themselves but even with the circuit there have been quite a few examples of under constrained circuits showing up in

28. 13:03

    in test Nets and Dev Nets and for all you know maybe there are some in in main net and you only need you know one under constrained one unconstrained variable or you know one line somewhere that lets you mess with memory and suddenly you know you lose soundness for your proof system and everything breaks and because one of the really nice things that's I think going on in this industry is that we're quite good at taking you know

29. 13:29

    brand new research and deploying it into life systems um in maybe like a year or so that's quite exciting but it also means that there's very little time to actually check that things you know really work the way that they are and also once you go from papers to implementations if you look at the proof systems you know you can look at the paper for Stocks by the the starware team and you know it's a really good

30. 13:53

    paper they all really smart is you know is probably correct but then you look at the implementations and suddenly you don't have just one stock you have recursive stocks and you suddenly need to make sure of like you know does that change your assumptions um is your security parameter the same you know do you have the same amount of bits of security um for all of these proofs that

31. 14:16

    are recursive and suddenly you know now I think as of this year Alexander ker and and some of his quarters have a you know paper that came out um related to this and this is kind of a few years you know after we've already had stocks in Productions and so because there's that lag between the high level details and the protocol specifications on paper and then implementations doing some Innovation as well on their side to actually Mak things work in the real world and then the catching back up to

32. 14:47

    these to those implementation details I think form verification can play quite a useful role in figuring out where we have gaps and where we have things that we don't understand because if you're trying to formally you know prove that you know code Implement some kind of specification then you quickly realize where your understanding is lacking and where your security model might not actually you know apply to the real

33. 15:09

    world Cod that you're looking at um so there's very kind of practical aspect to this as well um and that I think that adds to the feedback between the Innovation on the research side and the Innovation on the implementation side and if you do it correctly I think to some extent it means you can possibly push performance even faster because if you are formally verifying things and you're getting you know correctors as

34. 15:33

    part of your de development cycle suddenly you can do you know the sketchiest looking um optimizations at every step but they formally verified so it's okay and that's something that I think hasn't been done in our industry sadly but it's something that for example the form verification team at AWS does really well where they will get you know 60% 100% improvements in performance on things like electronic

35. 16:03

    signatures or um access control it with in the a stack and that pays off to a very large extent because they're serving you know hundreds of billions of requests maybe per second uh with the size of death stack and their experience has actually been that once they set up the whole process of form verification as part of development they've actually been quicker with getting new code out

36. 16:27

    and better performance out um than than they were before formally verifying things because actually now they can move faster with correctness along the way built into the development process and therefore ship faster and get performance out faster and I think for us if we could get the same for all of the pr systems that we're deploying then potentially we could accelerate things you know even further than we're than we're doing now and that would be very

37. 16:52

    exciting and so let's let's for a second assume that artificial intelligence does not become good at uh at doing at helping with proofs and whatnot right so so what would be the strategy would you be trying to recruit people who already understand Lin pretty well or what would be the the approach to having this machine that keeps on you know proving the you know the new code new changes yeah so the approach now is essentially to have a big budget and to

38. 17:23

    try and get as many people involved to to do this um for two reasons one is obiously that the scale of the work is really big um one ZK VM by itself is is a really complex stack and then in practice actually we have several zkm teams that are all doing good work right we have Nexus suin with zero jolt powder and you know there'll probably be more coming up and so we actually need to kind of hopefully make it possible to verify multiple of these zvm that have different implementation details and

39. 17:55

    different optimization techniques so we want to get aot lot of people involved because of the size of the stack but also so that actually as many people as possible within our ecosystem have hands-on experience with that kind of work um if you rely on a single team or one or two teams that are you know maybe particularly good they will certainly have limited time and and that'll make maintenance impossible across kind of

40. 18:19

    multiple ZK VMS um but then yeah there's a lot of effort that goes on into try to plan for maintenance and that's something that's occupying my brain quite a lot these days um it's not always clear how to how to do this because teams want to ship really quickly they want to you know run a new circuit that's a bit more efficient and deploy it and if verifying that circuit takes a couple months and then by the time you've done that work they actually have a new circuit ready to ship the code that you're running is never the

41. 18:51

    code that's actually formally verified so for maintenance we need to figure out ways to embed for verification into the the development process and that's about building relationships with developers and you know the kind of form verification contractor teams that are that exist um and better tooling right if we can maybe start writing circuits in lean directly or some kind of lean DSO instead of riding them in whatever rust based DSO um maybe we get you know

42. 19:23

    people just write circuits that are just kind of Fairly easily provable in lean and and things are better or maybe we just you know build better tooling to extract circuits from rust or Noir or circom or you know Cairo and whatever extract these into lean and then maybe build some Automation in lean to verify these efficiently um that's something that we do we're actively working on

43. 19:46

    it's not something that has easy answers unfortunately for me um but it but it's something that we we're putting a lot of effort in it and that's part of the reason for having such a big budget is that the goal really isn't to very by you know one zvm once and then you know hope for the best in the future it's to make sure that we put everything in place so of beyond the two-year lifetime of this project there's a pass to

44. 20:10

    maintainable form verification for multiple zbm that can be sustained by the zkm teams you know themselves hopefully because they will keen on obviously having form verification done on on their stack and if we give them the tools to to do that and and show that it can be done you know efficiently in terms of time and cost then then I think we're set for a better future in that regard yeah yeah and I want to get

45. 20:36

    a couple of estimates from you uh from your experience right so so let's say like as a unit of measure let's say there's a you know like a a a piece of code that took you know let's say one week to implement so in your like like on a very like what would be a very rough estimate in terms of how much time it would take to write the assertions about it right like the things to prove

46. 21:00

    and how much time would it take uh to actually prove them um that's a good question I don't think there's a standard answer because you could write you can write code that is fairly easy to prove for example if you don't have any we optimizations one thing that often becomes a big time Sy is when you know someone might go and see a contractor to do form verification on some code base and the codebase might be implementing

47. 21:31

    what a proof system uh or maybe like just a ver you know a smart contract verifier let's say um and that's a fairly small amount of code it's not insane like an entire zvm um and it might not take that long to write but it might include a lot of optimizations and then the tricky part there is that the formication team gets given this Mark contract written in maybe y that has a lot of

48. 21:56

    optimizations and the question of Ness doesn't just become you know is the actual specification for the verifier correct it becomes are all of these optimizations not breaking the correct specifications of verifier and so it depends on what you're given right if you're given an optimized smart contract it's really hard because you have to reverse engineer essentially all of the optimizations to figure out like the

49. 22:20

    kind of Base an optimized program that should match you know the specified the specification for the verifier that would be maybe in in the paper or or in some kind of documentation um and that can be quite annoying and tedious but maybe you're given an optimized code the optimized version of the code that you know has some easily shown link with the unoptimized code and a nice

50. 22:45

    specification and then your life is much easier um so so yeah I don't think there's a a good kind of standard estimate of of how hard it is to to verify things because a lot of the times what happens is that actually the problem is not so much in the verification itself but in the varying levels of specifications that you start with and and that has a big influence on on figuring out what you're supposed to

51. 23:09

    do um and simly sometimes you start with no specification and then you have to figure out a specification do essentially manual audit of the code to to figure out what's going on and and that can you know we all know all it to take you know a lot of time um so so a lot a lot of the complexity is is not only the verification it's also in in figuring out what the Handover from developers to to form verification teams

52. 23:34

    looks like in in and how kind of the relationship exists between between these kind of two different teams that have different assumptions and different goals about the system but would it be fair to say that first if you already have a proof for a nonoptimized version it would be easier to prove the optimized version right because you can probably just like yeah uh reduce it to the nonoptimized version

53. 23:58

    right so like inative development if you know if like if proving the implementation was always one of the CI checks right then you have a lot of things uh you can tap into right you have a library of uh of like hypothesis and proof that you can take advantage of go ahead yeah it makes like if if you have like in an Ideal World you have a formal specification you have an unoptimized optim not optimized implementation of

54. 24:31

    that specification and then you show that you know that implementation matches the spec and it's easy because it's optimized and then you have an optimized implementation and you show that the unoptimized implementation you know behaves the same way as the the optimized and unoptimized implementations behave the same way and and that means you don't need to relate some weird optimized implementation to a specification that it's where it's

55. 24:55

    clearly not obvious to they're the same and and that makes your life EAS um I think it also probably helps you with automation um a lot of goals you know if you can use smt solvers and things like this you can gain a lot of time essentially just brute forcing through a bunch of assertions and that's always easier with an unoptimized implementation that like you know clearly matches the the formal spec that you're working

56. 25:21

    with so so so yeah I think a lot of work should just go into specification more than anything um if you like a good specification is very close by itself to to a formal proof in a sense once you have you know type checking and everything it's it's really close to the same thing yeah and uh so so going back to artificial intelligence right uh if we remove this assumption that artificial intelligence does not become good a couple interesting things uh that we've been doing one is uh generally

57. 25:53

    I've been thinking a lot about formal verification uh not From perspective of Z kvms also From perspective of zero knowledge but more so from perspective of generally building smart contracts because smart contracts without formal proofs do not quite leave to the promise of blockchain right if I you know like if I cannot if I'm not uh experienced enough to verify myself the implementation hypothetical you know uh compound or Unis swap I'm always Taking

58. 26:24

    Chances and I'm still trusting a centralized entity that build the code right yeah but if there's a formal proof and I can and I can only need to verify the assertions it's still possible obviously to mess up the assertions right like that that will always be there's always going to be some common factor but if I can but it's much easier to review the assertions right and then say well indeed if I put my money into this Unis swap like the product of the pool will not change Etc right so I and

59. 26:50

    from this perspective one effort I've been U quite involved is uh I I don't think lean or any of other implementation is I think they all designed so that uh good actors are are able to share proofs with each other but they don't they not necessarily designed against a bad actor that tries to build a proof that breaks it right so presumably I'm pretty certain that a bad actor would be able to Pro full them by like figuring some overflow or

60. 27:24

    something yeah so you can also if you're if you're a bad actor it's you know you can add an axum that you would like and then you know prove whatever you want based on that axum so that's you have to be careful that that you can check right like like axom and S yeah and like the red flags you can definitely check for but there was a website I will never remember the website but they had like a

61. 27:48

    list of uh ways in which uh you know like typ save languages were broken because because of implementation bugs right and in the actual usage of line is not a problem right it is very unlikely you would trigger any of those accidentally so like you know if mathematicians share proofs or if people who bu Z kvms Shir proofs they're probably not malicious hopefully not malicious if you smart contracts that's

62. 28:12

    it's a different story so so we we be like I'm working on a on a way less capable but much much simpler formal system and and I'm and I'm launching before the end of the year an effort on at near we have a annotation platform where where we annotate a lot of coding and math data and so I will be annotating a lot of formal for you know like building formal proofs for code so so that will be like a a step towards training those systems but I don't think I don't think we would be able to annotate the

63. 28:46

    sufficient amount to to to make the to make them good right so something like alpha alpha proof would be necessary uh where machine do it themselves and and the beauty of the of the formal verif ation systems is that the proofs there's an explicit reward right the proof is either correct or not and when it is correct you get the reward and the proof is the most complex part of the of the

64. 29:09

    process right so like writing the hypothesises is uh like a small percentage of the work relative to proofs right and and that's something that I I think Alpha proof is a great example of the of the fact that it's possible to use reinforcement learning yeah and I think because Alpha proof was doing something really interesting as well which was that they would obviously they would Auto formalize the you know the IMO problem statements with with a

65. 29:39

    fine Gemini model but then they had this whole reinforcement learning Loop where you would take whatever statement you were trying to prove and it would actually generate you know thousands of variations of that statement most of which is then false and that would give a lot of related training material to their model that some of it is quite simple because some of these things you

66. 30:01

    know you change you know one symbol in one symbol in the same statement and it's obviously wrong and so that's very easily solved by the model and then not only do you learn how to prove you know statements that are true but you also learn how to show the statements that are wrong or false and that probably prevents I think a lot of hallucinations and other kind of issues that you would run into with you know if you're trying

67. 30:22

    to generate kind of regular code that's not formally verified yeah yeah when you're like trite a intermediate hypothesis and that immediately says no that is not yeah that is not the case and you're you know you're not wasting a bunch of time by proving something that was based on it that that's that's pretty helpful there's also an interesting thing in there in there I don't remember where I readit but they were mentioning that

68. 30:45

    they have a process of like formalizing the statements right they begin with a with a bunch of math problems from Chinese olympiades but those are written in natural language so they have an auto formalization process that they don't go into the depths about but they mention that yeah sometimes it fails and doesn't transcribe it correctly but but it doesn't matter as long as the problem can be solved it is still a good data point yeah yeah yeah it's interesting so

69. 31:12

    I know I've I've tried using claw to Auto formalize you know some Ser statements in like cryptography papers and like and sometimes it fails in quite interesting ways where one thing I've seen happen kind of a few times now just running experiments is that you'll give it a statement of a serum that says you know there exists some unique X such that you know Y is true and it'll

70. 31:36

    usually formalize the there exist X part well but sometimes it will miss out on the unique part of there exist a unique X and you have these kind of like subtle things where if you're generating training data for a model that's basically fine but if you're trying to generate you know um proofs for an actual kind of cryptographic cryptographic system then you want to make sure that the St STS you have are the you know correct statements and not and not some you know variation because sometimes they might

71. 32:06

    be two vars of the true it's just a weaker one and and you have to be quite careful with with these things um so so yeah I remember they definitely had human oversight on on the auto formalization process which was interesting to see and I'd love to see the statistics they had on the error rate there yeah so so on our end as I mentioned we will be we will be using a lot of humans to annotate Auto formalization and and then building proofs but uh but it's not clear yet if

72. 32:37

    that amount of data will will be sufficient to to have any meaningful results that we will know in maybe like half a year when we we when we have like a reasonably big CH of data annotated and start find tuning I I'm pretty hopeful but it's uh with the with how data P view models are you never know yeah um yeah I think there's one thing that you can do that maybe be like a very interesting test case is if you

73. 33:08

    have all of these annotations you have a few languages which you know aren't lean but you have language like Daphne or Quint which was developed by the cosmos team and these are just kind of specification languages but they have some automation built in for property testing or model checking and things like this and so you you can kind of test you know your extraction from solidity code or your code or you know whatever smart contract language using to's languages to the extent that you can just prompt an llm get a translation

74. 33:40

    and then do the automated model checking and property testing in all fuzzing and see if something breaks um very quickly in that sense and and potentially feed that back into the training process and and that would be quite interesting because I think especially for Daphne you have some non AI based um extractions from Daphne to Python and from python to Daphne and so if you wanted you could start generating a lot

75. 34:06

    of Daphne code and a lot of python code and then you know do the man do the kind of non AI based translation between both but also train a model on all of these translations and poly get quite a lot of training data out of that yeah yeah that sounds that sounds like an interesting idea yeah generally any synthetic data is obviously better than human anotated because of scales yeah yeah so another interesting thing you mentioned at the very beginning uh is you know like if you swap you know like instead of finding

76. 34:37

    ways of using AI for formal verification how can we use formal verification for AI and I I never thought like you know to know that the model is doing what you think it's doing right and I never thought of formal verification from this perspective but one interesting I would like your thoughts on the idea of there is a the latest Nvidia gpus on h100s they have what is called execution environment like fact what TDX is on Intel right and we we are we are U

77. 35:10

    contemplating the idea of training a large language model inside the TD access so that you know so that you know that the model is actually the output of a particular code run on a particular data right so so that you have large language model like you know like a 500 billion parameter model for which you have a proof up to Nvidia being honest that that the model is the output of a particular code and and data right so so so I wonder if if that would if

78. 35:42

    you think that is sufficient for the for the requirements you have or or or if this is not quite there yet I think it's it's such a complicated question because I feel like a lot of the terminology around Ai and and transparency and decentralization and and see that this for AI isn't fully fleshed out yet um and so I think to some extent if you get you know you train your model inside a trusted execution environment and then you get some certainty that like you know at least there hasn't been bugs

79. 36:17

    during training that's what you kind of get out of the box but then to some extent like if the if the data that is trained on is trash or you know heavy Buy in some intentional way or something like it might still not satisfy you know your requirements you would have as a user um and and to a large extent I think like bugs during training isn't something I'm like massively concerned about if only because dual Nets are quite robust to noise so this is you

80. 36:48

    know you can if you had like a few bit flips during training because of a solar flare or something like your model probably wouldn't change that much um and so that's less of a concern for me I think a lot of a concern for me and this is purely from me as a user and not me as someone who would train models whereas you're thinking of training models it's that you know for any model that you use even if you're running it

81. 37:13

    locally or you're doing you know inference with the ZK proof that you know the output you get is from the model that you expect like it's really hard to know it's impossible to know what's actually in these models and and even you know what the system prompt is sometimes and and therefore how the model is going to behave regardless of the data that has been trained on when you set it to do a task and sometimes it's very easy to test right if you had

82. 37:39

    an AI agent and you tell your agent you know I want to order a stainless steel pan from Amazon then you know you can check what comes in the mail three days later and you can check it's a stainless steel pan and not a cast IR pan or or nonstick pan or something else um but if you was saying like you know hey you know give me some explanation of this event then it's really hard to check that that explanation is correct and and maybe there's you know there's not even kind of a nice sense of ground Truth for

83. 38:10

    it what you'd really like to check is whether you know there's some kind of bias in the model that like isn't breaking isn't you know kind of breaking rules of common sense or you know your own rules of Common Sense maybe that you would Define for yourself and and things like this and and I think that's where a lot of what I'd like to check with respect to models and and my use of them

84. 38:32

    is is to figure out whether I can Define like some basic common sense and check that the model follows that basic common sense to to some extent um and and I think that's really tricky right it's kind of like defining a really good system prompt and and making sure that the model actually follows the system prompt and maybe didn't you know jailbreak itself or something like this um so it's a really

85. 38:58

    yeah but but I think it's a very open question I don't think there's any clear sense of direction of of how to kind of solve these questions if only because of the complexity of the models and and things like this and it it ties back into all the questions R you know mechanistic interpretability and and and all of the research that's going on there um but but but and I really see it as something as like not a kind of you know safety say you know let's not hope

86. 39:24

    Killers or something but something that's actually like for the kind of day-to-day use experience um if we are going to start using AI agents to execute a lot of tasks dayto day then it starts becoming very important I think to get a sense that the agents are actually doing things that conform to to your common sense and there not some Eng that is encoded some bias or common sense from some you know open Ai and then like feeling that you know back into you uh if you're you know whatever

87. 39:54

    like trying to analyze data analyze news uh trying to generate you know secure code according to some specification or or things like this um and I think that that's quite exciting and something that maybe is a bit underd discussed in a lot of talks around transparent Ai and decentralized Ai and in user and AI um probably because there are no good answers at the moment um but but I think it's really interesting to think about what that would even entail yeah yeah I

88. 40:24

    have no good ideas in terms of how to do do that with the form verification because the model is very uh the model is an Alchemy it's not it's not like a well understood uh process but but in terms of uh to address your other concern uh it's with keys my understanding is that you can have uh in the future like the attestation you can you you can you can you can run the process in such a way that the future you can prove that the output is the result of a particular computation and therefore you can start

89. 40:56

    by saying well we're going to start with the you know like common craw Dum uh you know that goes all the way up to Mid mid 2020 when was the chat GPT M mid 2022 right uh and then the whole data preparation process the whole model training process are open source and there's a commitment you know there is a proof that they were used to train the model right so then you know that at least

90. 41:20

    intentionally uh unless someone was smart enough to put something you know into the common contr before 2022 then at least intentionally nobody's trying the model is not trying to deceive you right so that's uh that's at least like part way there in terms of solving the problem yeah I think I think that would that would help a lot but but I saying like a lot terminology around you know what open source AI is in terms of you know does it mean open weights does it mean open data is still is still kind of

91. 41:53

    so maybe kind of either misused or or confusing um that it's it's it's hard to always be super specific in terms of what you mean um and and that makes it hard to evaluate a lot of things but but I think yeah if you get you know if you get to the end to end thing where you know what data is trained on you know that this a kind of standard data set that you know people have looked at to some extent

92. 42:17

    right obviously if the data set is is insane in size you know it's not like you won't be able to really audit it um then then that would like help quite a lot I think um and and hopefully we start seeing this because one of things is you know you have listry now is what people think of as you know the epitome of an open source model but in practice it's trained on a lot of propriety Facebook data that we will never see um

93. 42:41

    and and never understand and that always kind of makes me slightly uneasy from from that perspective y so so something I like about it so as I mentioned right for the RO data you will you will need like on the order of tens of trillions of tokens right so nobody will review in any meaningful weigh tens of trillions of tokens but they can review the data pipeline right and the inputs and say well okay as long as we believe that

94. 43:04

    those inputs are actually common C and we have those beliefs about the common C then that data set has the following properties right uh but for the fine-tuning data I think an interesting approach here is you can define a process like like you can as as I mentioned we we did a lot of uh things around data annotations and you can Define data annotation uh like checks and balances the whole

95. 43:30

    protocol on the smart contract run the whole annotation on the smart contract so now you know you know exactly which participants participated in annotating data what was the review process what was the guidelines for review right so so so you can have certain uh estimates in terms of how much malicious data was able to sneak in uh through you know during the preparation of fine tuning

96. 43:53

    data there's a lot of interesting ideas there around you know can provide yeah I think transparent annotation would be a a big step um that would be very cool to see yeah yeah but yeah it's it's it's a bit of a theot from formal verification but there's a lot of interesting ideas there that yeah but but I think I think to some it's it's a bit of a d root but I think it's in um like it's not like I think for verification is some silver bullet that will solve all of these problems I just think it's a useful

97. 44:28

    framework to think about these things because it forc you to think of trying to Define things properly and trying to figure out ways of understanding you know what different things imply and and how to reason about them and so from that perspective I think it's it's always useful to keep in mind but obviously the kind of yeah the complexity of everything will will always make it hard but then if you know maybe if AI if you get you know actual

98. 44:51

    HGI maybe maybe the AI will figure out how to formally verify itself hopefully yeah that would be you know if it is possible at all eventually it should be able to do to do so yeah um yeah it' be nice I think you know a test case of if you ask it to generate you know a bunch of Pon code can it generate a proof to that Pon code is you know matches the specification you asked it to generate and I think this is something that people are actually working on I was in a workshop uh I was at a workshop in Cambridge earlier in

99. 45:23

    October and and someone did actually bring this up that you know now the people are you know getting a lot of code from prompts then instead of prompting you know Claude or chaty PT for some R code you should prompt Claud chat GPT to generate some code in a specific language that you would then design for that purpose do would then be extracted into you know rust or something like this with a verified

100. 45:47

     Pipeline and I think that's you know one maybe practical way of addressing these things is is developing the tooling s to instead of you know getting an output just directly from your prompt to rust and hoping that the can formally verify this actually what the AI output is a formal spec of what you've asked for and then from that you generate you know rust code that matches that specification and and that suddenly

101. 46:13

     becomes actually quite a practical goal and something that's well within uh you know well defined that you can give to form verification experts to to work on and and all you need is to actually design that kind of specification language to the AI returns um as the output of a prompt and and hopefully that kind of makes everyone's life easier to to get form verified code yeah yeah it's very lines of what uh I think when we when we were starting near

102. 46:44

     AI with Ilia one of the diagrams we had was you know user talking to the AI but the AI is not is not solving the problem yet the AI is building a formal specification of the user request communicates it back to the user until the user says yes that is exactly what I want right and then everything Happ in the symbolic space and you know you sort of know that what you get back conforms to the specification that you and the

103. 47:07

     agent you know device together which I think is interesting yeah I think it's very yeah yeah like I think everything that's in going in that direction is is really useful and I think you know if you're talking about code it's at least possible to start reasoning about you know specification in some foral sense right it's when you move to you know other things that are based on common sense where it's much harder to Define

104. 47:33

     that in a formal way um and and because everyone has you know their own personal view of what common sense might be in in in their own biases that they think are correct um and and that's something that's you know the the next level once we figure out you know generation of correct code I suppose yeah yeah okay we're slightly over time so as a closing as a closing thoughts uh so if people you know there are probably people who are interested in formal verification or

105. 48:03

     you know in application with to evm where does they go uh you know to get involved uh so the verified dzk m.org website is a good start and then my email is listed somewhere on that page and and that's a a good next step after that um we've got a lot of people involved we have one big telegram Channel with 140 or 150 people who are kind of interested in the project and obviously for some of them participating in in getting funding to to work on this um so anyone that wants to have a look

106. 48:37

     at contributing and want to follow things more closely than then the documentation will be posted on the verified dkbm website um can send me a message and and we can go from there and and they can get in touch with everyone awesome okay that was a that was a very exciting uh topic and uh thanks a lot for um for joining us today and uh yeah yeah thanks for thanks for having me and um I'm looking forward to the 500 billion parameter model that you'll

107. 49:10

     train that'll be fun yeah okay