AI and the Future of Math, with DeepMind’s AlphaProof Team

0:05Hi, listeners, and welcome to KnowPriors. Today, we have Thomas Hubert, Rishi Mehta,

0:23and mathematical reasoning. In today's episode, we'll explore how AlphaProof works, its implications for math and AI, more about Test Time RL, and what this reveals about machine learning's capability to reason rigorously. Really happy to have you guys. Welcome. Thank you for having us. Yeah. Maybe you can start by just talking a little bit about your backgrounds and how you came to be working on AlphaProof together. I'm Rishi. I was one of the tech leads on AlphaProof. I've been working in computer science and machine learning for a while. I'm a chess player, and I came across the AlphaZero paper and saw some of the chess games that that agent produced.

0:59And I found it really inspiring. And I thought, like, this is the kind of thing I need to work on. Coming up with something beautiful and superhuman and almost alien felt magical. I came over to DeepMind and the AlphaZero team, which Thomas was leading, was working on math. And that's how I got into math. That's my background. So, yeah, I started working in industry in my early career. I worked on the many detection computer networks. I worked on ad targeting and switched to AI research. And there, a constant interest of mine has been systems that can spend more computes to either tackle harder problems or to think more.

1:39And math seemed to be a perfect domain for that. Yeah, on my side, I was actually a Go player. So instead of doing programming since the age of 10, I was actually playing Goal. And I played a lot of Goal during my youth. And then at some point, it was also my dad's dream to build a computer Goal program. And so I was kind of figuring out, like, what do I need to know to be able to build a computer Goal program? And then I realized that maybe it was being built at that time. And so that's how I discovered DeepMind and how I discovered AGI. And that's how I joined the company and have been kind of involved with AlphaGo and AlphaZero, MuZero, this line of work.

2:21And recently we had worked on AlphaCode and AlphaTensor. So, you know, like that's way before ChatGPT, but we already knew that Transformers were kind of changing a little bit how things were done. And so we, you know, I found that in Mathias you could get this perfect verifiability and with AlphaCode we realized we can generate a lot of good code. And so it was very natural at that time to think about the potential there was for mathematics. Can you contrast? So maybe just as context, like for any listener who wasn't a super cool mathlete like me, IMO is the sort of oldest and most prestigious math competition for young people.

3:03There's a set of six problems. They feel impossibly hard. And AlphaProof had this really amazing results of solving four of the six problems this year. Can you talk a little bit about math and the IMO in particular as a problem relative to game playing and other search problems like chess? I think, you know, like first there is a big difference is that in board games you play against someone. And that's a lot of fun in the board games. And for instance, when we did this AlphaGo or AlphaZero algorithms, we could really have this thing about self-play. You could always play against someone who is exactly just your strengths.

3:43And that proved to be a powerful idea. When you're kind of trying to learn to do math, in some sense, you know, you don't really have an opponent. You just have to think about it. And math is a bit special in the sense that it's like, it's almost like a purely cognitive kind of thing where you can just, you know, the only thing you can do is to think more. You know, maybe you can't really go into the real world and run an experiment. And I guess mathematicians says that, you know, sometimes it's a good thing to take a nap and let your unconscious self kind of think about the problem. And that's a good way to come up with new ideas.

4:16It's a lot about thinking. And so, you know, like when you're confronted with a really hard problem, there's a whole question about how do you go and try to solve it. Maybe this is a good time to ask you to describe for our listeners, most of whom are technical or somewhere in the tech field, but also a broader business audience. And it's like, you know, how does AlphaProof work overall architecturally? Yes, sure. So AlphaProof is based on this thing called AlphaZero. So maybe let me start there. AlphaZero has this program we developed to, you know, like be basically kind of solve kind of perfect information board games.

4:51And the way it works is it's also based on a reinforcement learning algorithm. So you can think of AlphaZero as maybe three components, like one, a neural network, two, kind of large-scale rate for smart learning, basically learning from trial and errors. And three, it also has like this planning and kind of search component to it to try to, given the current situation, trying to search for kind of the best answer. And it turned out that, you know, like maybe we weren't very imagining that when we were doing chess, but if you can handle kind of infinite action spaces, then, you know, instead of kind of looking for a chess move, you can look for, for instance, a line of a proof.

