Unfamiliar Terrain

IBM, Avi Morse was a summer intern. >> Did you know that connection before this? >> I cannot disclose but I got a phone from Avi today but he had an amazing time as an intern of Robohub. So, let's welcome Robohub. >> Thanks. Can you hear me? Yeah. Good. All right. So, so let me join everyone in wishing Avi a happy birthday. I'm going to begin with the puzzle and it's a puzzle for all of you with the exception of Avi who's not allowed to answer. So, so imagine you're in this large warehouse. Think of it as a square room. You're at this corner. Your goal is to get to the middle and there's these tall rectangular obstacles and you can think of these obstacles as opaque. They're all they all have integer dimensions and sit on integer coordinates. If two obstacles are touching, you can squeeze between them. So, there's no non-convexity. Okay? And the distance from S to T is about N. And I'm asking you to give me an Oh, and and there's no map. You're feeling your way around. All right? I'm asking you to give the robot means for getting from here to here, finding a path of no more than N to the three hubs. You can actually do better. But that's the warm-up exercise I'll leave you with here. And so, in some sense, the the metaphor here is you're in unfamiliar territory. Terrain you don't have a map. You have to find your way. And it's sort of intriguing that if you had to go in the other direction from T to S, there's a fairly trivial greedy way of doing it to distance about N. Right? You just keep going south and west as much as you can. Okay? But it turns out the other direction is not so so easy. All right. So, so I began by saying unfamiliar terrain and at least half a dozen people have asked me what I meant by this title and it's it's a bit of a personal reflection because I find myself in unfamiliar terrain in a few different ways professionally. Right. And this, you know, I I pose this as a somewhat rhetorical question. Does AI help us prove theorems? I've been in the business of proving theorems, but I've never been in the business of theorem proving. And uh can we use machines to prove theorems? That's not a topic I've thought much about. So, I'm going to describe our experience using a code mutation agent from Google DeepMind proving some results in theory. Uh to set the stage a little bit, this tool that we use called Alpha Evolve is now about 2-year-old technology. So, this is not state of the art. And in fact, we're in the midst of moving to something more modern. Uh I'll go through the results in a little more detail in a moment. But, part of what I want to do is try and re you know, reflect. We had these small successes. Uh in all cases, they're problems that have stood the test of time. These are not things that nobody happened to notice. Right? And and then what what indispensable role did AI play? That's kind of what I'm trying to figure out. Okay? Um Okay. So, so we're not asking was AI help used to help prove some math problem. The answer is a resounding yes. There's plenty of evidence that people found inspiration from partnering with models in various ways. Uh some months ago, Tony Fang and company wrote this paper which I thought had a wonderfully honest line in it. It said the the successes they had in some of these problems owed to the obscurity rather than the difficulty of the problems. Okay? And and that set me thinking, okay. Uh so so what is really going on? Uh a few months later, you have a paper like this one. And when you read this paper by Shastri, uh, it's a problem that's been thought about a fair bit by a lot of smart people. Uh, if you read what he presents, uh, it's fair to say that it was not a completely autonomous AI that did this, but still large fragments of the proof, the critical portions, did come from AI. So, this is a bit more inspiring. Uh, right? And then the this announcement, of course, very striking announcement from OpenAI last week, which says that, uh, for the unit distance problem, uh, you have a lower bound of n to the 1 plus delta unit distances realizable on the plane, okay? And And this is as far as we can tell, a completely autonomous. So, they even give the prompt, you put the prompt in some system, which is presumably not some stock model, uh, and out came, after 125 pages of thinking traces, uh, a proof, uh, of n to the 1 plus delta as a lower bound in the number of unit distances, okay? And this is, uh, uh, a striking in my mind, a landmark step, uh, in the area. Okay. So, so let me, uh, now tell you what we've been doing for the last year or so, uh, with this tool, uh, uh, uh, Alpha Evolve. And then I'll, uh, close up with some reflections on what seems to be going on and what doesn't seem to be going on, okay? So, so what's Alpha Evolve? It's The idea is you as a user go tell an LLM that you're looking for some object which is part of a proof, okay? That's going to be the motif, right? Um, and what the LLM does, it spits out a fleet of programs, okay? And these programs are going to generate the objects in question, okay? Uh, for instance, the in one of the results, there'll be Ramanujan graphs of a certain with certain properties, okay? All right. And you score the objects and use that to back send back a score on the programs. The ones that seem to be doing a good job, you feed back into the LLM to generate new, evolved, fitter programs. And the rest, you trash them. Okay, so that's sort of the the schematic. Okay? All right. Uh so so we threw AlphaEvolve at a bunch of problems. So what were we able to do? Uh this is sort of a compressed list of the results we have. So let me try and go through a couple of them, right? Uh we have what seems to be the state-of-the-art result on the NP-hardness of approximating the traveling salesman problem, okay? We get a ratio of 111 over 110. That means it's not really NP-hard to solve the metric traveling salesman problem exactly. Even getting this approximation is hard, which is an improvement on a prior result. And if you've not worked in this area, I know you'll squint at it to say is it really an improvement? Yes, it is. Uh and if you're wondering is it really hard, I'll say ask Santosh. He worked for several years on this problem. It's always nice uh if you can point to somebody in the audience and say you know it's hard, don't you? Uh in this case, uh Santosh, right? Uh likewise for cutting a graph into four pieces, we improved on a previous thing uh result by 0.1%. Uh we also have results on max cut on random regular graphs. Uh essentially saying that you're not going to get closer than about 5% on average. Okay? Uh we demonstrate essentially matching analytical upper bound. So this is obtained by AI this analytically, and the gap is minuscule. So this is a case where AI helped us close off a gap essentially. Okay? We have similar results on maximum uh independent set. And I'll give you a little bit of a flavor of how these things work. Uh the worst-case results what we did was we fashioned proofs, reductions, and in them we found improved gadgets. Okay? Um for the average case results, uh it required constructing some neural magic graphs. So, so let me uh uh uh give you uh a hint of how this works. So, let me start with the TSP. The TSP is the one where we had to do the most human work before we could even bring in the machine. We had to refactor several existing proofs including paper Santosh's paper, try and get it to a point where you could essentially view the proof as a long string. Um in the middle there's a gadget and we used Alpha Evolve, the machine that I just showed you, to come up with a better gadget. Okay. Um there's a couple of things I'll point out about this gadget. Number one, it's not massive. Okay, it's it's like 110 nodes. And so, you could even say, "Well, if an oracle told you it was this small, couldn't you have just enumerated every graph?" Uh and the answer is almost true except there's weights in some of the edges, so it gets a little more complicated, right? Uh the second thing is One thing that struck us, unlike the previous proofs, this gadget is intrinsically asymmetric. Okay, and and I'll come back to why this is intriguing later. Yeah. Let me briefly touch uh on some a couple of other things. So, the idea of mechanically generating gadgets is not actually new. There's a paper from almost 30 years ago uh due to Trevisan et al. Uh and I'd never read this paper even though it was work happening in my group at IBM. Uh I kind of ignored it back then, but uh when I started doing this work uh uh I was drawn to this paper. And they used linear programming to generate simpler results. Uh not quite matching this, but on a large number of problems. So, at that time it was the first mechanical generation of gadgets that they that they provided. Yeah. Um Let me give you a hint of the max flow cut gadget turns out to be a little more complicated. So, this looks intimidating and in fact it is. It's a 19-node gadget. And edge weights go from 1 to 1429. So, a couple of remarks on that. One, it's not the kind of thing that you're probably going to come up with paper and pencil. Two, your suspicions will be aroused now saying, "Okay, how do we know this is correct?" Right, you're just showing me this nice picture. And I'll get to that point in the next slide. Okay. Because in any of these proofs, verification is hard. The fact that I'm only exercising a small portion of the proof and replacing it means I don't have to verify the whole thing. I just have to verify the the thing in the middle and the interface to the rest. Okay. And then for random graphs, Kunisky and Yu in Fox 24 had a construction where they had Ramanujan graphs of like 10 nodes. By blowing that up to hundreds of nodes, we were able to get all these other results. So, that's So, that's sort of the the program that we followed here. Okay. All right. So, now let me address how do we know it's correct because verification of these generated objects turns out to be critical, right? In pretty much all of these cases, you can do some sort of exhaustive verification and that can take hours to days. Okay. But, inasmuch as these things are fitting in proofs that you're checking and evolving, that's not feasible. It just takes too long. Okay. So, here's what we did. Um So, we used Alpha Evolve to write fast verifiers for these gadgets. So, So, for instance, in that case of the 19-node gadget, where every variable, every node could take on one of four colors, you you had this massive verification problem. And rather than exhaustively verifying it, we said to Alpha Evolve, "Find a fast verifier for this." And it did. And it would spit out this code and we would use Gemini to summarize it summarize it and it would say, "Well, I used this kind of branch and bound and then I do use this fast library in you know, whatever language and in practice this gave us enough of a speed that a typical verification would be like a second and so you could crank it through thousands of times. Okay. But then before we could claim a theorem we would still run the exhaustive verification at the end of the day end of several days to to actually claim the theorem because we couldn't afford to as far as I know these verifiers are not correct. I know they're fast. Okay. They're fast and they let us loop through quickly and get to our claimed result but before we claim the result we do the exhaustive verification. Okay. So all the Yeah, so so suppose I I you know, let's take a fairly clean problem, right? Count the number of 10 cliques in this graph. Okay. Well, the the naive way is to enumerate 10 subsets. Go to Alpha evolve and say you know, use whatever heuristic thing you want and I want you to be right pretty much all the time. And it's right on various test data sets. We use that pretending it's known to be correct because it's fast because each crank takes about a Yeah. In the inner loop but then at the end we still do an exhaustive Yes. Yeah, exactly. Right. And all I'm saying is I don't know those fast verifiers to be accurate. They worked. >> So but so do you know that they're that they're not accurate? >> No, I don't know. So on everything we've tried they've been accurate. >> When you ask when you ask Alpha evolve do you ask Alpha evolve to pass the test do you ask Alpha evolve to act to solve the problem and then test it and >> So so we generated large synthetic data set, and on that it regressed clearly. All right. So, we did use sloppy verification, and I think this is a powerful technique in sort of guiding the search along, but obviously not reliable for the end result. All right. So, so let me take stock of what we did. We We didn't prompt the LLM to generate gadgets. In fact, that didn't work well for us. It We evolved code using the LLM to generate the gadgets. Okay. This is a single-shot run, meaning it's not interactive where a human is sitting saying, "How about you try that? How about you try that?" It is you put in the start prompt, step back, and hours later you get something. All right. Um You remember I had this thing where the program was generating these gadgets, and they were being scored. That was a synthetic objective function. Okay. Uh it didn't really know it was proving a theorem in this case. I mean, "No" is a strong word, but you see there's no strong semantic notion of theorem proof. Right? It's generating graphs towards the proxy score function. Right. Um And And then I mentioned this sloppy verification. Okay. Uh let me get to the other domain that uh we use these techniques. Okay. So, so remember Ramsey numbers. Um so, given two positive integers R and S, uh a Ramsey number uh is you know, a graph with no R-clique or S-independent set. So, in general, we don't know how to find these things. Yeah, go ahead. >> Um just a quick question on the previous part of the talk. >> Yeah. >> Uh how were the problems for which you designed these gadgets chosen? Did it work for basically everything you tried or not? >> No. No. It didn't work for many things. Uh we picked TSP because it's a landmark problem, and we banged our heads on it for like 9 months. Uh On the way, we found MaxCut succumbed earlier. Uh and that gave us a lot of intuition, especially in the verification. But, really TSP is what we were shooting for. >> I see. Do you have uh intuition for what types of gadget constructions this would work for versus what it would not? >> So, it's a little complicated. Hold that question because as I walk you through this, you'll find that closely related problems can be harder or easier. Okay? All right. So, one way you can prove a lower bound on a small Ramsey number, as these things are called, is to exhibit a graph. So, if you could find a graph with 35 nodes with no four-clique or six independent set, you know that R(4,6) is at least 36, right? Uh, and so we went about searching for these counterexample graphs. Okay, they're called Ramsey graphs. Okay. Uh, so these are lower bounds, and here's a table. Uh, this is not entirely complete. I think this table is about 3 weeks old. We have a few more cells filled in now. Um, of Ramsey lower bounds found by AlphaEvolve. And I'll explain all the colors in just a second. Okay? So, for instance, it says that the lower bound for 4 and 12 that we found is 128. So, we found a 127-node graph that uh had no four-clique or 12 independent set. Okay. So, what all these colors mean? Uh, a blue cell is one where AlphaEvolve found a lower bound that matches the best known upper bound. And all of the blue cells are not new results. These were known results. We we simply reproduce the lower bound. Okay? Uh, a yellow cell is one where we matched the best known lower bound, but we still have headroom to the uh to the best known upper bound. So, we're still cranking away on some of these. Uh, and in these yellow cells, none of them is a new result. These are all matching existing results. Okay? The green cells are all new results, beating the known state of the art by anywhere from one to four uh in these cases. Okay? All right. Uh, now let me give you a little bit of a summary and glimpse of how this worked, right? So, one thing is we found and that touches on your question, every cell, even adjacent cells, uh had not just varying difficulty, the programs that worked for a particular cell often had nothing to do with the program that generated the graph for the very next cell, right? And these have to do for There are good reasons for this. One, it has to do with the relative number theoretic characteristics of R and S, okay? Uh so, there's no simple unification of the various algorithms uh other than the fact that the meta algorithm Alpha evolve is common to all, right? Uh in many cases, the thing is obviously they're using language models. It's not completely oblivious to background knowledge. So, it's seen everything that humans have done and would say, "Well, let me borrow this heuristic that this person wrote and this heuristic." And I'll give you a snapshot in a moment of one of these heuristics, right? Uh and in some cases, there was uh the early 2000s, there was a somewhat mysterious Russian project that actually published a whole bunch of Ramsey graphs without saying how they were generated. The so, the the lower bounds were correct, but we have no idea why they were true. So, we recovered those and we published uh the algorithms on on GitHub, right? Um So, we took the code for each in each case and then use Gemini to summarize it and I'm giving you just one picture, right? And if you read it, it actually is fairly literate. It says, "Well, I'm going to bootstrap with a cyclic graph, which is a very common starting point uh for Ramsey graphs. And then I'm going to iteratively expand uh and then I'm going to do something using max independent sets and finally use simulated annealing." So, it's chaining together in some sense known techniques, right? Uh In only one case to date, uh did it do something that we've seen no human do, okay? And this is a case where to find a Ramsey graph of a certain size, it overshot, found a bigger graph, and then threw away some nodes, uh which is a direction that humans had never done. It's not a difficult idea, but it was the first. Okay. So So, let me wrap up now. So, uh as original research results, I wouldn't claim that these are amazing, right? Uh uh they're intriguing. They're on time-tested problems. Uh it wasn't obvious how to solve them, right? Uh but what else are we learning? So, the use of AlphaFold today is very syntactic. It's not like it's doing intelligent reasoning about, you know, uh PCP reductions or anything like that, right? And one of the things we're doing now is to try to to build better models that have more of the semantics of the problem, right? Um So, then you say, "Okay, could couldn't a talented human uh have reproduced some of these results?" And uh it's very hard to argue no. I mean, if maybe if you jailed Andre Weil in a French jail, which I think they did, uh he could have come up with uh some of these things, right? Uh but so So, really the the two things it's standing on is these are problems that in some cases haven't been solved for decades, and then the question is when are they superseded by uh humans. Uh It's also the case that humans, typically when they're looking to cut a search space, will try and exploit symmetries in uh in the in the space. The TSP gadget notably did not have a symmetry. It actually exploited the asymmetry to get the result. Okay. Um if a smart person had been given comparable computing, uh could they have come up with it, right? And we looked at SAT solvers, SMT solvers, and all the math programming methods, and in some cases uh recognizing none of us is a great expert on math programming or SAT solvers. The number of constraints in these problems were 10 raised to over 300 and we got through. So, there is something happening. I'm not able to define it as okay, I can tell you exactly what AI did, but it doesn't seem to easily come from you know SAT solvers or computer algebra systems. There's a very intriguing note that I'd urge you to read by Alon Massel. He published it a few months ago where he basically says you cannot claim AI did this unless you can refute that claim. Okay. It's only a four-page note. It's sort of a philosophical argument and he has fairly strong views that in his opinion somewhat inflated claims are being made at the moment. Okay. There is one thing that AlphaZero seems to be accomplishing. This indirection going through generating programs seems to help. And in my sense, you know, it was like unleashing a fleet of smart research assistants who each understood Ramsey theory for instance quite well. But one of each one of them sat down or 10 of them sat down in a single cell and they focused and then one of them suddenly put up their hand and say, you know, I got a breakthrough, right? That's sort of the the way they're thinking traces in the models. Okay. I don't think this form of interaction where LLMs just evolve code to write proof fragments is the best and this is something that you know, it seems more than amply reaffirmed by the OpenAI breakthrough that was announced last week. Okay. We certainly couldn't through reasonable attempts directly prompt an LLM. In some case, the LLMs didn't even reconstruct the non-state-of-the-art. So, So, some of these problems have so far defied attempts to directly prompting, whereas going through this indirect route does help. Now, the one thing that for me is philosophically intriguing is that language models are trained on large amounts of data full of successes, right? But mathematicians, humans, embody a lot of knowledge of failures that doesn't really make it to language models. And bringing that, I think, will dramatically accelerate the capabilities of these systems. Right? Uh and and so, you know, there's a part of me that was reminded of a note 30 years ago by Bill Thurston, uh where he argues that as a mathematician, your job is not to just churn out theorems. Your job is to deepen human understanding, right? Uh and and I look at that and I certainly will not point to that 19 note gadget with all those weights and say that deepened human understanding of what's going on, right? Uh so so there is a real question of what this could look like. Like and, you know, I used Gemini to generate two potential alternate views of the proof of uh Fermat's Last Theorem, one which is a billion lines of Lean, uh which doesn't give you any insight, and the other was a nice graphic that talked about how, you know, the Wildt-Taniyama-Shimura connects uh through Ribet's work and Frey curves uh to finally uh get a contradiction. And there is something of this that uh I think is still missing and will probably even though we have these early successes. Right? Um and so, this brings me back to unfamiliar terrain because we now have a computing model that I feel kind of on shaky ground about. Um For all the prodigious feats, there are surprisingly elementary facts. So, for instance, one of the thing we uh found in a series of experiments is when you're adding two in integers, if on a digit, the sum is around nine or 10, language models, all of them, tend to get confused about the carry, okay? And you do enough of these experiments and you start to understand how the tokenization is done in each of the major models. It's kind of interesting, right? Uh and so, I'm used to programming computers in a way where I say, "Okay, uh if I add two numbers, I'll get the correct answer predictably. If I propagate a variable, propagates predictably. If I run a loop 50 times, it runs 50 times and not something else, right? Uh and in some sense, we are in a situation we are not able to declare invariants because we don't get a handle on the model of computing. There's even a workshop uh called I can't believe it's not better. Uh the Uh and it's it check it out. It's full of, you know, these uh Uh and yet, today most algorithms that we all experience are written by machines. Even before LLMs came along, machine learning made that uh de facto the case, right? So, the fact that we have incomplete guarantees uh leads us in a very strange place. Uh Until recently, I was responsible for the for Google's consumer products. And one of my last projects was to retool the search engine to have LLMs built into them. So, when you see these AI overviews things like that, that was the project I was responsible for. And I always felt very queasy about it because uh you know, it's very hard to make assertions about exactly what the thing is doing. And yet, you know, a lot of the time it seems to work and you know, users love it. In fact, one of the things you can measure, you users love it so much, they they increase their intensity of querying on the kinds of queries that LLMs answer. Okay? And that's observable and measurable, right? Uh and so, as we try and design a proof engine what is the invariant and and the next speaker John will actually talk about more reflections on okay if you don't have invariants what is it we can look forward to relying on and some of the experiences we've had and certainly you wouldn't think of building a controller for a nuclear power plant today using using LLMs you wouldn't abdecate your responsibility thus right So we are standing in this very uh exciting but fraught locale and I was reminded and close with this of a beautiful line at the end of Alan Turing's paper on the imitation game and it goes and he talks about you know different styles of learning but at the end he says we can only see see a short distance ahead but we can see plenty there that needs to be done. That I think summarizes where we are today. Thank you. >> Uh what about the puzzle? >> Thank you Adam. I thought nobody was going to ask what about the puzzle. Right. Uh so this is the puzzle right? So the robot has to get from here to here. Right? And find a path of length at most n over three hops and uh some in the summer of 1990 I gave this puzzle to an intern I had uh and uh Adam you want to come and explain it? You can Anyway. So so Adam cracked it and I'm going to give you sort of the hint of the solution and it is turning into paper that's uh please believe me it's deeper than the simple solution that give you right? So you're starting from S go to T uh drop something and and the the first thing you do is get over to a point at about root n comma root n and you pay about n cost in this and that's not hard. Okay. And then you do this sweep up until you match T on this coordinate and then sweep down here. And in the process, you can guarantee you'll end up in a point in a place that's advanced at least one of the coordinates by square root of n and paid no more than n. And you keep repeating this thing and you get n to the 3/2. Uh remember this? >> Yeah. Yeah. >> Okay. Uh and so this resulted I guess in our first paper together, which is STOC 1991. And uh I remember recounting this um morning what a painful referee we had who took 6 years to get it to into a journal. Uh and then it was only recently Alvin when I was looking through the references, uh I realized, you know, your secret motivation for this working on this problem. Uh Uh it is this money. I don't know if you remember this, uh but you had a paper with Dexter Kozen. And uh uh that was the thing. Okay, thank you. >> So, um did you find So, so one way that we, you know, often solve problems is