Autoformalization and Verifiable Superintelligence with Christian Szegedy - #745

34:55Today'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 ,000 steps, I think you said.

35:42I mean, I just said some number. I don't know. The order of magnitude, right? Yeah. But the idea being that, you know, 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, you know, 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 CRM's nowadays that human mathematicians care about, and they actually try to formalize it. Like Fitzmedalist Teritao has worked on this prime number CRM that talks about the distribution of prime numbers and gives an asymptotic estimate of that.

36:34And that was a very hard work. Like people worked on like 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 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 kinds of steps as well.

37:18And 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.

38:01and 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, or very few people accept it.

38:53They think, okay, there is a 30 % probability that it might be true, but most mathematicians thinks 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 this could be prevented when we are formalizing all of mathematics, but there's just a side effect. but I think once AI gets to the point that it knows all of human mathematics to maximum extent and it basically it will be like a much much better version of any human mathematician and then it can develop new mathematics 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.

40:04But 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 presumably some degree of automation in achieving that. Can you talk a little bit about the automation that was employed and how you see that kind of taking you to a broader ability to automate?

41:00So 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 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 used some AI automation but it's more like a copilot so it's it helps you autocomplete, but the mathematician always have to say, okay, I like this line of code, etc.

41:53So the automations we had is like, we're working with Jared Lichtman, who is a very established mathematician who is very knowledgeable about number theory. And he basically, he created, 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 easing, 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.

42:45alone. 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.

43:34So 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.

44:34So that's how it works. And is it a conventional AI in some sense or another? Like, is it LLM-based or is it? 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 like we can start to reason about this thing not knowing what it is by saying, well, you know, there's transformers, there's LLMs.

45:29those 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 like it's this whole new thing that we've not you know conceived of that you know you guys have invented it's again it depends on where do you draw the line between so i think i think i think it's i think it's i mean i think i i think a lot of people are impressed by they say, okay, we don't think. So impressed in the sense that when you show them, then they say, when you tell them that what you want, then they say, oh, that's not possible.

46:08And 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, yeah. 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.

46:58And I think once we collect 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. branched with this? Am I thinking about it correctly?

47:46I 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 have.

48:44So basically, we can develop these kinds of agents and run them much faster and much better than it could be done without the morph infrastructure. So that's an important component. So, yeah, but we have a lot of directions in parallel that is both opened by our approach and also important to have an open-ended improvement loop that can get to super intelligence, I think, in the fastest possible way. So that's the goal, is to get to a super intelligence 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.

49:29We are making this superintelligence safe by construction that we are only focusing on verifiable artifacts. Others focus on various objective functions, just like 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, like 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.

50:24You 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.

51:17how do you is it clear to you how that is melded with you know the linguistic and kind of world knowledge that the you know traditional approach brings or is it 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.

52:12So 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.

53:01And 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 things from 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 formal reasoning backbone comes from your research into verification and that understanding of kind of the human communication and natural language comes from the emphasis on validation.

54:09No, 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 we don't necessarily have to mess with that, in my opinion. Yeah, that's what I was going. It's like, you know, at some point, once your system is, it doesn't need to do everything. It will work in conjunction with conventional LLMs. But 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.

54:59So you can have a pre-trained model that is pre-trained with all the human communication, just like current telelabs. 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 bit more like concrete tool use to improve the depth and correctness of logical inferences.

55:54Excellent, 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, so even like very high-level people that I talk to and I see these 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,

56:38the current state of the art is... 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 or 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 AIs by end of next year.

57:46So 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?

58:33And like, and I guess maybe a broader issue is like, is there like, you know, How do you think about the moving of goalposts and all that kind of stuff? Going back to your thought about verifiable versus unverifiable statements. So I tried it myself. And first, I tried it not the perfect way. So for example, if you 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 option, which is kind of necessary for high-quality answers. So he just did very, very stupid mistakes, which is a bit like, kind of, I don't know why they did that.

59:14I 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 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 they don't 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 it 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.

1:00:59So 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. 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.

1:01:31But yeah, I think regardless, I think it's a step forward. So I think that the reasoning abilities are 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.

1:02:23And 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 like, you know, 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 kind of problems can it solve that humans couldn't solve. So that's the real question. And that's kind of like a benchmark. It's not a traditional benchmark that you get like 80 or 90 % or something, but you say, okay, now my AI proved a Riemann hypothesis, so it must be good.

1:03:10So 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.

1:03:53That'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 design that system reasonable, then I think we could measure the AI's progress even on domains that are open-ended not like just like, say, 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.

1:04:50So 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.

1:05:34And I think that the most interesting thing for me personally is to create 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 to make you understand yourself so basically an AI that helps you discover the depths of human basically 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 solve sciences, then we start understanding the humans, how humans work, what makes us happy, what is life about, what is the purpose, etc., all these things.

1:06:32And 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 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.

1:07:28And AI can become like a dividing factor that everybody puts in their own bubble and then just pushes like 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 the real nice future would be that AI really is a deeply one to help you. And it's 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 human, you know, understanding humans feels like kind of a soft thing and the current LLMs can fake it pretty well.

1:08:20But do you feel like that the mathematical side of things like 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 it's like 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 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 they were never really scientifically tested. So I think that there is a potential there for sure for more scientific methods.

1:09:11And if you have super strong mathematician and statistician and AI that can actually 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 that we need is the real truth, not like just some pretending and making people feel better.

1:10:02We 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.

1:10:20Just teasing Claude here. I certainly agree

1:10:30thank you

1:10:37awesome 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.