Trust Models for AI-Generated Code — Andrey Lyashin | Ordocode

Hi everyone. So I'm trying to realize how to use all these devices. Yeah. Uh so a few words about me. Uh I'm Andrew and for 20 years I was doing some stuff with mathematics with formal methods and especially in blockchain technology in smart contracts.

So today uh I would like to uncover some special things about how we can create and how we can trust some specific s software uh in terms of how we can develop it, how we can check what we have developed and especially I would like to uncover the things about AI generated code. So everyone is using AI now. So everyone is using agent and agentic wave IP coding whatever. uh so the way of thinking about software and the way of thinking about smart contract especially changed from my perspective so and the change is uh like you know that's [clears throat] not the previous adopted methods of delivering of trusting to software uh has been changed just because their agentic way to produce software changed the world and we cannot even predict of how the software will be will be created in the one two maybe five years. Um yeah so start with the Yep it's it's not the first slides sorry actually it's not the presentation I would like to to tell today is another one [laughter] I was talking about that yesterday on another on another meetup So of course I I can repeat my previous talk but I would like to tell something bit different.

Absolutely. Yeah I I will try to make something. Uh actually what I would like to say beyond the presentation uh is like uh you know when you're using AI when you're using LLMs to produce software you think just you know please DLM produce me some beautiful code and of course uh it's answer yes I can do this and when when you ask the question if that code is good he can answer no it's absolutely absolutely bad and the fun thing is that the question you ask to you know to LLM to AI can can be answered in both way. So it can answer yes and answer no and the and the funny thing is that nobody knows is that yes or no. And my talk today is about how to get the right answer on this question.

how to get there, how to pre pretend to imagine what is what is actually happening with software which is generated by AI. Uh yeah, I need I I I need to prepare some joke to fill the gap. Uh but I don't have just let guys for wait for one two minutes. Sorry for that. It's not my fault.

Maybe uh maybe let's let's talk about uh does anybody know what is formal forification uh something like that? Please raise your hand. No. Okay. apologies for the little technical delays.

Um, There we go. We're back. We're back in action. Yep. Yeah.

So uh the next slide showing the the situation when you are trying to create any software with AI and of course you can you know estimate the high highest almost highest uh in the old future of software creating speeds of of producing new code and the bad thing is that uh the number of bugs in seconds grows the same way maybe even faster. So the more code you produce, the more technical depth you have today. And so that the problem just just because nobody knows is that good is that code good or not. Uh just because it has a lot of bugs and it has a lot of you know misinterpretation of your intent, misinterpretation of technology and you need to somehow to investigate if this code is good, if this code is what you wanted to to to to get. Finally uh to speak about this in from you know from from perspective of evolution uh I would like to say that every process every process uh needs to have just two forces mainly one force is you know positive force and another is of course negative so and if you don't have one of that you cannot you cannot just evolve or you cannot correct what you have and every evolution process must have two forces and one force is to create new things.

One force is to explore something and another force is to measure what you actually have now and to compare with what you wanted to have and then you need to fix somehow what you have. So the biological evolution works like this way but you know naturally and we can try to create something similar into the processes of software creation. uh then I will speak of you know [snorts] not not not pretending to to cover every every way of creating positive and negative forces just just start from what everybody knows it's no reputation thing and reputation by its very nature is the positive force just like you know the more reputation you have the more resources the more success you can you can get right and the more resources you have the more outcome you can produce. So that's that's of course the positive force. So uh the more you have the more you get.

Okay. So the problem is that uh I think that this process cannot be sustainable in any sense. No, in some middle term it will it will break itself right just just because it doesn't have any negative correction forces. So we we of course we can add it like like this way. Uh the processes approach uh you know shows you how you can combine just evolving and correcting steps in your pipeline of software creating.

For example, and on the graph below on on the bottom of the slides, you can see of how you can think you can drive from the some points a where you start to produce a software to the final target where you can see if if you produce something what you like to produce, right? But the problem here is that there is no no direct way. Every software developer know that that there's no direct way to produce software just going by line you know and you of course in every step you have two two direction uh one direction is to over evolve the system just to create new features just to satisfy your customers whatever like uh to add something and when you added something you think oh my gosh so I added something that I cannot control just because the system is under constraints and there's a problem just because you you begin to constrain the system you add more tests you add more audits and to end testing integration test and after after all you have the over character system which is too rigid to produce new features that that's also the problem and the bad news is That in aentic way of code producing all these all these lines are too rapid and just one day and you will be in over evolving state. One hour more and you are in rigid state where you cannot produce any new more feature. So we we need to think how we can add something here just to be in the right place in the right time.

Uh [clears throat] one one uh words about the audit. Everybody knows what audit is. So and audit is like you know uh ask somebody or maybe several several guys what my code actually does, right? And and the funny thing is that you can ask this question in two different directions. And one one question is does my code contain contain bugs?

Right? So I I do have specification that's that's my documentation. Very good. So please check if my code has bugs or not. And this is all we know.

This is all we know. And that's the normal audited task. But another way you can ask the modern LLM just you can ask is my architecture is my design as good as as I need to produce features I need. Right? And in both questions you you will get the correct answer some no some answer from LLMs and they can say yeah your code has bugs and yeah I have 100 ideas how to create new architecture which which helps you to produce just more features etc.