5:32And so that's what we tried to do when we started off a proof. It's basically, can we look, can we, our action space is to generate lines of proofs. And maybe very importantly, we used a formal language to do that. So basically another way to say that is we use kind of code to write maths and it's become quite popular recently. And the advantage of that is that once kind of the proof is complete, then you know the machine would give you a signal back to say yes your proof is correct or not and so we could search for kind of correct proofs once we find a correct proof we can learn from it and get a better neural network and kind of go into this self-improving loop of tackling harder and harder problems and learning more and more about mass so at a very high level picture that's kind of how it works and how kind of the ideas behind offer zero are adapted to to do mass one One of the things that was an interesting tidbit from your announcement was, you know, there's a series of problems, solves one problem within minutes, three days to solve other problems.

6:36Is there a way you can characterize like the search space for math overall or what alpha proof is better at in terms of domains than others, like types of reasoning within math? The search space in math is quite large compared to like something like chess or other board games. So, you know, some people might think of writing math proofs as like picking from a bag of known tricks at each step. But in fact, like there are many proofs where like you've got to come up with some non-trivial constructions, like you've got to invent a function out of thin air or you've got to like come up with like some way to manipulate.

7:11Even if you're just rewriting an expression, you can rewrite it in infinite ways. And there's only like a few ways you could rewrite it to actually make progress on the proof. Sometimes thinking about some novel problem requires decades of theory building and approaching it from an entirely new perspective to arrive at the angle that helps you solve it. And so in that sense, the reason why there are a lot of math problems that are very simple to state but have stood the test of time in that they've been unsolved for centuries even is that the search space is not easy to navigate in most cases.

7:45I think what AlphaProof is good at amongst the IMO categories is it's largely good. So the IMO problems have come in four categories. So there's algebra, number theory, combinatrix, and geometry. The two that it's strongest at are algebra and number theory. It's relatively weaker at combinatrix, although it can do quite good at some IMO combinatrix problems. And we didn't apply it at geometry at this year's contest. and one of the ways in which it navigates this massive search space is via an idea that we came up with which we call test time RL. So this is an idea where like let's say you're confronted with a problem that you don't know how to solve and you can do some search with what you know right now and you're not able to find a proof to it.

8:32What the agent then does is it constructs many variations of the problem in the vicinity of that problem and attempts to solve all of them. And if it manages to solve any of them, it learns from that experience and sort of comes closer and closer to solving the original problem. And you can think of this as like when confronted with a new scientific problem, many of your priors that you've developed from other problems may not directly apply to it. And so you've got to do like very bespoke experiments on this problem itself to learn something about it. And then he'll climb your way towards the solution of this problem.

9:06And so this process kind of mimics that. And so when you talk about, you know, these like the problems that are solved out of three days, like these are the problems that had this in this loop of like, we can't solve it with the base network, but we propose many, many variations. We try all of them. We get slightly better, slightly better, slightly better. And then we hill climb our way to the final solution after like days of inference time compute. Or what are the limitations or approaches to scaling or, you know, increasing the set of problems that alpha proof can solve? And I guess there's two dimensions to that.

9:37To your point, there's a set of areas where it already does quite well, algebra and other areas. And then there's a set of areas where you may need new forms of training data or other things like certain aspects of geometry or potentially other areas of mathematics. I'm a little bit curious how you think about what is necessary to increase performance dramatically from here. And obviously what you've done is incredibly impressive. I'm just sort of curious like how you think about what are the obstacles to future growth? Maybe the main thing that AlphaProof doesn't do is theory building. It doesn't matter to the theories.

10:11AlphaProof and the equipment, number theory, wouldn't be able to come up with the complex analysis necessary to derive results in number theory. So it's one of the main things that we don't even, and we generate variants and get better by solving these and that enables us to tackle the original problems of interest. Theory building is a component that is, that would be required to go further. Maybe another dimension, some problems like combinatorics can be stated in a somewhat obfuscated manner. That doesn't mean that all combinatorics problems, And just as a reminder, commune-otherics problems are all about counting the number of things.

