Autoformalization and Verifiable Superintelligence with Christian Szegedy - #745

Also next year, we will see the first time that AI will surpass human scientists and mathematicians in a lot of domains. And we will see that AI will solve problems that humans couldn't solve before. Not just like extremely specialized problems like saying protein folding, but really like whole scientific domains will be dominated by AIs by end of next year. All right, everyone, welcome to another episode of the TwiML AI podcast. I am your host, Sam Sherrington. Today, I'm joined by Christian Segedy. Christian is chief scientist at Morph Labs. Before we get going, be sure to take a moment to hit that subscribe button wherever you're listening to today's show. Christian, welcome to the podcast. Yeah, thank you. I'm really looking forward to digging into our conversation and super excited to have you on the show. You have had an incredible research career in AI. Just thinking about some of the work that folks might know you from. the inception paper in vision, batch norm, your work in adversarial examples, not to mention being a co-founder of XAI. You have done a ton, and there's lots of things that we could talk about, but for the past 10 years or so, you've been really focused on the role of mathematics and improving AI, auto-formalization, and a focus on verifiability. And that's really going to be where we center the conversation today. But to get us going, I'd love to have you share a little bit about your background and what really drew you to the field. Oh, thanks a lot. So yeah, generally I was interested in AI since I was a kid, like the 80s. And I always wanted to do AI, but back then in the 90s it became really hard. so I studied mathematics so I have a PhD in applied mathematics and I worked in chip design for quite a while so I came to the US to work as a research scientist at Cadence which is a company that develops software for EDA so design automation for chips so I learned a lot about the various bottlenecks and also the importance of verification there but I worked mostly on physical design so generally optimization convex and non-convex optimization so at 2010 I decided that chip design is getting slowed I mean most of the interesting developments are not happening there and I started to think about what would be the next step for me and I thought that AI will take off so that was my prediction in 2010 when it was like for most people it was not obvious but I thought that this will be happening soon. So I considered which company is the best place for that to join. And then I thought that Google has the most data and the most talent in that direction. So I joined Google in 2010. But I first worked on some advertisement optimization project, but I quickly got into a computer vision. So my previous manager Hartmut Neven, who is now leading the quantum computing effort at Google, he was head of the mobile vision. and I worked with Hartmut on neural networks. And he was not really enthusiastic about neural networks back then because he did his PhD on them and said that it was probably a dead end. But in a year it turned out it was not. So then I worked on object detection, human pose estimation classification so I designed a lot of networks around that area so the networks that I designed this inception was very useful back then where there were mostly CPUs used in the data centers because the network was much more efficient than even the NelxNet so on CPU architectures and it's still used in embedded systems quite a bit I hear from people So it's not the highest quality network, but it's one of the most efficient ones for those purposes. And it inspired a lot of work that followed it. Yeah, it was a lot of ideas that I just sent out today. Also, I found first the adversarial examples for computer vision in 2011 or 12. Yeah, so it's end of 2011. I didn't publish that result originally, but then I talked to Wojciech Zaremba, who was a co-founder of OpenAI, and he convinced me in 2013 to publish that. And a lot of people didn't want to believe me that that's possible, that we just slightly changed the image and then it gets misrecognized. Also, Jeff Hinton joined Google at that time, and he told us that, yeah, that's a problem if that's true. but he also initially didn't believe me. So that was a fun time. So I worked on computer vision until it became like very crowded and I was thinking, okay, now it's time to do the real deal and do reasoning, which back then was not really the main progress. So it was like, it took like seven more years or six more years that people started to focus on reasoning. But I thought, okay, that will be the next big thing. So let's do reasoning with AI. And I started a team at Google, what was called Interformal, which was this idea of connecting formal and informal reasoning via neural networks. And that's what I worked on until 2022. 22 when we started to see in my team that this could be scaled up dramatically and try to get resources for it at Google, but we just got like they said, yeah, this work is very important. We will come back to you like half a year. And then as I went, okay, that doesn't work. So let's start a company And then we talked to several people trying to get funding. And at some point, it turned out that Elon also wanted to start an AI company. And so we went there. And that's where XAI started. But after one and a half year, I found that XAI didn't want to focus. So they just wanted to focus on informal reasoning, which was not my main interest. And then I thought, okay, let's switch gears again. And then that was when I joined Morph this year. And we started to work on the actual auto-formalization idea again, which is the formalizing goal of mathematics. And we made some progress on that, yeah. Talk a little bit about the distinction between informal reasoning and formal reasoning and why you're so excited about the latter. Yes. So, I mean, I'm excited about both. So it's not like I think that informal reasoning is much more used nowadays because informal reasoning can be much easier to apply on a lot of domains where formal reasoning cannot. and so most language models today use informal reasoning which means that they just spit out some text and that text cannot be easily verified even by humans so if this is a complicated task, let's say some solution to a mathematics problem then it can take very long time even to verify a one-page solution and it can have subtle bugs so the history of mathematics is full of these even human proofs like the proof of the four colors you are there were like three times people thought that it was proven and that they forgot it for 10 years and then 10 years later they figured out that the proof was wrong they published another proof so so that happened in mathematics several times that you find subtle bugs in your informally given proofs so most people would think that mathematics is mostly formal because if it has formulas etc that means formal But actually what I mean by formal is much more that it's a computer code that you can actually run, and then it gives you absolute 100% certainty of correctness. And that's, so basically by that standard, most human mathematics is not formal. Only a very, very tiny fraction of human mathematics has been formalized to that extent that we can 100% certain about its correctness. And what's the relationship between formal math and formal logic? Yeah, so it's a very close relationship. So basically, formal math is logic turned into program. So to use the same logic as formal logic uses, it just... Formal logic is basically a procedure described in an informal way, such that humans could check on paper whether something is correct in theory. But typically you need like thousands of steps even to prove a simple theorem, like Pythagorean theorem. You need like tens of thousands of steps actually to prove it. And humans cannot do it by hand, but computer can easily do it. So it's kind of like formal logic. It's kind of like a specification of a computer chip. and when you implement an abstract CRM prover that's kind of like implementing that chip so basically taping out that chip and then actually being able to run at high speed and so that's the connection between formal logic and CRM provers and there are a lot of formal logics that people use like several different ones so there is like the first order logic, the more classical that Gödel uses, there are C-O-N provers that are based on that, but they are very convenient to use for human at least. And then the higher order logic systems, and then nowadays is a special higher order logic, is this type theory-based, dependent type-based prover, Lean, that is the most convenient for human mathematicians to be used. And talk a little bit about how these ideas around formalisms and verifiability create to or link to your broader objectives with regards to intelligence. Like what really, what vision is motivating you? Are you driven by a desire to create, you know, AGI or super intelligence? And you can talk about which of those terms you prefer. Are you driven by practical concerns? You know, what do you see as kind of the end game here? And how does your research lead towards that? Okay, so to clarify my terminology. so AGI I don't really use ever because that's a very overloaded term and everybody means something different by it. I use superintelligence as a word as a domain-specific intelligence that exceeds human abilities by a large margin. So that's why I prefer superintelligence because you can say mathematical superintelligence means it's a vastly better mathematician than any human. So that's something that's a much more quantifiable objective term, in my opinion. So AGI is very hard to tell because it's the coverage of what is an AGI. So what does AGI really cover to me? That's very unclear. And that's why I don't use that term. If I say, OK, it's super intelligent in this respect, like it can detect certain object in the world, better than a human, then I think that's clear what it means, or at least you can develop a benchmark for it. So that's why I prefer that. So does that mean that it is by definition narrow in the traditional sense of the word? No, not necessarily. I mean, a superintelligence can be superintelligent in any domain, but I mean, the problem is the quantifier any, because it's not... So you tend to focus on more narrow domains as opposed to necessarily trying to create a generalized super intelligence. I mean, I don't say that. I prefer notions that I can objectively test. So basically, if I say that I can tell, is it X or is it not X? So if X is a notion, I want to be able to tell that. to me is like a notion that is quantified by a fuzzy set of like a lie set that is not clear, not clearly specified. What it is, it's basically an unfalsifiable statement. So that's why I don't prefer it. I don't, I believe that an agent that can reason about mathematics that would basically cover 99% all of the reasoning tasks that anybody can come up with. It's just mathematics is harder to apply, but I mean, for me, mathematics is a much wider notion than most people use. So for me, it's like this mathematical logic is really, it would cover like almost everything. but I don't want to make that kind of statement because I don't want to overhype it, but I really believe in that. And in particular, the idea that, you know, common statements, things that you might want to interact with your AI about, these can, in some future world, be transformed into formal mathematical statements operated on by the intelligence and then transformed back into more human, consumable statements. But that formalization presumably addresses issues like hallucination and other challenges that we have with today's AIs. Is that the general idea? Yeah, that's just one, but that's an important aspect as well. But I think that the list is important. So I don't say necessarily that everything needs to be formally specified and then formally processed and translated back. But I mean, that's a big part of it. So I think as if you get better and better understanding certain aspects of reality, at some point you can capture those aspects mathematically. And what I mean by mathematically is not necessarily the same notion of mathematical that most people It's not like, okay, give a few simple formulas or a theory of everything for that. It's much more like mathematics can also be an extremely complicated distribution, probability distribution, about you can make statements and then you can do bounds on that distribution. So basically, what AI does is represents, so today's AI's neural networks represent the probability distributions by just using a few matrices, like thousands of matrices, but for mathematics, it's just a few. And basically, it's basically just mass. So also, informally, AI is just mathematics, essentially. It's just a bunch of matrix multiplications and extra functions. But it basically captures probability distributions very mathematically. And we can make mathematical statements about those. So that's why I believe that mathematics can capture much more than we think it can. It's just that our capabilities of humans are not very bad at mass. So we cannot really use mass as much as we would need to get really good But AI will not have that constraint So that's the point here. I think that's an interesting point to call out that, you know, today's LLMs, today's AI, it's all math. It's all mathematical operations. so clearly you know just an AI that is good at math is not enough it's about the kind of math and the way that it processes math that is the focus of your research so elaborate on like kind of how you see the you know direction from like where we are today to where you're trying where your research is trying to go? I think that AI research has a lot of very useful passes. So one pass is this kind of like approximating reality with neural networks without any verification. That's still extremely useful and important agenda. And most people focus on it. So that's not my focus because I don't want to do that everybody else is doing. So, but I still, I'm very, very convinced that formal verification will gain on importance in the next few years. And one part, so basically what I believe is that AI needs to be somehow kept in check as we go on, because AI is getting more and more powerful and we don't exactly know what it does. And that way we want to create safeguards for AI not subverting us what we're asking from it. So we want to be able to tell statements about the AI's behavior. we want to check the output of the AI, that it gives correct answers. So for example, if you synthesize some code with some AI, you want to make sure it doesn't put backdoors in your code. It doesn't do some self-serving purposes when you are using it to create like a critical infrastructure for yourself. Because it might, so if AI is so super intelligent, then it could basically create all kinds of extra artifacts in your code or in your infrastructure that you are developing, maybe chips you are making with AI or even like larger plants. And then they might be subverted by AI in a way that at some point it can be used either by malicious human actors or even by AI actors to exploit these holes in the designs. So I really think that what we want that AI should produce always guaranteed artifacts that guarantee certain properties of those artifacts. And that's one way to prevent AI from subverting us. And one way of doing that is by formal verification because the advantage of formal verification that the verification will not depend on any AI. So you can run a verifier and then those properties will be checked completely without any AI interference. So you can be sure that those properties hold. You don't need to rely on another AI that, okay, I double-checked this AI and it works. And a lot of other ideas of people, but people in the AI community often propose, okay, let's have AIs that check the AIs, but I don't think that's a very safe way to go about it. There is obvious loop was in that. So yeah, but I really think that there are two aspects there. One is the verification aspect for AI that we say, okay, is the AI created something correct or the validation aspect. And the validation is much more, did the AI create something what we wanted? And the problem is that verification can work with formats specifications. So if you formally specified what your code has to do, then you can formally verify it if you have a strong enough prover. But the problem is that validation on the other hand cannot be. That's the question whether your informal description of the task that you give on the AI, is it really matches the formal specification. So it doesn't say that, okay, that the AI created the correct program. It just says, did the AI create the correct specification for the program to be worked on? Let's take a step back and linger on this distinction between verification and validation. What's the input to verification and what's the output to verification and what's the same for validation? So the verification takes a formal artifact. So basically two formal artifacts. One formal artifact is, for example, a program, and the other one is a proof of correctness for that program. So maybe you can say it's three. So that is a, the AI takes a, and these all three are basically formal. So verification only works on formal. And it's verification takes the program, the specification, and the proof. and then it says does this program specify does this program work according to the specification given here and does this proof proves that and and then it checks the proof and if the proof is correct then it says yes, everything is fine, but everything is only in the formal domain and that's the problem because humans are not very good at creating formal verification specifications either. So after you created the specification, it's much harder to prove that your specification is satisfied by the program, but just creating the specification is hard enough. For validation, you are taking an informal specification and a formal specification. And then it has to check, is the informal specification covered by the formal specification? specification. So is it the same specification that the human intended? And by definition, you cannot formally verify that. So you cannot formally validate something because there is always like a subjective component. So that's the definition of informal, that it's a bit fuzzy. Right. But I think most people don't really distinguish these two things. It's like there is this confusion that they don't separate these two concepts. And I think it's very important to say, OK, we can verify a lot already. We should use that methodology, but we should draw a clear line between where we can verify something and where we should just validate it. And I think validation will require some AI process because humans cannot really check like formal artifacts very efficiently. So we need some safeguard. But at some point, the risk is much lower if we are splitting formal verification and validation into two different categories because something like a simple property can be very hard to be satisfied in a program. So for example, you say, I want this program never to crash, then that's a simple thing. We can specify it easily, but it might be very hard to prove. So it's still worthwhile to have the verification component as a rock-solid thing in the whole system. And that's what people do for chip design, by the way. So it's a no-brainer for 25 years. And I'm old enough to remember that in chip design people, like in the 90s, they said, come on, I mean, it's impossible to verify chips formally because it just felt too hard. Like people did like patterns similar to unit tests today for programs. They just generated random patterns and tested the chips on that. And then you remember there were like kind of like the floating point bugs and others. So things can fall through the cracks if you don't do complete verification. And then when it became feasible, around 2000, set solvers came out, and suddenly the whole domain shifted. Now we do it. Why not do it? Because if you can do it and it really helps, then let's do it. yeah that's the specification domain and the physical domain of chips is a lot more constrained than the ideas we're talking about now like language and math and intelligence right i don't know i mean it's a different story i mean the the physical verification of these chips is like insanely complicated much more complicated than anything else i think about humans programmed i I mean, you have to verify, for example, how the light behaves physically and make sure that when you are lighting all these masks and everything, that they will get the right patterns and all those things. All the signal integrity verification, you have to emulate very, very complicated signal behaviors of continuously how the electric signals behave. So you shouldn't underestimate that. So that's a very, very complex domain. The logical verification is still kind of maybe easier because chips are more constraints and the properties you want to verify are simpler. But I think the general verification of the chips is like insanely complicated. Got it, got it. So it's that domain, when you think about it and to a practitioner in that domain, it extends beyond logical verification and goes down into like the physical properties of the chip in silicon, and it's complex. It's extremely complex. So there is the logic, then there is the signals, and there is the physical where the chip actually has the right structure at all because currently when you are lighting the chip, it's like the interference pattern says to align, so you have to solve the Maxwell equations at the live scale, which is crazy hard. Okay, okay, okay. So in talking about verification and validation, one of the works that you publish is auto-formalization. And it seems like that is kind of a foundational step in kind of thinking about these two ideas. Can you talk a little bit about that work, what you think its contributions were? Yeah, I mean, I've been working on auto-formalization for a very long time. I mean, I published multiple papers around that. So, I mean, I still have the same general idea, but of course it got refined. And since language models have surprised me as well. So around 2021, I started to say, oh, okay. So a lot of things are much easier than I thought they will be. So, yeah. So yeah, basically auto-formalization is the idea that we want to exploit the data that we have in practice in a much deeper way than current pre-training does. So current pre-training just tries to match the surface level structure of language. So basically just predict the next most likely token. I don't think the next token prediction itself is a bad idea. I think that's not itself the problem. The problem is the training methodology of how do we train the next token prediction. So we already seeing with informal reasoning that just dumping a lot of data into the model and then always predict the next token is inferior to let the model try to solve hard problems and then reinforce those next broken prediction streams that led to the right solution. So that's the current star, this star paradigm. So this paper was also co-authored from Tony Yuhaivu, who was at my team at Google. So it was developed before he left Google to start XCI. So basically, the idea is that in order to train at a much higher level of efficiency, meaning that you learn most from the data, is that you need to change your training methodology. Your inference time, you still do next token prediction, like the thinking models do. But at training time, you're using RL, reinforcement learning. So letting the model try things and then reinforcing the successful reasoning. And that was the big change in models, language models in the past year that has led to all these much better reasoners that can solve IMO, for example, IMO problems, mathematical Olympiad problems or exit human reasoning in like a lot of areas. like at least get to graduate level reasoning is mostly based on this reinforcement learning paradigm. But the models are still a next token prediction. And I'm kind of agnostic about whether next token prediction is the right long-term things. I'm convinced that next token prediction will be obsolete in a few years. We will probably use like diffusion-like models. It seems much more natural to me. And it's much more efficient. But still, I don't think it will change the abilities of the models. It will just change the efficiency by which we are using the models. So basically, it will be very helpful, but that's not the main problem. So next token prediction itself is fine, probably. Okay. And so how does that connect to auto-formulization? So basically the idea is that we want to create this lot of problems to work on. And we are running out of easily verifiable problems nowadays. So it's like we have run through all this. We turned a lot of the mathematical competitions and programming competitions into verifiable problems that are somewhat verifiable. But there is an end to it. And I think that the next stage to make a lot of verifiable problems for RLing is that we want to interpret all of mathematics and turn them into verifiable mathematics. And that means that every mathematical problem can be turned into almost like a computer program that you can run with a proof. And then if that proof runs through without error, then you have solved that problem. So it becomes something that the verifier will be, basically, it's running a program. And the good thing about that, that doesn't depend on any AI. So currently, a lot of advances happen because AI is checking AI. So basically, AI is great to their own solutions. But I think that's a bit, I mean, there are multiple problems with that. one is efficiency because, I mean, AI is slower than traditional algorithms like this CRM proven. Secondly, the solution is not clearly correct necessarily. So there is a lot of room for reward hacking, for example. And also, if we get to the point that we created some super, like for example, a new proof for some famous conjecture, then we will not be able to say for sure whether that proof is correct if we don't use formal methods. If only AI says, okay, I checked your other AI's work and it looks correct, then I mean, I wouldn't trust you. Today's AIs are not that good. So basically auto-formalization for me is more like creating a huge library of all of the human knowledge that's formalizable and then turn it into formal mathematics or formal artifacts. And then this can be both used in new proofs or new derivations. And also they can be used for training an AI that I think will be super intelligent at this point in mathematical domains. Earlier, you brought up the example of the Pythagorean theorem when we talked about the distinction between logic and mathematics in terms of formalisms. And you mentioned that the Pythagorean theorem is like 10 steps I think you said I mean I just said some number I don know The order of magnitude, right? Yeah. But the idea being that we've got lots of math, but the math that we have is very different from the thing that you're saying that we need in order to train these models. And so in terms of how to think about auto-formalization, give us some examples of a thing that you might want to auto-formalize and what that looks like when you've auto-formalized it. Basically, there are a lot of CRMs nowadays that human mathematicians care about and they actually, they try to formalize it like Fitzmedalist Teri Tao has worked on this prime number CRM that talks about the distribution of prime numbers and then gives an asymptotic estimate of that. And that was a very hard work. People worked on almost a year or something like that, and many people just to formalize that single statement. And that's just one statement of many that human mathematicians have proven. And when you try to formalize those statements, then you end up with a lot of small statements that were not clear that they are problematic. But it turns out, yeah, we have to check that, and then you spend like a month on like proving some substatement that it turns out to be necessary. So it clarifies the thinking of mathematicians as well, of like saying if you formalize something, then you have to do these kind of steps as well. And I mean, most mathematics is not formalized. So I think that the first step would be to formalize most of mathematics that humans have done. And these mathematics includes extremely complicated mathematics, like the differential equations that govern the behavior of light, for example, or fluids. So basically, everything that you can, mathematicians, work on and publish could be formalized in theory. And we should, in my opinion. And humans will never finish. It's kind of like saying, in order to predict the weather, you needed like 10,000 people computing by hand. But, I mean, if you have computers, you can predict the weather much faster. And so I think some mathematics could be formalized on a live scale. And that was one of our recent results a few months ago, is that we formalized a not-too-complicated, but still research-level mathematics statements. That is a relatively new statement about the very famous conjecture, the ABC conjecture. and we managed to formally verify the whole paper. So that gives a 100% certainty about that paper. And that's important, especially in that context, because ABC conjecture has the full statement, a much stronger version of it that we proved, was some Japanese mathematicians have given a very long proof of it and nobody accepts it. Very few people accept it. They think, okay, there is a first episode 30% probability that it might be true, but most mathematicians think it's probably not true. But nobody feels like reading the whole thing because it's just too complicated. It's a very famous mathematician, so it's kind of like a precarious situation that there is a proof of the famous conjecture, but everybody thinks it's probably not good. So we want This could be prevented When we are formalizing all of mathematics But that's just a side effect But I think once AI gets to the point that It knows all of human Mathematics to maximum Accent and it basically It will be like a much much better Version of any human mathematician And then it can develop new Mathematics for for describing biological systems, to describe economy, to describe the behavior of the world in like behavior of complex systems, etc. And that will be a lot of completely new mathematics that humans couldn't even start developing because we just don't have the brain capacity to do that. But first we have to have an AI mathematician just that that's better than Terry Tao or better than any of the best mathematicians today. So it's a low bar, but we still have to get there first. In thinking about that example, I get the formalization part, but I want to dig into the auto part. So you've talked about this one conjecture that you formalized. That could be a roll-up-the-sleeves manual, be a mathematician type of approach, or it can be, you know, presumably, you know, some degree of automation in achieving that. Can you talk a little bit about the automation that was employed and like how you see that kind of taking you to a broader ability to automate? So basically the idea here is in general, we want to do auto formalization. That means that we just let lose an agent on all of the mathematical literature, just like a pre-training just ingests all the data on the internet, basically, that's available. And that's the idea. So the state of the art of formalization so far was that humans had to sit down and write the code for every statement and split down the statements into smaller statements if they couldn't prove them formally, etc. So it was a very manual process. And they use some AI automation, but it's more like a copilot. So it helps you autocomplete, but the mathematician always have to say, OK, I like this line of code, etc. So the automations we had is like we were working with Jared Lichtman, who is a very established mathematician who is very knowledgeable about number theory. and basically he only worked in informal mathematics, but he had to split the statement into smaller statements. So he had to do a lot of informal reasoning, but he didn't write a single line of link code, so a single line of formal code. So it's a very different level of automation. And then we have let run agents, like sometimes for hours, to work on the proofs. and all the proofs were created by AI alone. So basically the whole formalization, that is like several thousand lines of code, was created completely by AI alone. So of course, if the AI failed at some point and said, yeah, I cannot complete this proof, then Jared had to go there and then split the statement into, break it down into more digestible statements. But that happened in informal mathematics. So he was just writing mathematics as any mathematicians write. And the goal here, I think the first goal for us is to create a system that any mathematicians can use that doesn't know about these formal systems. It just gets a feedback from the AI that says, sorry, I cannot follow this argument. Can you make it clearer? Or why is this true? So basically an AI that only talks to you in informal language, like informal mathematics, very high level. and then under the hood, it does all the formal stuff. So the human mathematician doesn't need to do any formal work at all, but you end up with a formally verified artifact at the very end. So that would be the first step. And then the second step will be to take it that you don't even need the human. AI just reads the paper and then formalizes the whole thing completely automatically. That's where we are not quite there yet, but we are getting very close to it. so basically the system we are using is basically a complicated AI agent that can do a lot of operations, it uses Morph Cloud so that it can try different variations, roll them back try new ideas if something didn't work, analyzes the outputs of the compiler, looks at all these things and makes decisions and iterates until it either fails or says, yeah, I found the proof, and then the proof is verified, and then it can stop. So that's how it works. And is it a conventional AI in some sense or another? Like, is it LLM-based? It's LLM-based. What is it? Okay. It's LLM-based, yeah. So, I mean, but we are using other methods as well, But I mean, it's like, in some sense, it's, I mean, where is the line between conventional and new? I mean, it's like, if you make enough changes to a conventional algorithm, then is it conventional? So, yeah. But it's, you know, based on, there's a foundation of things that, maybe this is a silly question, But we can start to reason about this thing not knowing what it is by saying, well, there's transformers, there's LLMs. Those things are trained kind of using the conventional approaches, and you're doing stuff on top of that, as opposed to you talk to your friend that's working on quantum, and it's this whole new thing that we've not conceived of that you guys have invented. Again, it depends on where do you draw the line between. I mean, so I think it's, I mean, I think a lot of people are impressed by it. They say, okay, we don't think. So impressed in the sense that when you show them, when you tell them that what you want, then they say, oh, that's not possible. And then you show them, okay, but we just did it. So in that sense, I think it is impressive already. But I think that's just the start. So thinking of it as an LLM is underappreciating what you've done to allow it to, you know, do these proofs, essentially. Yeah, I mean, it also needs the whole infrastructure that basically goes around. So basically, of course, agents are more powerful, but you have to do a bit of work to make them work. And also then you want to improve the underlying machine learning part as well. So yeah, I think, of course, nothing works in isolation. It's like LLMs are very powerful. And I think once we get collected enough data by new methods, we can train better systems that are doing the same things much faster, exploiting all the new data that we got by auto-formalization. So that's the promise here. And so presumably if it's LLM based, you have done, you know, a big part of what you've done is in post training the LLM. And can you talk a little bit about like, you know, you're using some data set for post training. Maybe you're getting it to spit out tokens or something like special tokens to do the kinds of things you're trying to do. branch with this? Am I thinking about it correctly? I guess is the question. We don't need to dig into the details. Yeah, there is some truth to it. So by the way, we are trying to figure out what is our next step because we need a lot of compute for taking this to the next level. So we are currently in, I mean, we are looking into funding opportunities So therefore, I'm a bit reserved in telling much details about what we are doing and how we're doing exactly. So we want to keep all options open at this point. So I don't really want to get into details. But generally, the idea here is that we exploit a lot of the morph infrastructure to create systems that can integrate with LLMs. in a way that is much more flexible than previous that other approaches can. So basically, we can develop these kinds of agents and run them much faster and much better than it could be done without the infrastructure. So that's an important component. So yeah, but we have a lot of directions in parallel that we are that is both opened by our approach and also important to have an open-ended improvement loop that can get to superintelligence, I think, in the fastest possible way. So that's the goal, is to get to a superintelligence in the fastest possible way. And I think that our superintelligence will be kind of safer than others because we are not just scaling up data. We are making this superintelligence safe by construction that we are only focusing on verifiable artifacts. Others focus on various objective functions, like just predict whatever is there. Whatever the system develops, it depends on what you are trying to predict. So if you try to predict something like some crazy extremist tweets from X, then your AI will be very good at being extremist or whatever. And it's like that's kind of like not what you want in my opinion, but you really want an AI that wants to do like most excited about reasoning and reason really like logically correct way. You know, today we've got, you know, these next token predicting LLMs that are trained on kind of conventional human data in the sense of, I guess I'm throwing around this word conventional, but like, you know, the internet, Reddit, you know, soon videos and other, you know, forms of media will, you know, begin to dominate this data set. And, you know, you're proposing that, you know, we train them formally with, you know, these formal proofs, verification, validation, all this stuff that we've talked about. It strikes me that for, you know, A, that formal, you know, that formal, the formalism is an important kind of backbone for reasoning. how do you is it clear to you how that is melded with the linguistic and kind of world knowledge that the traditional approach brings? Do you have to do that separately in your world or do these things come together in some way? So the idea is that we separate these two issues like verification and validation and of course you want to capture the natural language distribution just like any model, and we are not really trying to tweak that part too much. But of course, the validation, whether something formal matches the informal, it has to be trained and it has to be improved, and therefore that's one important aspect of what we are doing is that we want to create an open-ended improvement loop for the validation. So that's a very important part of our agenda as well. So language models already have a lot of use cases that are not easily capturable by formal methods. So I don't really want to address those directions yet. I think that a lot of them could be addressed by basically kind of like imagine a very good scientist who has like deep understanding of a lot of topics, but still you can chat with it whenever you want. And it can chat you about the weather and how do you feel. But when it comes to some scientific or engineering topic, then it becomes suddenly extremely objective. And then it knows all the possibilities. And it can basically switch between these domains. And I think as language models go, they will move less from this chatty, this very intuitive style to a style that is more based in reality and more based in hard logic and actual feedback from the environment And when you have to just crack a few jokes then of course it will use the current methodologies because it just learned a lot of this natural language. But other than that, it's grounded much more in logic and actual measurements than current systems. So that would be the goal. So what I hear you say is that that formal reasoning backbone comes from your research into verification and that understanding of kind of the, you know, human communication and natural language comes from the emphasis on validation. No, I don't think it has to come from validation necessarily. I mean, part of it, yes. But I mean, we can just rely on, we know that the current LLMs are pretty good at capturing surface level human communication. So that's, we don't necessarily have to mess with that in my opinion. Yeah, that's what I was going, is like at some point once your system is, it doesn't need to do everything, it will work in conjunction with conventional LLMs. At convention, I mean, I don't think that there needs to be a difference. I think whether it's LLM or not, that's again a different question, but you can use one model for everything, but you train it with different methods. So you can have a pre-trained model that is pre-trained with all the human communication, just like current LLMs. And then you're also training it with other methods, and then you create basically an agent infrastructure around it, but you use the same model probably for all the different purposes. It's just like you are creating a system out of it but that's what also the other big labs are converging they also create systems that can do deep research and stuff so they basically do tool use and execute programs and go to internet etc so they're already doing that. The main difference is that we are focusing on a a bit more like concrete to use to improve the depth and correctness of logical inferences. Excellent. Excellent. Excellent. Talk a little bit about timeline. Like how do you see this evolving in time? Yeah, it's speeding up. Yeah, so I think most people are kind of yeah, I don't so even like very high-level people that I talk to and I see recent interviews with them. I think they underestimate the rate of progress still. So I really think that next year we will see a big change. First of all, the current state of the art So basically it will reach the point where AI will become a real economic force in general. So not just like the verifiable things, but just generally. Which will be like a scary thing as well, because I think AI will create a lot of dangers. So dangers of misuse, especially cybersecurity-wise. I think that there will be a lot of problems. and I think also next year we will see the first time that AI will surpass human scientists and mathematicians in a lot of domains and we will see that AI will solve problems that humans couldn't solve before so that will be the first year and not just like extremely specialized problems like protein folding but really like whole scientific domains will be dominated by AI by end of next year. So that's my prediction there. And I think most people disagree with that, especially people who are experts in those domains, think that that's not possible. But we will see. So we're recording this the week after the GPT-5 launch. And for many people, both kind of experts, high-level people, as well as kind of the, you know, unwashed masses, so to speak, you know, thought that GPT-5 would be this big watershed moment in intelligence. And I think the consensus is that we're not really seeing that. Like, how do you, does that play at all into, like, how did you receive that launch? Like, and how did it play into your timeline? And like, and I guess maybe a broader issue is like, is there like, you know, how do you think about like the moving of goalposts and all that kind of stuff? Yeah. You know, going back to your thought about verifiable versus unverifiable statements. So I tried it myself and first I tried it there, not like the perfect way. So for example, you should just go there and then you just say, okay, answer me some questions. I mean, it was clearly lackluster because it didn't use the thinking, thinking option, which is kind of like necessary for high quality answer. So he just did very, very stupid mistakes, which is a bit like, kind of, I don't know why they did that. I mean, reputation-wise, it's not very good that you go there and then you get bad answers. You don't know why. If you try the high-effort versions, then they do pretty decently. and it's really starting to get really hard to actually understand the AI in terms of how well it would perform on really tough questions because those questions are getting harder and harder to come by. A question that is not on the internet so we can be sure that it really figured out something not just remembering it. so what we did we tried to use GPT-5 in some of our agents and what we found is that it's a bit subversive so basically it was like when you ask proving things then it introduced new axioms so basically make sure that it'll prove it based on things it made up yeah so basically introducing new axioms saying that just believe this it's like and that's not nice I mean and so and basically it tried to figure out loopholes how to how it can pass or approving so so basically how it can play the environment which is a bit scary but I mean also impressive at the same time that it it does that but on the other hand it's it's it's not what you want And that, I think, highlights the importance of verified intelligence, that you don't want your AI to be playing. So basically, if you are training the AI on problems where the verifier has a lot of loopholes like another AI, then I think you necessarily get into these kind of problems. And what he found is that other AIs were much less subversive than GP25. So yeah, I'm not sure if it gets into this. But yeah, I think regardless, I think it's a step forward. So I think that the reasoning ability is improving. And I think it's, I'm still believing that my timeline, I mean, if you look at the rate of progress, then things come out every once. and it's like the pace of improvements is accelerating. So I think that we will certainly see, like not like, I don't think you can expect an AI to be like suddenly human level in everything and then basically like as flexible as a human on every respect, but you will see like this idiot someone AI that is like super good at mass or being able to suddenly create new physics or new mathematics, etc. And that's what I really believe in. We will see this kind of AI emerging next year. I'm thinking about the challenges that you alluded to with benchmarking, meaning what questions do we have that aren't on the internet. That becomes particularly difficult when we're talking about benchmarking the creation of new knowledge. is it are we left only with you know we'll know it when we see it we will have to benchmark on what what kind of problems can it solve that humans couldn't solve so that's the real question and and that's kind of like a benchmark it's not a traditional benchmark that you get like 80 or 90 percent or something but you say okay now my ai proved the rima hypothesis so that's it it must be good. So I think that there is a way of making AI more measurable, even in the new knowledge. I have some ideas around that. So basically what I believe is that we have to create a kind of like a market for knowledge and it's kind of similar to a stock market where you are giving credit for solving something new or like creating a new connection or solving an old problem. And that way if you will unleash an AI agent, then you can measure it, how much credit it creates in that market. So I think that this new market... So kind of an implicit reward function, you know, that's economically based. Yeah, it's basically based on mechanism design. That's called like that. So human markets work that way, that you get some reward, like you get money for doing some economically useful activity. That's how we measure humans. I mean, you can discuss, I mean, It's disputable how well this market rewards actual output. But yeah, if we decide that system reasonable, then I think we could measure the AI's progress even on domains that are open-ended and not just like a fixed set of problems that once the next AI comes out, it's already public. So that might have been trained on it. So that doesn't work anymore. So that has been a problem with benchmarking AI for the past three, four years, where everybody trains on everything, and then you don't know which benchmark they train on, basically. So I think it really should move to kind of like a more forward-looking, open-ended benchmark that just measures the output of new stuff rather than like back. So this kind of testing on older things. So they are much less reliable in my opinion. And now the AI really gets to the point where it will be able to create new knowledge and that's what we need to measure. Besides the work that you're focused on, what else really excites you in terms of pushing the field forward? Yeah, I think I thought a lot about what I should do if mathematics is really solved. And I think that's in a year or two. And I think that the most interesting thing for me personally is to create... So an AI that helps understand humans better. So basically helps understand me, myself. So can we create an AI that does not just like acts like a body and then it just gives you like feel good answers, but actually challenges you and tries to make you understand yourself. So basically an AI that helps you discover the depths of human beings, the depths of human intellect or even spirituality in a sense. So I think that would be a really groundbreaking thing that once we saw sciences, then we start understanding the humans, how humans work, what makes us happy, what is life about, what is the purpose, etc. All of these things. And I think if we apply AI in a bad way, then we can end up in a dystopian society where AI just pushes you like video clips that keeps you slightly entertained. Or it could be an AI that challenges you, makes you a better and better human being and allows you to move up in a deeper manner. So basically helps humans to really improve themselves at their core. And I think that there is a real danger that we will misuse the AI so that it becomes a drug rather than a help. And I mean, I'm not really sure what will happen, but I'm a bit afraid about the future because it's already AI dominates a lot of YouTube recommendations or social networks, et cetera. And AI can become like a dividing factor that everybody puts in their own bubble and then just pushes things that pushes your buttons all the time just to extract money out of you by advertising it. So that's the dystopian future. and a real nice future would be that AI really is a deeply one to help you. And it designed the purpose to elevate everybody. And that's what I would be more excited to see happening. To what extent do you feel like that AI that understands humans needs to or would incorporate kind of the mathematical formalism that you're working on today? Like, understanding humans feels like kind of a soft thing, and the current LLMs can fake it pretty well. But do you feel like the mathematical side of things makes that better? Or is it a different direction? I don't want AI to understand us necessarily. I just want AI to help us understand ourselves better. But I also think mathematics is super powerful and much more powerful than we believe. And I think that a lot of the facts that we know about humans are not mathematized enough. So we don't really, don't really see the actual numbers or the actual rules. So of course, a lot of people try to figure out those rules for thousands of years, but I mean, they were never really like scientifically tested. So I think that there is a potential there for sure, for more scientific methods. And if we have like super strong mathematician and statistician and AI that can actually like dig into the data and find hidden connections and hidden rules and patterns in large data sets, then they can give us new insights for sure. I think that humans, I don't just want humans to get some feel-good answers from the AI that act like a good friend to you, but much more like an AI that actually figures out the hard truths as well that you don't like necessarily, but true about humans. So that's what I really believe what we need is the real truth, not like just some pretending and making people feel better. We need to make people feel maybe inconvenient sometimes, but challenge them to come to improve themselves and get to the next level. You're absolutely right, Christian. just teasing Claude here I certainly agree thank you awesome well this has been a fascinating conversation and I've really enjoyed learning it a bit about the way you think about the field and your research. Thanks so much for jumping on and sharing a bit about what you've been working on. It was my pleasure. So thanks a lot. Thank you so much. you