So and uh I suggest that audit currently can be can be thought just to just to work in both direction. So you can you can just uh reveal bugs or you can just uh upgrade this upgrade the architecture to produce more features. So I suggest that every every developer can can think about this in this way because that is very good uh because it's it's working in both directions you need to make your system sustainable. What about my profession? What about the form of vocation and why I would like to tell you more about this today is that uh I think you can think of all these correcting steps like suggest you're driving a car and you have gear you have wheel you have steering and that's all your internal processes which can locally operate a car but the question is where is navigator so the question is where are you now and the answer can can can be seen that like you know it's not the you know it's not the unique answer on this question so where uh I am where I'm am I now and the formal methods can answer this question in most precisely way so I can just uh correspond your quote to the formal specification and the answer will be yes you are in the right place or no you are not in the right place so it's working like GPS you know [snorts] uh and of course you need of course you need all the things I I mentioned before you need gear you need wheels and this is you know nor [snorts] normal way of software producing like testing creating new feature etc audits but but the question will still uh be like where am I and formal methods can answer this there are a huge amount of formal methods currently we have in in industry.

So and on this slide I tried to put them in two different textes. The first one is the how precise is answer how sound is is answer. Uh so can we believe this or this is just an opinion. This is the x-axis and yaxis you can see what actually properties uh can we cover but by by every methods we I mentioned. So and yeah starting from audit which can answer on every question you asked but it's less precise as can be imagined and finally at the right hand side you will have the deductive verification the most comp complex and sophisticated methods of software anal an anal [clears throat] analization and the uh answer is most precise but the currently uh I cannot say that uh deductive formification can cover all the questions you have about your software design.

So uh funny thing is that uh speaking about the first six six points they will not move they will not move from time to time but deductive verification uh from time will be move higher and higher because it cannot lose it its soundness but it can cover more and more areas of of you know uh industry. they would like to check to verify. Yeah. So all these methods uh can be applied to software and all of them will answer certain questions about what you have now. But deductive verification will answer any question in the future but currently not but the answer is the most precise the most precise.

So it's the best GPS in the world. Yeah, that is the problem [laughter] I would like to this my favorite thing just because uh uh funny thing is that nobody knows what software actually does even developers even creators nobody nobody in the world uh so just because is very very s simple answer just because what people mean cannot be formalized in mathematics at the moment and this is a gap in you know in general human knowledge how we can you know get from the human meaning of the words to mathematical meaning of some terms and this gap can be filled by you know uh by engineering efforts at the moment. So there there's there is no any scientific answer on this but we can fill this fill this gap uh step by step adding more formal specification uh going from human words to math uh losing some flexibility but getting some more formalism. Uh to do this from my scientific view uh we need to imagine some new language uh which humans can still speak and which is much more close to mathematic is more than one. For example, uh the there exists a lot of efforts here to somehow present the human thinking in more formal way and natural language processing uh science is you know is rocketing at the moment.

So I think in maybe two five years this gap uh will be filling much more much more interestingly than today. So and we in in my company we're also working here uh studying the way of how we can explain human words formally and how we can shift this gap to just engineering efforts. Yeah. [snorts] Uh so final opinion here that the gap is not is not conceptual. So you can you can you can just try to solve this technologically.

Yeah. [snorts] So uh my idea how we can uh add formal methods this two slides just uh with added formal verification in the loop is just you you have your normal legacy development map. So starting with plan then you code test audit some somehow analyze the results and looping to the start again plan code test audit and this process is okay as I told this very good and it's working excellently but the uh this green things you know formal specification formal vocation will add two points just what you have at the start what we would like to create that is the specification and what you have at the final and the and the in the end of the story that's a verification. So that's your GPS and uh uh in previous years you know it was very very very expensive to add this into the loop but with aentic age you know this can be done in much more cheaper way. So just because agents can speak any language and they can speak a language of formal verification that's what we are doing in order code.

Uh so we added all the stuff in one gigantic agentic loop uh with 80 agents working together and some of them are doing the thing of formification and solve the stuff as I have speaking before. So fizing testing everything specification different ways or to specify all this stuff [snorts] and yeah now the idea is to uh now the idea of horicult that's you can go just from your intent just to code which is known how it behaves right so going through through all this all the steps and even to do that we have created our own programming language which is called Cambrian and that's is a first force language humans can't program on that uh but agents can and this language bring the bring the you know the bridge between between uh programming languages like we like we used to do every day and what we can actually verify actually prove Right? Because the artifact of verification is the proof not the K proof but another way another another uh kinds of proof it's called deductive proof. So it's artifact it can be seen as a program. So it's not just handdriven proof and can and the good thing is that this proof can be independently verified by software another software.

So yeah uh that's prefal slides. Uh so what's my uh intention here to to tell you is that all with all this stuff we are one step closer from trusted way trusted trusted way of software creation from trusted world where we need to think about whom to trust which producer to choose uh who are customer who are developer to more trustless world where we can trust the the software itself. Trust the uh programming artifact just because there these artifacts are proven in a in a absolutely certain and maximizely precise way. So one step closer to trustless world. Yeah, that's the final slide.

Uh I would like to ask you all to come to our booth and if you're interested to know let's talk about all the stuff uh I can share all my ideas and my colleagues will show you of how our platform actually works. Thank you very much guys.