10:59For instance, if you have 40 socks in a drawer, how many pairs do you have? It can be stated in some obfuscated way and how to translate them in lean is a major difficulty and then how to solve them in lean is a bit unwieldy. How to best cycle this is still an open question. I think there is a link a little bit to your theory building because, for instance, you know, So if there were, in some sense, part of the difficulty comes from the fact that the tools you need to express those things don't actually exist currently in the library that we're using. And so for instance, if you had like some kind of things that expressed, you know, what is an agent, what is an environment, what is a strategy?

11:41Then for instance, some, most of the, you know, a lot of the combinatorics problems would be much easier to state. But because that doesn't exist at the moment, in some sense, kind of the auto-formalization would need to kind of come up with all these things beforehand before actually kind of formalizing the problem. And so that's kind of, maybe that's kind of linked to the fact that, you know, at some point you will need to be able to develop new definitions, new mathematical objects, kind of come up with their properties and their proofs, et cetera, et cetera. So I guess, I think it was 1900 when David Hilbert posed his famous 23 problems that kind of defined a lot of the big areas that at the time he felt were important to mathematics and the sort of unsolved things that were important or topical.

12:22Or is there some Turing test equivalent, I guess, as a generic question? It's an excellent question. That totally defined kind of, you know, like the mathematics in the 20th century and maybe, you know, the millennium problems, you know, the seven millennium problems of which, you know, one has been solved so far is another attempt at defining kind of what, you know, what could be one trajectory of mathematics for the 21st century. What are our chances of solving that? That's like a really hard question because we know, you know, our brain kind of thinks linearly, but we know from our experience in working on the AI that we should actually try to think exponentially.

13:04Things might change pretty quickly. At the same time, you know, I think we have no idea how hard maybe something like the Riemann hypothesis is. Is it two orders of magnitude, three orders? Maybe it is like 10 orders of magnitude away from what we can do, right? Because we don't have an existence kind of proof. It's much harder to kind of have an estimate of how hard this actually is. But I imagine that solving that problem will involve like kind of creating brand new math, brand new theories and things like this. So if we want to take out a proof all the way there, I think that's a capability we need to, either it emerges, it's possible because, you know, like to prove harder problems, you start to need to be able to introduce this new kind of mathematical objects to decompose the problem in some problems.

13:54And we see that already happening for the IMO at a small scale. But it's very possible that it could emerge from just trying to solve problems or potentially, you know, we have to kind of explicitly think more about what does it mean to build theories and how can we encourage our folks to do these kind of things. Yeah, just for our listener friends who don't spend as much time on the unsolved math problems, just to contextualize a little bit, the Riemann hypothesis is it essentially predicts that prime numbers follow a specific pattern like distribution, and it has important implications. Maybe we can go from there to thinking a little bit about when you were working, beginning to work on math as a search space, there are like lots of interesting hypotheses for like why go work on math at all.

14:44One is like the field itself. Right. And so be curious if any of you have problems you want to work on. Another is the premise that this sort of advancement in reasoning will transfer to other domains, be they science or what we think of as more language-based, less verifiable non-code, non -rules-based domains as well. Where do you all want to take this? I'm not really a mathematician, so I didn't have a problem I absolutely wanted to solve. But it's been my favorite subject when I was a student. And I think you're absolutely right. there are like, you know, at least two kind of main reasons why you would want to potentially spend a lot of time on math.

15:27One is that, I guess, it's been described as the language of the universe. And, you know, it's been extremely powerful to both, you know, describe and predict the natural world and of course, to shape it. And you see that, you know, basically, we see math being at the core of all the technology we're using now. So kind of having a good understanding of math is probably kind of very important to understand our current world. And then, of course, you could, as you alluded to, make an argument that, you know, kind of solving math or, you know, like, which requires, you know, reasoning, generalization, abstraction, all these things that we think about when we're talking about something like a cognitive HGI would be, would be, it is a path to, you know, go towards HGI and that could really help in kind of the development of HGI.

16:15So I think at least for me, you know, these are maybe the two main reasons as to, you know, why mass is a particular interesting, you know, topic to try to solve in a general way, even though, you know, like mass, okay, let's say it's still kind of a constrained domain, but with kind of unbounded complexity and actually it's representing a lot of stuff. but it might be worse kind of making a really kind of focused effort on it because of all the potential implications it might have. I can add something about my own motivation. I've always been interested in the question of making systems that get better by thinking more.

16:57I looked at this in mesh translation and text diffusion and navigating agents that discover the environment and where they do better by thinking more. math seems to be, in particular, proving statement, so the core of AlphaProve, seems to be one of the last big challenge domains where AI still had a long way to go. And one of the key ingredients would be figuring out a way of thinking more. So that can be searching more, that can be a test material, and maybe the next step of thinking more will be thinking so much of the agent comes up with its own theories. So math as a test bed for thinking more was my motivation.

17:41One of the big reasons to perceive HCI at all is to uncover the secrets of the universe, the deep questions of why do things work the way they do and why are we here and why am I conscious and what's going on? And I guess solving these pure math problems, it feels like one domain where we're already... There's a large number of people who are already just doing this. They're seeing math as a search for truth. like, you know, people are pursuing these problems, not because they have any applications often, but more that it's like, you know, what, what actually is the answer? Why, why does this thing work this way?

18:13Something like you in solving the Riemann hypothesis feels like it has the flavor of like, you know, a sort of pure search for truth, which is just quite appealing. I guess like related to that, you know, there's a long history in mathematics of people or in science in general, or science and mathematics of doing things for their own sake or for the pursuit of knowledge for its own sake. And Sarah mentioned as an example, number theory and its applications in cryptography, zero-knowledge proofs are propping up in different ways in cryptocurrencies. Group theory and algebra propped up in quantum mechanics over time and was developed beforehand and then applied and developed further there.

18:50Are there specific areas that you're most excited about from an applications area for some of the work that you're doing, or is it mainly doing it for the love of the theoretical part of it? It's a good question. I think we can, maybe, you know, maybe the answer depends on each one of us. I think one thing that I'd be motivated about is to learn from mathematicians, you know, what they are interested in and what they find interesting in the current, you know, world of mathematics. And so, for instance, you know, I've been reading about this thing called Langlang's program that is trying to connect different areas of math.

19:24And it was described to me a little bit as kind of, you know, just like in physics, where you're trying to look for this unified theory of physics. It's like trying this unified theory of mathematics, where maybe, you know, we have number theory here and we have like geometry there. And, and, but maybe there is kind of something behind that, you know, that is more unifying. So I personally like those abstract ideas, even though maybe I don't understand them very well. But yeah, I'd be very motivated to just see what mathematicians care about and they might disagree between themselves as well. I think they would disagree, right?

20:01Like if you look at the historical examples, like when von Belly starts working on imaginary numbers, he gets completely ridiculed by, I don't know, the more important mathematicians at the time. And like many years later, we get alternating current and the ability to describe electricity. And so I think it's really interesting as a question. Like if you have the machine, the machine is able to develop its own theorems, like where do you point it for interest or usefulness eventually? It's a really big question. To that, one domain I'm particularly excited is code verification. That is at the moment when we write software, we write the code and we write tests.

20:38And when the tests pass, we are reasonably happy. Every once in a while, bugs that pass the test or even security issues. It would be much better if we could express in code the properties that the algorithm is supposed to verify and to prove in code that the algorithm does verify these properties. So it's already done for very critical domain like Avionics cryptography, where it's very important. It has to be done by humans. I think the software industry would be in a much better place if verification was much more common. And if we remove the bottleneck, which is humans writing those proofs.

21:17So if humans could be enabled by specialized tools, we could handle the minishare of these proofs. I think we'd have done a major step for us. I think another application area I'm excited about is the transfer of this technology to many other domains. So there are two kinds of players. One is just the transfer of the mathematical reasoning skill that this agent acquires via this kind of training to many other domains. And as we see, math is critical for engineering and science and you name it. But also, some of the tech we developed here of scaling RL and figuring out how to spend a lot of inference time compute, stuff like this feels like it's quite generally applicable to many other problems.

22:00I'm going to ask a question that is more conjecture, right? We've been talking about math and code and domains which are not easily formalizable, but are formalizable and verifiable. How much do you think this applies in the language domain? Can NAI make something funnier and it's easier to tell if something is funny than to write a good stand-up set, right? Right. And so I think it's kind of an instructive example, but like, do you have any intuition for how to take some of these learnings around the ability to verify correctness or quality, you know, within the RL approach? I guess, you know, so as you said, you know, there are domains where there is a ground truth and there are domains where there aren't any ground truth.

22:53And so when, when they aren't, and you know, like for instance, funny is probably kind of, you know, a human kind of, it's a, it's a fuzzy human concept. And maybe there were kind of aliens out there and they would have a different sense of humor. And so for those kinds of problems, I think that, you know, the only way you can kind of get your grounding is through like the, the humans are your grounding. For other domains, maybe the real world is some sort of grounding and then you have to go to the real world to get your grounding. But basically the kind of the RL would allow you to say, well, you know, like where does my reward come from?

23:32I guess sometimes it comes from the real world. Sometimes you can perfectly round it and sometimes the reward comes from the human. And I think that's fine. There are some techniques basically that we developed in the sense that, you know, of course, when you can kind of machine check things, you can run at a scale that is quite different from, you know, if you have to ask humans in general, even though we are quite a lot of humans. So there's still probably quite a lot of scaling that is possible, especially for things like this, where, you know, like humor, where you could, you know, everyone should have a say about what is funny or not.

24:08So definitely, you know, for instance, the RL framework, I think is still a great framework to think about those questions. And part of, you know, what makes RL work, that should kind of also transfer. And maybe the things where we rely on buffer verification, that's maybe that wouldn't transfer to that particular question. Where is there room for, I suppose, like human rating or input in terms of the explicit description or labeling of their reasoning? in domains that are more verifiable, right? Like if you have unlimited access to Terry Tao to do labeling for you, is that useful? Or, you know, how should we think of that versus like just do more search and work on better formalization?

24:56The way AlphaProof currency operates there is that it discovers its own truths and when they are valid, it learns from them and develop its own style, which has been commented upon as looking, Yeah, quite, quite alien. So with unlimited access to Territah, I would create proofs that are correct with some niceness as perceived by this human. And we could start optimizing amongst the set of valid proofs towards proofs that look nice for purposes of interpretability, for purposes of teaching. So there's definitely still room in this space of valid proofs that humans might prefer. That's actually like a pretty damning statement to some degree, right?

25:47Because it's just like preference versus perhaps like, you know, capability advancement. Like, what do I care if the proof looks alien, if we have new knowledge? Interpretability seems useful in this case, but... Yes, I'm saying that's the only angle for sure. With more supervised data, we can avoid the exploration problem and we could translate all the problems that are known to man. And that certainly would make the agent much better. That would save us years of compute for sure. I'm not saying that interpretability is the only way we could use a dog math translation for sure. but it could provide us a signal that we couldn't get otherwise presumably with time compute theory building we might be able to to maybe rediscover proofs that are already known.

26:44I think it's an interesting question because it like like it highlights the sort of complementarity of like specialist human data and like RL data and I think it's especially prominent with like LLMs where like LLMs have generated have these like very strong human priors because they're pre-trained on a lot of human data. But then when we do RL with them, they have an opportunity to take these human priors and build on them and, you know, develop their own styles of doing things like Afterproof has done. And I think one thing we've seen in this project is that often, like, the small amounts of precious human data can be really useful to, like, seed the agent's behavior and sort of, you know, get it from, like, a complete zero state to, like, somewhere much higher where it can play with the environment in a much more efficient way.