How AI Could Be A Mathematician's Co-Pilot by 2026 (Prof. Swarat Chaudhuri)

Professor Swarat Chaudhuri from the University of Texas at Austin and visiting researcher at Google DeepMind discusses breakthroughs in AI reasoning, theorem proving, and mathematical discovery. Chaudhuri explains his groundbreaking work on COPRA (a GPT-based prover agent), shares insights on neurosymbolic approaches to AI. Professor Swarat Chaudhuri: https://www.cs.utexas.edu/~swarat/ SPONSOR MESSAGES: CentML offers competitive pricing for GenAI model deployment, with flexible options to suit a wide range of models, from small to large-scale deployments. https://centml.ai/pricing/ Tufa AI Labs is a brand new research lab in Zurich started by Benjamin Crouzier focussed on ARC and AGI, they just acquired MindsAI - the current winners of the ARC challenge. Are you interested in working on ARC, or getting involved in their events? Goto https://tufalabs.ai/ TOC: [00:00:00] 0. Introduction / CentML ad, Tufa ad 1. AI Reasoning: From Language Models to Neurosymbolic Approaches [00:02:27] 1.1 Defining Reasoning in AI [00:09:51] 1.2 Limitations of Current Language Models [00:17:22] 1.3 Neuro-symbolic Approaches and Program Synthesis [00:24:59] 1.4 COPRA and In-Context Learning for Theorem Proving [00:34:39] 1.5 Symbolic Regression and LLM-Guided Abstraction 2. AI in Mathematics: Theorem Proving and Concept Discovery [00:43:37] 2.1 AI-Assisted Theorem Proving and Proof Verification [01:01:37] 2.2 Symbolic Regression and Concept Discovery in Mathematics [01:11:57] 2.3 Scaling and Modularizing Mathematical Proofs [01:21:53] 2.4 COPRA: In-Context Learning for Formal Theorem-Proving [01:28:22] 2.5 AI-driven theorem proving and mathematical discovery 3. Formal Methods and Challenges in AI Mathematics [01:30:42] 3.1 Formal proofs, empirical predicates, and uncertainty in AI mathematics [01:34:01] 3.2 Characteristics of good theoretical computer science research [01:39:16] 3.3 LLMs in theorem generation and proving [01:42:21] 3.4 Addressing contamination and concept learning in AI systems REFS: 00:04:58 The Chinese Room Argument, https://plato.stanford.edu/entries/chinese-room/ 00:11:42 Software 2.0, https://medium.com/@karpathy/software-2-0-a64152b37c35 00:11:57 Solving Olympiad Geometry Without Human Demonstrations, https://www.nature.com/articles/s41586-023-06747-5 00:13:26 Lean, https://lean-lang.org/ 00:15:43 A General Reinforcement Learning Algorithm That Masters Chess, Shogi, and Go Through Self-Play, https://www.science.org/doi/10.1126/science.aar6404 00:19:24 DreamCoder (Ellis et al., PLDI 2021), https://arxiv.org/abs/2006.08381 00:24:37 The Lambda Calculus, https://plato.stanford.edu/entries/lambda-calculus/ 00:26:43 Neural Sketch Learning for Conditional Program Generation, https://arxiv.org/pdf/1703.05698 00:28:08 Learning Differentiable Programs With Admissible Neural Heuristics, https://arxiv.org/abs/2007.12101 00:31:03 Symbolic Regression With a Learned Concept Library (Grayeli et al., NeurIPS 2024), https://arxiv.org/abs/2409.09359 00:41:30 Formal Verification of Parallel Programs, https://dl.acm.org/doi/10.1145/360248.360251 01:00:37 Training Compute-Optimal Large Language Models, https://arxiv.org/abs/2203.15556 01:18:19 Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, https://arxiv.org/abs/2201.11903 01:18:42 Draft, Sketch, and Prove: Guiding Formal Theorem Provers With Informal Proofs, https://arxiv.org/abs/2210.12283 01:19:49 Learning Formal Mathematics From Intrinsic Motivation, https://arxiv.org/pdf/2407.00695 01:20:19 An In-Context Learning Agent for Formal Theorem-Proving (Thakur et al., CoLM 2024), https://arxiv.org/pdf/2310.04353 01:23:58 Learning to Prove Theorems via Interacting With Proof Assistants, https://arxiv.org/abs/1905.09381 01:39:58 An In-Context Learning Agent for Formal Theorem-Proving (Thakur et al., CoLM 2024), https://arxiv.org/pdf/2310.04353 01:42:24 Programmatically Interpretable Reinforcement Learning (Verma et al., ICML 2018), https://arxiv.org/abs/1804.02477

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:00Speaker 00

  Neurosymbolic programming is this approach to artificial intelligence, where you are representing models using a mix of neural networks and classical symbolic code. You mentioned Alpha证, that's a great example. But I would say that even these agents that are generating some code using language model and then executing the code and then getting feedback and then using that to make further decisions. They are really doing something neurosymbolic as well, right? Because you are actually using a Python interpreter, which is a symbolic tool. Now, there is a universe where you have again an extremely low-level language, a sort of assembly language, and then you just let the machine figure out over time

• 0:45Speaker 00

  what kinds of abstractions are useful. And to me, that could have a lot of value because you could discover things that no human would ever imagine. And that could enable you potentially to do new kinds of math, new kinds of physics, new kinds of biology. And you are going to, you know, discover these higher-level building blocks. Yes, you know, no human has figured that out yet, but this AI has. But then you're using this building block to build parsimonious programs, models, that can do amazing things. And then you're just bootstrapping and you're building up this entirely new universe of mathematics and computation. I can imagine such a world.

• 1:25Tim Scarfe?

  MLST is sponsored by CentML, which is the model-serving platform for machine learning workloads. Now, you log into their platform. The first thing you see is the SAS option. So this is the really simple option, just like on OpenAI. You can send requests up, you stick your access token in there, and you can access all of the latest open-source models. And it's faster and it's cheaper. By the way, when you sign up, you get 10 free credits, which means you can do some experimentation without spending a penny. Also, watch the interview I did with Ganadi, their CEO, the other day. Enjoy.

• 1:59Tim Scarfe?

  MLST is sponsored by TwoFor AI Labs. This is a research lab started by Benjamin Krucia over in Zurich. They have just acquired Minds AI, the winners of the Art Challenge. Their sole purpose is trying to figure out AGI as quickly as possible, and they're looking at the Art Challenge in particular. If you're in Zurich and you want to join their monthly meetups, if you're interested in working for Ben as an ML researcher, reach out to him, go to twoforlabs.ai. Tuarat, welcome to MLST.

• 2:29Speaker 00

  Thank you very much. Thanks for having me.

• 2:30Tim Scarfe?

  It's so nice to have you here. Can you tell us about your background?

• 2:34Speaker 00

  I'm a professor of computer science at the University of Texas at Austin. And this year, I'm also a visiting researcher at Google DeepMind in London. My original research background is in symbolic methods for reasoning and programming languages. But over the last 10 years, I've also gotten very involved in machine learning. And these days, I'd say that I have a foot in on both sides, both symbolic methods and machine learning.

• 3:06Tim Scarfe?

  Wonderful. Now, we had a very interesting conversation in the car on the way over about reasoning.

• 3:12Speaker 00

  That's right.

• 3:12Tim Scarfe?

  What is reasoning?

• 3:14Speaker 00

  Well, to me, reasoning is, to some extent, in the eyes of the beholder. You know, it's one of those things that you know it when you see it. But I think that from the point of view of defining that in the AI context, it makes sense to have some criteria in mind. So what constitutes reasoning? So one of these is, in my mind, doing well at mathematical or programming or planning these kinds of tasks, right? That historically, people have associated with deeper thinking and reasoning.

• 3:53Speaker 00

  So I would say that if a system is performing better at those tasks compared to existing methods, then that's, I would say that it's doing, you know, it's showing improvement on reasoning. So I hesitate to say that a model either does or does not do reasoning, because to me, it's not a Boolean. It's really a quantitative measure. And you can see, you know, progress on this measure over time. Now, this is more about the what of it. You know, what does the model do in order to be in order for it to be doing reasoning? There's also the question of how, and I think that it's really useful to separate the how

• 4:35Speaker 00

  consideration from this because I think that there are many, many different methods for doing reasoning. We have seen some of them in the recent past gain prominence, but there are other kinds of methods as well.

• 4:48Tim Scarfe?

  Yeah, this is this is it, though. Do you think that it's, you know, like, some people are human chauvinists and they say that it's not really reasoning, the way we reason is better. John Searle was a famous example of this. You know, he argued that there was some complicated physical causation that can't easily be replicated in a machine. But we can agree that, you know, certainly in simulation, that there's a myriad of different ways we can make something behave as if it's reasoning. What's the difference?

• 5:17Speaker 00

  Right. So I think then, again, it's one of those things that we have to decide on our criteria. So if you have a system that takes a very large amount of compute in order to solve a very difficult mathematical problem, is that reasoning? Right? So by your definition, I think that that probably wouldn't count. But I think that, you know, one could argue that it's the end that matters, that if you're able to solve this hard math problem, then you're doing reasoning.

• 5:53Tim Scarfe?

  Well, yeah, I mean, there's also the robustness aspect of it because, for example, you could simulate something that happened in the physical world and you could reproduce the trace and you could say, well, it's the same thing, so why is it not reasoning? But but the real phenomenon would be able to reason in many, many different situations. And certainly with language models, when they are trained on specific types of reasoning, then, of course, they can generalize in that setting. But there are these holes in the Swiss cheese all over the place. So there's always this problem with test set contamination, isn't there?

• 6:29Speaker 00

  Yeah, so I think that then, you know, you have just named one additional criterion for a model to be doing reasoning, which is that you need to have this form of robustness. I would add to it, going back to the previous point, maybe computational budget is also a consideration if it takes you.

• 6:49Speaker 00

  You know, 5,000 hours of compute on a massive cluster in order to solve a math problem, maybe it's not exactly doing reasoning either, right? But to me, again, you have to decide what your definitions are, right? What your criteria are? And then you can talk about whether or not a system is making progress on those measures. Talking about a model is doing reasoning based on, you know, human-like behavior. To me, that's sort of a, it's a bit too ambiguous for my taste, I would say.

• 7:22Tim Scarfe?

  Yeah, there's this challenge with anthropomorphization that the existence proof we have, of course, are humans doing it, but it wouldn't be particularly good from an AI point of view if we have to create a simulacrum of a human. I do believe, though, that there's some kind of spectrum of strength of reasoning. And it feels to me that language models create these very blown-up circuits, and it's not reusing the same circuits in different situations. And we seem to have this incredible ability to reflect these very parsimonious, abstract motifs. And some cognitive psychologists argue that there's something fundamental about these motifs. Maybe it's the way the universe works, or certainly it's the way our cognition works.

• 8:06Tim Scarfe?

  And that doesn't seem to be the way that language models work.

• 8:09Speaker 00

  I completely agree. We have been arguing for these sorts of more modular compositional models for a long time. And I think that abstraction is an essential capability of humans that modern language models lack. But I would say that that's, again, going into the how of things. You know, there are a certain set of goalposts that I want to be able to achieve certain tasks, right? To me, it's useful to separate that. Definition of what we are trying to do from how we are achieving it, right? Using modular models in which there are explicit abstraction mechanisms. And we are going to talk about examples of that from my work and in other folks' work, I'm sure, in the going forward.

• 8:55Speaker 00

  But I think that it's it's possible that, you know, there may be some class of language models that comes up, you know, maybe with a different training objective, but that even though it's not explicitly dealing in, dealing with modularity, it's able to nevertheless achieve robustness, right? I don't know that such a possibility is just not there. However, I would say that, given all we have seen from recent language models, there seems to be something fundamentally challenging in terms of robustness. And to me, you know, mechanisms for abstraction and modularity would be a good bet to have, to achieve those goals.

• 9:40Tim Scarfe?

  Hmm. Oh, one from OpenAI. Is it reasoning?

• 9:44Speaker 00

  To me, it's a it's a milestone in reasoning. There's a big headroom ahead of it, but it definitely by measures that we just discussed, you know, performance in in programming tasks, in solving math problems, it seems to be substantially better than prior models. So to me, it's a step towards models that can reason.

• 10:08Tim Scarfe?

  Interesting. Are there any situations where, I mean, maybe we should first say, in situations where it is doing reasoning, which means it's fitting your criteria, I think it's fair to say that, yes, yes, it's reasoning. And then there's the space of situations where perhaps it doesn't reason for many reasons, possibly because of computational reasons. It might be trying to solve an NP hard problem and it just simply runs out of context. Or it might be trying to do reasoning in a domain where it hasn't been, you know, trained on, for example. So there are limitations, but you think in principle that those limitations could be overcome?

• 10:48Speaker 00

  I think that.

• 10:51Speaker 00

  O one augmented with a lot of other things could make substantial steps towards overcoming those limitations. Okay, now, there are a few things here that I have left ambiguous, and to me, that's where the real questions are, that what are those extra pieces that need to be added to something like O one in order to achieve, again, I wouldn't say does reasoning, you know, better performance at reasoning tasks, right? And to me, there are clear candidates, like, for example, having more grounding mechanisms, using more powerful symbolic tools, but this is speculative, and, and over the next few years, I think we are going to see if those methods actually work.

• 11:34Tim Scarfe?

  It's interesting to see the shift towards neuro-symbolic. So, a lot of folks in the kind of connectionism space, Andre Capati, for example, spoke about software 2.0, there's this idea, and Hinton as well, there's this idea that language models can do everything, that they can do this emergent symbolic reasoning, and, and we can train them end to end. And what we're starting to see now with things like alpha geometry and alpha proof and so on are these hybrid systems that, that kind of, and, and generally as well, I, I think that the way to robustness is building specific architectures to do specific things well. I, I think having these completely general blank slate things doesn't work very, very robustly, but are, are you seeing that trend as well?

• 12:18Speaker 00

  Yes, absolutely. Many of us have been arguing for neuro-symbolic methods for a while now, but increasingly, I feel that this term is, is unnecessary, because it seems to me that neuro-symbolic methods are really increasingly everywhere. You mentioned alpha proof, that's a great example, but I would say that even these agents that are Generating some code using language model and then executing the code. And then getting feedback and then using that to make further decisions. They are really doing something neuro-symbolic as well, right? Because you are actually using a Python interpreter, which is a symbolic tool.

• 13:03Speaker 00

  Now, that said, to me, the more interesting question is, again, not the word itself, but the precise form that these kinds of combinations are going to take. And we have seen some examples of this. So, for example, in Alpha证, we have a machine learning model, a neural model, that is getting feedback from a lean interpreter or a lean prover, right? And that's providing it a very solid form of grounding.

• 13:34Tim Scarfe?

  Hmm.

• 13:35Speaker 00

  So I think that we are going to see this trend in other forms as well, in broader settings. I don't know that it has to be extremely domain-specific. There is a world where you can imagine, you know, code execution and formal proofs basically informing all sorts of decision-making in the world with purely neural models serving as the layer that goes between human language and sort of messy signals to this kind of reasoning mechanisms.

• 14:08Tim Scarfe?

  Can reasoning exist without axioms?

• 14:10Speaker 00

  That's a great question. I think that, again, it depends on what we mean by reasoning. When we are talking about mathematical reasoning, the entire objective is that you're going from certain axioms to certain kinds of conclusions. So mathematical reasoning, as we understand it, doesn't really make sense without axioms.

• 14:36Speaker 00

  What about something like physical reasoning? So there, everything that we consider to be physical reasoning, it depends on us being in a certain place with certain laws of physics. So to me, you know, you can imagine reasoning happening in a world where those laws are different. But even then you have axioms, it's just that you have different axioms.

• 15:05Tim Scarfe?

  Can we combine together reasoning systems?

• 15:08Speaker 00

  Absolutely. We in fact do it all the time. We combine mathematical reasoning systems with, for example, you know, experimental empirical reasoning methods that people use in the natural sciences all the times when we are doing any kind of scientific discovery, right? And I can imagine that in the future, we could have many different reasoning systems with different kinds of capabilities and they all come together in something that's bigger than the sum of its parts.

• 15:41Tim Scarfe?

  AlphaZero, do you think that's reasoning and why?

• 15:44Speaker 00

  I think, again, it is definitely a powerful system that makes highly non-trivial progress on a task that's traditionally considered to be reasoning. So to me, you know, it's sort of a behaviorist definition, right? If it looks like a reasoning system, it does well on a reasoning task, then it's doing some kind of reasoning.

• 16:09Tim Scarfe?

  Okay, if it looks like a duck, quacks like a duck. What is neuro-symbolic programming?

• 16:15Speaker 00

  Neuro-symbolic programming is this approach to artificial intelligence where you are representing models using a mix of neural networks and classical symbolic code. So you could imagine, for example, you know, a program in which you have some neural modules that are making decisions about perception, let's say, whether or not, you know, a certain kind of object appears in a scene. And then you have some vectors coming out of that and then you have some symbolic methods that are processing those vectors.

• 16:54Speaker 00

  A lot of the times, this makes sense if you have prior knowledge about what a model should look like. So then you can, you know, imagine using the symbolic code to basically encode some of those priors. You could also imagine neuro-symbolic models being used when interpretability is a concern. So for example, you're trying to understand a certain biological process. Now, you may get this perfect black box neural predictor, except the scientist cannot really make sense of it and use it to guide experiments. But if you have a more

• 17:33Speaker 00

  mechanistic model that is coded up in the form of, in the sort of notation that scientists traditionally use, and to me, all of those are just, you know, programs, physics equations, and, and, you know, definitions of dynamical systems and so on. These are all just programs of various sorts. So if you have a model that is, you know, represented mechanistically like that as a, as a sort of program, but maybe with certain neural pieces for parts that just cannot be easily symbolically represented. So that would be another potential application of this.

• 18:09Tim Scarfe?

  Yeah, there seems to be, I guess it's quite an ambiguous term, but for example, Francois Charlet talks about discrete program search, using a neural network to guide the generation of programs. In, in your work, for example, you could use it to represent functions, or even some kind of post hoc validation type process, you know, to ensure things are in guardrails. And there are many, many more kind of instantiation. So, so I guess it's quite an ambiguous thing.

• 18:35Speaker 00

  It is. So when we defined the term neuro-symbolic programming, we want it to be very precise. But the word neuro-symbolic is again, as we discussed earlier, it's being used in lots of different forms, to the extent that I would say it has also kind of lost all meaning. But when we talk about neuro-symbolic programming, we mean a very specific thing, which is that I have a, I have a programming language in which I can represent these hybrid models. I have combinations of, of symbolic code and neural networks. And then we have some body of methods that are being used to discover those programs. And these methods may be

• 19:20Speaker 00

  Partly neural, partly symbolic. Typically, they are a mix of the two.

• 19:25Tim Scarfe?

  So many fans of the show would be familiar with the DreamCoder paper by Kevin Ellison and Tannenbaum, et cetera. As I recall correctly, there was a domain-specific language and they had a waking phase and they had this neural-guided search and they had an abstraction sleep and so on. So it's related to that idea?

• 19:44Speaker 00

  Absolutely. So I would say that there are a few categories of methods that have come out in the last few years in this space. And one big challenge is library learning, where you are not just working with a fixed programming language and trying to find programs in that language, but you are actually doing explicit abstraction and you're trying to discover new primitives that are then added to the programming language. And DreamCoder falls in this category. In DreamCoder, you are starting with an extremely low-level language, the lambda calculus. And then progressively, you are discovering bigger and bigger modules, which are abstractions,

• 20:29Speaker 00

  really. You're seeing patterns in these really low-level programs and then you're abstracting them into these modules and then you're reusing them, right? Now, the programming language that they had over there is purely symbolic, but one can easily generalize it. And there's in fact some work that's happened more recently where that's been done. So you could imagine then these programs that are mixtures of neural networks and these sorts of lambda calculus terms, right? And then the method that they used for discovering these library functions and also just do program synthesis, search for programs, those were all neural over there.

• 21:11Speaker 00

  One could imagine, you know, modernizing them, it's recent enough, but you know, a few years back. You could imagine bringing them to sort of 2024, adapting them to 2024 deep learning by using large language models to do the search over programs and abstraction.

• 21:31Tim Scarfe?

  Interesting. So DreamCoder was not using language models and it had a hardcoded DSL. And One thing that interests me is what the primitives are. So for example, we could search the space of Turing machines, we could use lambda calculus. I think Josh Tannenbaum is a big fan of cognitive psychology, which is that we have these native fundamental priors of cognition, therefore we should search those priors. And presumably it was trained to do a particular task. You could train it to do the ARC challenge. So then what it's kind of doing is it's saying, well, what's composition of these seeded priors in my DSL produce skill programs that would work for this particular thing? So like, there's a question of where do you start?

• 22:15Tim Scarfe?

  And to what extent is the task you're training it on? Kind of, does that derange or influence the library that you learn?

• 22:22Speaker 00

  Right. So to me, the prior question is open. I think that humans may well have a set of cognitive priors, but we don't necessarily know what they are. What is however true is that the presence of priors makes your ability to solve the program synthesis problem or the learning, library learning problem a lot better. And by that, I mean that if you have already a reasonable set of primitives that are there in your programming language, you won't have to discover everything from scratch. That said, I can imagine a world where you're starting with an extremely low level language without any sort of priors.

• 23:06Speaker 00

  And you are, you just have these basic operations like composition. And then you are just discovering the entire universe of programming, of mathematics, of physics, what have you.

• 23:22Tim Scarfe?

  Does it matter if we can't understand the programs that are generated? And this will be a theme in this discussion, because of course, your work in theorem proving as well is talking about how essentially mathematicians don't do the stuff themselves anymore. We're leaning on computers to search this huge space. But just with this discrete program search thing, we might be creating programs that are still, you know, lots of abstractions and lots of interesting efficiencies in there, but they seem quite inscrutable.

• 23:49Speaker 00

  That's right. So I think that we should distinguish between the interpretability question and the capability question. To me, there is potential value in interpretability, definitely in certain application domains like scientific discovery. We really care about interpretability. There is also a potential safety and security kind of angle, and we are going to discuss that later. But I think that it's useful to separate that concern from the concern of just what would it take to build models that are really robust and capable? And so I think that there is a universe

• 24:31Speaker 00

  where you have, again, an extremely low-level language, a sort of assembly language, and I consider the lambda calculus to be something like that. And then you just let the machine figure out over time what kinds of abstractions are useful. And to me, that could have a lot of value because you could discover things that no human would ever imagine, right? And that would enable you potentially to do new kinds of math, new kinds of physics, new kinds of biology. And so I don't rule out that possibility at all. I think this idea of abstraction would be valuable even in that regime because what that will mean is that you are going to, you know, discover these higher-level building blocks.

• 25:15Speaker 00

  Yes, you know, no human has figured that out yet, but this AI has. But then you're using this building block to build parsimonious programs, models, that can do amazing things. And then you're just bootstrapping and you're building up this, you know, entirely new universe of mathematics and computation, right? I can imagine such a world.

• 25:39Tim Scarfe?

  So can you tell us about your work in this area? So you've created this architecture that uses LLMs and does type-directed search and learning to search and so on. Can you tell us about that?

• 25:48Speaker 00

  Right. So I have a series of efforts in this space. I Back in the day, did a lot of work on just symbolic methods for program synthesis. And the setup there is that you have a programming language. You have a programming task that is defined either by, at that time, it was either logical constraints or a set of examples. And then you are defining a search problem. Find me a program that fits the task specification. And so those symbolic methods had some scalability challenges. And then when deep learning came about, you know, we all moved in that direction. And this sort of neurally guided program search, this became a very powerful approach.

• 26:34Speaker 00

  Now, some of the methods there, they combined these older symbolic ideas with the deep learning ideas. So for example, we had these results on type directed neural program synthesis, where you have a, you're generating programs in a strongly typed language. And the type system of the language serves as a pruning mechanism as well as a guidance mechanism. So it rules out programs that are obviously not going to be reasonable and also helps us focus on certain kinds of subgoals. Now, if you think of what's going on in the world of theorem proving, it's actually very closely related. So Lean is really a functional programming language with a really powerful type system.

• 27:18Speaker 00

  And so when you are, for example, using feedback from the theorem prover to rule out certain kinds of steps in your math proof search, you are really using a version of this idea, right? But we had been thinking about that for a while. And the broader program synthesis community that came out of the programming languages world, they were thinking about this problem. Okay.

• 27:46Speaker 00

  Then, this is still in the context of you have a fixed programming language and you're looking for programs in that language. Now, there are other approaches that are relevant here. So we had, for example, these results on using neural relaxations. So there is this paper we have led by Amish Shah and with Isang Yu, who's my long-term collaborator, and Jennifer Sun, and my former student Avina Verma. So this was on using neural relaxations of programs as heuristics for doing a search of her programs. So the idea is this.

• 28:31Speaker 00

  Suppose you are doing a search of her programs and you are progressively filling up these incomplete programs. So you start with nothing, just a code with a big hole in it, and then you're progressively adding more and more code. So one challenge here was that because you're always working with these incomplete programs, how do you know whether or not a certain decision is valuable? Right? As in, you know, should I keep a certain incomplete program in the pool or should I throw it out? And the idea then was that, you know, in that hole, you're going to, so there is a space of possible ways to complete that program.

• 29:17Speaker 00

  So there are a lot of symbolic discrete terms that you can plug into that hole. But instead of that, what you do is that you stick a neural network in there. And there is this kind of a subset relationship. So because these neural networks are more expressive than any symbolic program in your programming language, you are going to have the property that if you train the neural net well enough, you're going to get a loss that is better than whatever you would get with any sort of symbolic program. And this leads to a, an argument that you can basically use the, the, the, the loss that you get after you have plugged in this neural network into that hole.

• 30:01Speaker 00

  You can use that as a lower bound on the cost to go. That is the, the best possible thing you can do from that point on, using a symbolic program. And this can in turn be used to guide heuristic search. You know, this sort of classic search algorithms like A* and, and branch unbound plus, you know, iterative deepening search and so on. So there are, there's this whole slew of algorithms from GoFi back in the day, right? And now you're imagining accelerating these sorts of algorithms with these neural relaxations. Yep. So this sort of idea has been there.

• 30:42Speaker 00

  So in general, we have looked a lot at this question of, you know, can I use a neural network as a relaxation, a sort of continuous approximation of a discrete program? And to what use can we put such a relaxation? And we have looked at a few versions of this. Other more recent efforts, so we have this recent paper on library learning in the context of symbolic regression with, with LLMs. And here, we are doing a lot of these same sorts of things, you know, searching for programs, doing abstraction, but this time using LLMs. And in particular, an LLM can be a really good way of guiding, even if you're doing

• 31:27Speaker 00

  this sort of traditional search over programs, for example, using a genetic algorithm or using, you know, some sort of type-directed enumeration, you can still imagine, you know, an LLM serving as the neural network that guides such a search. But on top of that, you could also imagine using an LLM as a tool for abstraction of the sort that we were talking about a little while ago. So for example, you know, in Dreamcoder, the way abstraction would happen is that you, you know, look at a set of programs that did well, and then you find syntactic substructures.

• 32:06Speaker 00

  That show up in those programs again and again, right? And then you would say that, OK, this is a module that I can potentially reuse. And that then becomes part of my library. The issue is that this is, this process can be difficult because identifying these sorts of common substructures in a large pool of programs can be very challenging. And there were these symbolic methods that were used for this purpose. But you could imagine not doing that and instead just using an L L M. What could that look like? Well, you should read this paper, which is led by Arya Gryali and Athar Vasagel.

• 32:46Speaker 00

  And it's with Miles Kramer and Omar Costieris appearing at NewRIP this year. But the basic idea is that you are going to use an L L M as the abductor. So you're going to ask an L L M, what are some of the common patterns that are showing up in these programs? And you're going to use its natural language, you know, reasoning, I understand it's a loaded term, but its ability to at least, you know, find patterns in syntaxes, in the syntax of programs, you're going, and, and explain that in natural language. You're going to use that capability to do the abstraction, right? And that's how you're going to learn a concept.

• 33:23Tim Scarfe?

  I'm a big fan of Miles Kramer. He wrote a landmark paper on symbolic regression.

• 33:28Speaker 00

  That's right.

• 33:29Tim Scarfe?

  A few years ago. And I guess that is that another form of neurosymbolic programming that, and, and also I've heard people talk about doing symbolic decomposition of language models. So this idea that, you know, you, you, you start with this kind of block of clay, you do stochastic gradient descent, and then we, we tease out some kind of symbolic structure from it. It's a fascinating idea.

• 33:48Speaker 00

  Absolutely. So going to your first question first, symbolic regression, I see it as a form of program synthesis.

• 33:56Tim Scarfe?

  Yep.

• 33:56Speaker 00

  Really, what you're trying to do there is that you're given a data set, you're trying to find a, an expression, right? That, that fits that data set well. But an expression is just a special kind of programs. So some of the methods that we have talked about, for example, this neural admissible heuristics, that was done in the symbolic regression setting, that you're trying to find a program that fits a data set well, right? But now, one can imagine going beyond the sort of genetic programming approaches or these approaches of distillation, where you first train a neural network and then distill it into a symbolic program.

• 34:38Speaker 00

  You can go beyond these kinds of strategies and you can use an LLM really heavily in order to do that, to solve that symbolic regression problem, right? And so what are the ways in which that can be used? One angle is that you could use an LLM to basically do the search of our programs or guide the search of our programs or expressions. In particular, these, let's say that we are talking about evolutionary search. So you could imagine using an LLM to do the crossover or the mutation of the programs that are there in your pool.

• 35:16Speaker 00

  And you can also use an LLM to do the abstraction, which is that you could ask the LLM to come up with some of the concepts that are showing up inside the high-performing programs, right? And then those concepts become a condition under which they basically condition the search of our programs at that point.

• 35:40Tim Scarfe?

  So I spoke with Sabarao Kamahati very recently, and he's got this LLM modulo architecture. So he said, LLMs are very creative. So we can kind of traverse this space and then we stick a verifier on the end, so we actually, we can kind of cherry pick when it actually gets it correct. But I had a bit of a disagreement with him because certainly when we let the LLMs find creative things, when we're doing, let's say, LLM-guided search, and when we let the LLMs do abstraction, I feel that they are still somewhat parasitic on the data that they are trained on, which means there is a kind of creativity gap. We seem to have access to a source of creativity which is richer.

• 36:24Tim Scarfe?

  And then there's the thing, well, we're building up this library, and at some point, does the weight of the library kind of affect our creative ability?

• 36:33Speaker 00

  That's a fantastic question. So one thing I would add is that in settings like symbolic regression, you have the advantage that you have grounding provided by the data. At the end of the day, what you're trying to do is you have seen some empirical, you've made some empirical observations and you're trying to find expressions that fit those observations, right? So now, when you have a new candidate that is creatively constructed by the LLM, you could imagine actually evaluating that on your dataset and seeing how well it does, right? So that's something that prevents it from going off the rails completely.

• 37:15Speaker 00

  Now, regarding the prior knowledge question, yes, absolutely. LLMs are drawing on the prior knowledge that they have seen. And if you're using LLMs in a purely black box, zero-shot way, then you are only going to be constrained by what the LLM has seen before. Now, I would add that this is still a, there's still a non-trivial value in that prior knowledge because when you are doing new science, you are typically building on science that other people have done before. And the LLM has presumably seen that in the form of various sorts of scientific papers and, you know, math problems and so on.

• 38:00Speaker 00

  But that said, you know, you don't have to be stuck to this zero-shot, black box model. You could imagine a loop where you come up with candidates creatively using an LLM. You empirically evaluate these candidates and then you use the experience to basically fine-tune the model further. And you could even imagine a universe where you are starting with an LLM that is completely blank slate. Maybe it has some elementary knowledge of language, but not much science. And then you are just progressively building it up on all manners of scientific tasks. And it's seeing, you know, how various kinds of hypothesis performed. It's getting feedback from the real world, right?

• 38:45Speaker 00

  In the form of experiments. Maybe it can even go ahead and do new experiments, right? Reason about causality and determine what are some of the new experiments to try out and then get feedback.

• 39:00Speaker 00

  In terms of the results of those experiments and then use that to, we can use that information to fine tune it further, right? So a lot more is possible than just using, you know, an L L M and then as a black box and then just having a verifier at the end.

• 39:16Tim Scarfe?

  I agree with that and there's always this discussion about creativity. I mean, Demis Hassabis spoke about the ladder of creativity with the inventive one being the highest strength. And of course, you know, we can, we can imagine unicorns. We can imagine things that we haven't seen in the real world because they're still composed of primitives that are in the convex hull of things that we understand. But in the, in the context of program generation, so language models, they have so many degrees of freedom, you know, they understand, you know, natural language and like made up languages and programming languages and so on. And then we can do things like generating code and we can use DSLs. And even, even then, if, if, if we execute a bunch of these programs, they might not halt or they might not be valid. So there seems to be like another step we need to do to actually check that these are,

• 40:01Tim Scarfe?

  these are good programs to run.

• 40:02Speaker 00

  That's right. And by the way, you can get more forms of feedback than just whether or not this program ran correctly on a few tests. You can do more serious kinds of analysis of programs as well.

• 40:15Tim Scarfe?

  Go on.

• 40:16Speaker 00

  But at the end, yeah, so you are getting all these extra forms of feedback from those external tools. And then the question is, what do you do with that, right? So you could just use that to decide whether or not you keep this program. But you could do more. Maybe you could go and go back to the, the L L M and, and use this information to basically train it further and guide the way it writes programs. And if you think of human programmers, that's how it happens, right? So you write code and then you try out various sorts of things and then you see that certain kinds of programs work and certain kinds do not. You get feedback from your compiler, your type checker, your interpreter, right?

• 41:01Speaker 00

  And then you use that to refine the way you code as well.

• 41:04Tim Scarfe?

  Yes, even with the halting problem, I mean, I have some idea in my mind that this is, I don't know, it's a quadratic algorithm and it's got a thousand data points.

• 41:13Speaker 00

  That's right.

• 41:13Tim Scarfe?

  It's still running after 90 seconds. Probably there's something wrong here. Ctrl C, I go back, fix the button. Yeah.

• 41:19Speaker 00

  And, and you know, there is a huge body of work on solving the halting problem, even though in principle, this is an undecidable problem. In practice, this literature on proving termination of programs, the way it works is that it recognizes that proving termination of a program is really about coming up with an inductive argument. So what you're showing is there is some kind of an expression whose value goes down strictly each time you execute one step of the program. So if you think of a loop, right? So you have written a loop where it says that while i is less than n,

• 42:00Speaker 00

  you know, something, something, and then i gets incremented. You know that this program is going to terminate, you know, in spite of Alan Turing. The, the reason is that what's going on is something very simple. Each step of the loop, you are incrementing this i, and it can only go up so far, right? And so there is this value, which is n minus i, which is strictly going down in every step. And it can only go down so far. It cannot go down below zero because zero or whatever, you know, lower bound you have set, because of the way your program is structured. And so this kind of a reasoning that you're doing here, right?

• 42:42Speaker 00

  This is an example of an inductive proof, except applied to programs. And there is a lot of work on automatically discovering these sorts of inductive proofs, which are really, you know, very simple symbolic expressions, right? And you could imagine using an L L M or other kinds of machine learning techniques to search for these sorts of arguments.

• 43:02Tim Scarfe?

  Couple of points on that. And maybe you should bring in Turing's famous proof, because he proved by contradiction, didn't he, about the halting problem? But, but also, if I understand correctly, you're pointing to specific instances where you can do proof by induction that a program would, would halt. But you, but would you accept that there are still a space of programs that, that you wouldn't be able to do that?

• 43:24Speaker 00

  So I didn't say anything about automatically discovering those inductive proofs.

• 43:32Tim Scarfe?

  Okay.

• 43:32Speaker 00

  So so my point is that for a vast number of practical programs, in fact, most loops that people write or most recursion that people write, the argument for why these programs are going to terminate is very simple.

• 43:48Tim Scarfe?

  Hmm.

• 43:48Speaker 00

  And you can search for those kinds of proofs using various sorts of methods. Even just basic enumeration works quite well, but you could imagine, you know, using more contemporary machine learning techniques to solve this problem. But you cannot possibly have a method that is going to be automated and it's going to sort of it's going to always terminate and it's going to work for all programs. No. But the question is that, you know, for realistic programs, will this work or not? And we have every evidence that for realistic programs that people write, you could just do one of these things.

• 44:31Speaker 00

  You could try some of these strategies to prove termination. And if that doesn't work, you just say that, okay, you know, there is a problem here. Just go fix it, right? And maybe there is some reason why that program would still work, but you know, whatever, you know, you can just ignore that program and find a different way of solving the problem.

• 44:46Tim Scarfe?

  So my co-host, Dr. Dugger, he's really interested in Turing machines. And he says, you know, language models, they're, I mean, we're just, we're not talking about LLM systems. We're just talking about just a language model. He said they are finite state automata. And a Turing machine still has a finite state automata as a controller for these kind of pushdown automata. And he said, you know, so that there's a space of algorithms in the FSA class. He would actually call these Turing machine algorithms, even though they are for a finite state automata, that cannot be searched, discovered with stochastic gradient descent because of this halting problem. Now, I think you were pointing to earlier some interesting research that's been done in this space. I mean, he would be fascinated in that.

• 45:26Speaker 00

  Right, right. Yes. So there's been a whole lot of work on using gradient descent to solve program synthesis. And to me, searching for Turing machines, it's just a form of program synthesis. It's just the programming language is extremely low level. It is the that every program has, you know, access to this one counter, the tape, and then.

• 45:52Speaker 00

  And then also a controller, which is a finite state machine, right? So to me, this is a very simple kind of programming language. And it was useful in mathematical proofs in the theory of computation because it was so simple, right? But I don't think that there is anything special about Turing machines from the point of view of programming, right? Anything, any reasoning that you can do about Turing machines. You can also make the same kinds of arguments about other broader classes of programs. Now, there has been a lot of prior work on doing gradient descent to find programs, and these have not been very successful for the reasons that you are alluding to.

• 46:37Tim Scarfe?

  Yeah.

• 46:38Speaker 00

  And that's why people have historically wanted to use neural networks in a sort of guiding role, that you are still going to have some kind of a discrete search going on, and then you would, you know, use a neural network to guide that search process in various ways. And I would say that the use of neural networks in Dreamcode is an example of this, but also the use of L L M's to write programs or guide searches over programs, that's also, those are also examples of this.

• 47:12Tim Scarfe?

  Interesting. So Turing machines have this amazing ability to expand their memory. So we don't, we don't need to train the thing again from scratch. We can, we can just say, I need, I need to, I need to get some more data, I need to get some more data to add to my memory. And people say, well, you take a language model and you can train it to do RAGs, or even during its training process, presumably it's actually retrieving things from, from a database, or you could train it to do code execution. And then you could say, well, aren't we basically searching Turing space? Because I can, I can say, generate me a program that computes the nth digit of pi.

• 47:48Speaker 00

  Yes.

• 47:49Tim Scarfe?

  Which is something that, you know, has a, has an arbitrary runtime. And, and then I can run that on, on a tool, and then I can pass it back in. But it feels to me that there's a difference in kinds, right? But, but what is the difference? What's the difference between doing that and actually having a machine that can search Turing space natively?

• 48:07Speaker 00

  Okay, so I'm trying to understand. So you could imagine having the definition of the, of the Turing machine.

• 48:18Speaker 00

  Programs as as just a DSL, right? You could define a programming language.

• 48:22Tim Scarfe?

  Hmm.

• 48:23Speaker 00

  That's where each program is a Turing machine. Right? So to me, this is this is just what you would do if you open a theory of computation textbook. If you go to the definition of Turing machines, it's just a programming language, right? There is a syntax, there is a semantics. So now, what is the difference between training and L L M to generate programs in this language and any other kind of program synthesis that L L Ms already do? Right? I don't think there is a fundamental difference between Turing machine generation and Python code generation. Now, I think what you're describing, though, is something slightly different, which is

• 49:04Speaker 00

  that the process that is being used for this generation, you know, is that process a finite state process or is that process something more like a Turing machine? And that, I think, is a very interesting question, right? So what you're really saying, that instead of having a language model which is just operating, which is strained in this particular way, that it's just predicting the next token and and yes, maybe it can retrieve us a bounded amount of information, maybe, you know, instead of having a massively scaled up L L M, massively scaled up autoregressive model, you could have a massively scaled up Turing machine that is doing all sorts of generation, right? And I think that's a very exciting idea.

• 49:47Tim Scarfe?

  Well, yeah, exactly. And the thing that it took me a while to get my head around is is the the controller in a Turing machine is a finite state automator. So that there exists a set of weights in a language model that would allow it to, you know, to to to expand its memory with some push down automata or something like that. So we just can't find it with stochastic gradient descent. And the the other thing is, yeah, I completely agree that we could, in principle, imagine we had a huge data set of internet scale of Turing machines and descriptions, because I think the descriptions is important, because what's the point in having a Turing machine language model that we can't program in in any way? So there needs to be some kind of intelligible mapping to something that that we could use to instruct it.

• 50:32Speaker 00

  Right. So again, though, I would make a distinction between the what is generated and how you're generating it. So there are two different possibilities. So one is that you use a language model, whether it be a Turing machine language model or an RNN language model or a transformer language model. You're using some sort of a language model to generate programs in this Turing machine language. So that is version one, okay? Version two is one where you're making the specific point that this language model itself is a Turing machine, that it goes, it has this ability to, you know, access this unbounded memory and it goes and, you know, looks up stuff from this infinite tape, this

• 51:17Speaker 00

  unbounded memory. And that is something that is a very interesting proposition. My one hesitation there would be that we are finding out that the architecture may not matter that much after all. What really matters is the scale. So there are all these new results about, you know, state space models and highly scaled up RNNs. And we are seeing that many of these tasks for which transformers seemed especially capable are also being done by these extremely scaled up RNNs, right? So I think that, you know, it is possible that this Turing machine architecture is

• 51:59Speaker 00

  going to lead to, you know, amazing new capabilities, but I would probably wait to see some more evidence on that. But that said, it's definitely a very interesting idea to explore.

• 52:11Tim Scarfe?

  Yeah, there's always the objection of, well, for all practical purposes, it doesn't matter either because we can scale up the models. And I'm very excited about, you know, MIM, LSTN, state space models and Mamba and all of these things, because they can allow us to possibly 10x our model size. And then there's always the question of, well, at some point, the models are going to be big enough to do all of the reasonable types of computation that we want to do. But the counterargument to that is, you know, we sometimes spend a lot of time pondering problems and, you know, the Linux operating system, Keith always gives this as an example, you know, that we've had to design some really complicated artifacts to reach the level of, you know, technological complexity and

• 52:55Tim Scarfe?

  maturity that we have now. And it seems out of reach of these models, even if we 100x them.

• 53:01Speaker 00

  That's right. That's right. Yes. So I think that.

• 53:06Speaker 00

  You know, I'm a big believer in having algorithms that are that go beyond just the the autoregressive language model paradigm. And that's why we were talking about these methods where you have these external tools like, you know, code interpreters or or, you know, lean prover or theorem provers like lean and using feedback from them to do something more than what we could do with autoregressive models. But to me, the power of these methods come not from the internal architecture of the

• 53:47Speaker 00

  language model, but more in the higher level architecture of how these different kinds of grounding mechanisms work together with neural networks, right? And I think that that's a it's it's possible that a different neural implementation of of L L M's is going to give you drastically better results. I may be a little bit skeptical about that. It's something I would like to see more evidence of. But what to me is very clear is that if you have these sorts of higher level architectures where you are combining neural networks of whatever sort, right?

• 54:30Speaker 00

  With these kinds of symbolic grounding mechanisms, executing in the real world, human feedback, all of these things, you're going to get something better than what we have today. And to me, the challenge then is, how do you pass back feedback from these various sorts of grounding mechanisms back to the neural network? And maybe when you are doing so, certain kinds of neural architectures are going to be a lot better. But that is something I'm I'm still kind of on the fence about.

• 55:01Tim Scarfe?

  I really agree with with what you're saying. I mean, one thing I've noticed is, right now, certainly building real world applications, the way to overcome this complexity curse is with architecture and process. And it's the only way to to robustify these things. Possibly the only trade off, though, is the more engineering and architecture you put into a problem. You're kind of robustifying it for that problem, but you're also somehow taking away some of its generality and other problems.

• 55:31Speaker 00

  Right. So this is why I would ideally like to see something quite simple, an architecture that is quite simple and domain general. But it seems to me that there are a few examples of this. So, you know, let's take mathematics. So to me, mathematics is a very useful model for doing a lot of different kinds of, solving a lot of different kinds of problems. So for example, if you're doing physics, if you're doing biology, if you're doing programming, mathematics is useful. Even for day-to-day logical reasoning, mathematics is useful.

• 56:10Speaker 00

  And so I could imagine that the use of a tool that can give you rigorous feedback about the mathematical soundness of your models of the world. To me, that makes a lot of sense. And so I would probably not consider that a restriction on the kinds of approaches that, on the kinds of domains that you can apply your methods in. Likewise, code execution. To me, code is a very general model, a way of representing models of the world. And programs to me always come with semantics.

• 56:53Speaker 00

  So being able to execute programs and also analyze them and, you know, reason about sort of worst-case behaviors and so on. This is also something that I don't think imposes a massive restriction. So to me, the idea would be that you would have these sorts of grounding mechanisms that are fairly general, and then you would have a flexible way of composing them together. You wouldn't impose, you know, you wouldn't hard code a lot of things. You would maybe hard code when you are deploying these methods in particular applications, but the framework should be perfectly general, where you can write out, you know, new kinds of complex compositions of, say,

• 57:36Speaker 00

  lean proofs and code execution and neural prediction and maybe some natural language processing and vision as well, why not, right? So you would allow compositions of all of these different kinds of modules into new kinds of models, and then you would, you know, maybe let a An AI system just go and try to find the right composition.

• 57:57Tim Scarfe?

  Can you tell us about the laser architecture?

• 57:59Speaker 00

  Absolutely. The laser approach, the goal of this approach is to to use L L Ms to drive a search over programs and also to come up with abstractions that explain what is going on in high performing programs. This was done in the context of symbolic regression, where the setup is that you have a you have a data set and you have a language of programs or expressions and you are trying to find a high performing expression.

• 58:36Speaker 00

  Now, prior approaches here, they used evolutionary search and there is also some work that uses L L Ms to basically direct some parts of that search process. But what we were really exploring is that can we use L L Ms to come up with high level explanations or high level concepts that show up in the high performing programs? And so you could imagine a process where, you know, evolutionary search is coming up with a pool of candidates and you are actually evaluating these candidates in a using the data that you have. And so this serves as a grounding mechanism. Now you have a bunch of high performing candidates left.

• 59:19Speaker 00

  Now you're using the L L M to to explain what are some of the common themes that are showing up in these these high performing programs? And then you are remembering those themes, those concepts, and then using those to drive the search as well. Right? So an approach like this, one big appeal is that even if you're not using all of the, you know, the scientific prior knowledge that the L L M has, just the ability of L L Ms to abstract pieces of text into higher level concepts, that is something that is still very helpful.

• 1:00:01Speaker 00

  So we deployed this approach in the problem of finding rediscovering a bunch of standard equations. So specifically, equations from the all the equations in the Feynman lectures on on physics. This is a task that was proposed in this AI Feynman paper by Max Tegmer and and others.

• 1:00:23Speaker 00

  And in addition, we also evaluated the system on some synthetic benchmarks. And we also used it to do a new discovery of an, actually, an LLM scaling law.

• 1:00:35Tim Scarfe?

  Oh, tell us.

• 1:00:36Speaker 00

  Yes, absolutely. So here, we wanted to go beyond the Chinchilla law. We wanted to come up with a new law, just using data on LLMs. So you have, you know, information about, for example,

• 1:00:53Speaker 00

  number of parameters, the size of the data set, and, you know, how many shots were used in, in, in training and so on. So you have a bunch of these parameters and then you have, you have also data set characteristics, right? And then you have performance. And so now you could ask this question that, can I come up with, can I discover a symbolic law that is going to explain the LLM's behavior? Now, what we found was that we have this, we got this law that was a little bit different from the Chinchilla law. And that was definitely an objective, that we wanted to find something that is different, but yet as explanatory. And yes, for more details, please see the paper.

• 1:01:38Speaker 00

  But in addition to that, we also evaluated the system on completely synthetic tasks. And there also we found that this concept learning idea made some difference. So even if you ignore the LLM's prior understanding of the problem domain, which is not something I would argue you should do, because at the end of the day, in real-world applications, you are building on pre-existing knowledge. But even if you ignore that bit, you still have another way to use LLMs, which is as a tool for coming up with abstractions.

• 1:02:13Tim Scarfe?

  Yes, I'm also inspired by Melanie Mitchell's, she's done some work in this area. There seems to be something really interesting about iteratively abstracting.

• 1:02:23Speaker 00

  That's right.

• 1:02:23Tim Scarfe?

  Which is to say that there's almost some fixed outer loop and you're going up and you're going up and you're going up. That seems, tell me about that.

• 1:02:31Speaker 00

  That would make a lot of sense. The way we are doing it right now in laser is a little bit less sophisticated. We have our abstractions described in just natural language. But you could imagine a world where you have these abstractions represented in a more symbolic programmatic form as well. And now as time goes by, your abstractions, you are deliberately designing these abstractions to be higher and higher level. That is not something that we have done, but I would say that that is something that's present in Dreamcode. Because in Dreamcode, you do have, once you discover some library modules,

• 1:03:13Speaker 00

  you can write new programs using those library modules and then you can abstract them further, right? So this abstraction process, it is naturally directed towards discovering higher and higher level modules.

• 1:03:24Tim Scarfe?

  And could you make a quick comment as well that this is, to me, it's so exciting. It's not currently Sota, I mean certainly Dreamcode, for example, isn't Sota on the ARC challenge. But I have a deep, I can feel it in my bones that it's the right way to go. And unfortunately, because of the Sota chasing and so on, there isn't enough attention being paid to this really, really innovative work. I mean, what are your reflections on that?

• 1:03:50Speaker 00

  I think that Sota chasing is a really unfortunate trend. It is also, I think, it's a misallocation of resources. There are companies that are well suited to chasing Sota because, you know, you need both exploration and exploitation. And chasing Sota would be exploitation, right? You have a well-defined approach, now you're scaling it up, you are solving new problems that you couldn't do before. Great. But I think there is also this exploration direction that is very important. And unfortunately, Sota chasing is hurting that a bit.

• 1:04:38Speaker 00

  But at the same time, I would say that there are a lot of folks that are that are coming up with new interesting algorithms. What needs to perhaps happen is more of an arc from the exploration to the exploitation. So in other words, you know, let's say that you have this this algorithm like Dreamcutter. How do you scale that up? Okay, so our laser method is one way of scaling it up a bit by using L L M's. But maybe, you know, there are other approaches as well. And also, there is the question of how can you connect this to run this on very, very large amounts of compute? And and then can we see what happens?

• 1:05:23Speaker 00

  Now, this is something that we haven't done yet, but that's that's a direction that we are definitely very interested in. We are speaking with various partners to see if there's any way of scaling this up fastly. And we would be very excited to know what happens once we do that.

• 1:05:43Tim Scarfe?

  You've worked extensively on mathematical discovery. And I think you made the comment in one of your papers that you think we might have an A I co pilot by twenty twenty six. What makes you think that?

• 1:05:56Speaker 00

  That was actually a point made by Terrence Tao.

• 1:06:00Tim Scarfe?

  Oh, my apologies.

• 1:06:01Speaker 00

  Who I greatly, who I greatly respect. And I actually agree with that. So I think that we are in an extremely exciting time in A I for math. And I would imagine that getting an A I as a significant contributor, although not the, you know, the sole author in a math paper or even a computer science paper with significant mathematical components should be should be possible in the not too distant future. Now, okay, so what do we really mean by that?

• 1:06:43Speaker 00

  So, you know, if you think of the way mathematics is done and even actually.

• 1:06:51Speaker 00

  What happens in theoretical computer science? You have these definitions that are pretty rigorous, but ultimately, and you have proofs, but ultimately, the purpose of these is to convince human reviewers and human readers, right? And so what that means is that you can make mistakes. There are corner cases that you can you can forget, and your proofs may be broken as a result of that. So this is one possible risk from the way in the way mathematics is done today. The other thing is is just scaling up, right? Even if you don't think that there is anything fundamentally

• 1:07:35Speaker 00

  wrong with the way math is is done today, there is an opportunity to scale up mathematics using computational tools. That was just not possible until now. So what I mean by that is that if you think of, you know, a very large software system, if you think of, say, the Linux kernel or the Google Cloud infrastructure. These are extremely complex systems that no individual human can necessarily fully understand. People understand these systems at the high level of abstraction, and maybe they know, you know, all the low-level details of specific components.

• 1:08:17Speaker 00

  But I would say that there is really no one, or at least very few people, who have a detailed view of the of the entire system all the way.

• 1:08:30Speaker 00

  Now, if you think of math proofs, historically, math has been very oriented towards these individual contributors. So when you are thinking about a mathematician, it's somebody who, you know, they produce a proof, and this, all the details of the proof, they they know, right? And and they have produced it themselves, or at least they have understood those details. But imagine a world where you have these extremely complex mathematical theorems, where maybe, you know, no human is, individual human is able to understand all of the details. But you still have the guarantee that the overall proof can be broken down into these pieces that are more manageable by humans, right?

• 1:09:15Speaker 00

  Just the way we write code. Could we do that for mathematics? What would that look like? I think that that's a tremendous opportunity that these systems like Lean provide. And now AI naturally comes in, just the way AI co-pilots have made it much easier to write code. You could imagine having AI co-pilots writing math proofs as well. Now, if all of that is possible, so we'll have maybe new kinds of mathematics, new modalities of collaboration between humans, and this is something Terry Tao has extensively talked about. And then AI driving this process, making us 10x more productive. Would I say that that would lead to, you know, new papers with AI contributors? I would say yes.

• 1:10:00Speaker 00

  Now, you know, maybe we wouldn't list the AI as a co-author necessarily, because just like we don't, you know, list our calculators or computers as co-authors, we probably would just accept that, okay, you know, there is this tool over here and it did a bunch of things, but but there is still human creativity at the higher level and those are going to be the co-authors. But I would say that the AI would definitely still do a lot of things that today a math grad student has to do.

• 1:10:30Tim Scarfe?

  Interesting. So we are seeing, I guess a lot of people think about mathematical theorems as being quite parsimonious units that an individual mathematician or a few mathematicians have worked out and understood. And we've, I guess, not until recently, thought about what would it look like for this to scale massively?

• 1:10:48Speaker 00

  Right.

• 1:10:48Tim Scarfe?

  And so, yeah, we need to convince the reviewers. And you're saying that the reviewers, even though it's increasingly inscrutable because it's so large, the reviewers would be more inclined to trust it if it were found by a computer.

• 1:11:00Speaker 00

  So I would even question why you need a reviewer to understand every single detail of the proof, right? Maybe the reviewer needs to understand the high-level components of the proof and then just have an assurance that the lower bits of the proof are done correctly. Just like when you are reading code, you don't necessarily think about, okay, here is a system call that this code made. Is this system call implemented correctly at the assembly level? You don't reason about that. It's something that you assume that the Linux kernel implementer has properly figured out, right? So in the same way, one could imagine proofs where the proof is at the higher level of

• 1:11:45Speaker 00

  abstraction and then there are these lower level building blocks that you are taking for granted. Now also, one could imagine, you know, just like when you're building a big system in software, you break up the system into pieces, you pass these responsibilities on to different folks, and there is an interface where things are supposed to check out and so long as they do, and there are tests that pass at the unit level and end to end, you just accept that this system is okay, right? So likewise, you know, maybe for mathematical proofs, we should also have the same sort of decomposition. You would have this, you know, big, complex proof.

• 1:12:29Speaker 00

  Let's say we are talking about farmer's last theorem, which took an individual human a very long time to prove, right? But maybe now you're going to come up with decompositions, you're going to have a team of a thousand mathematicians that go and look at the pieces, and then there is some way of assuring that assuming these pieces are done correctly, everybody fulfills their local obligation, the global goal of proving farmer's last theorem is going to be true.

• 1:12:56Tim Scarfe?

  So I'm fascinated by that, by this idea of kind of decomposing a larger whole into these local obligations. Let's look at the Linux operating system. Do you think there is some kind of a bottleneck introduced by having these human intelligible interface modules at the local level? And what I mean by that is, I can imagine a future where language models are so powerful, they can, they can just regenerate the entire code all of the time. But that's going to be a nightmare for checking in code, isn't it? Because, you know, John, I've just broken John's component and this interface has changed and the schema over there has, has changed. So do you think there's always going to be an interesting kind of trade off where in

• 1:13:35Tim Scarfe?

  order to have an interface that is consistent, we'll need to almost like increase the complexity of the local modules?

• 1:13:43Speaker 00

  Right. So I think this goes back to this discussion of interpretability and, and capability. So I think that in principle, it is possible to come up with a Linux kernel that is written entirely in low-level assembly code. And it is, it is not modular. It doesn't have these sorts of human comprehensible interfaces, right? But yet it is provably safe. And by that, I mean that you have these high-level objectives that some set of humans have written down of what are the properties that the Linux kernel needs to satisfy.

• 1:14:27Speaker 00

  And then, you know, your AI goes in and produces this massive blob of assembly language code. And then there is also formal proof that this code is actually doing the right thing, right? So then, why would we have any objection? The issue to me is that, number one, there is, that kind of AI is, at this point, fantasy. We don't really have any AI that can produce, you know, large bodies of highly reliable code without any kind of human intervention, except at the very top level of doing some specification. And also, you know, over time, requirements are going to evolve and you may, you want

• 1:15:08Speaker 00

  to have a path through which humans can be involved in the, in the maintenance of this Linux kernel of yours. And I think that the same sorts of argument apply to mathematical proof as well. There is a world where all math gets done just via, you push one button and then the math gets done. So the mathematician comes up with this theorem, they state the theorem, and then they push a button, and then your AI goes in and just comes up with a proof in the lowest possible level without any kind of, any kind of human interpretability. But there is a proof checker, namely, let's say, the Lean proof checker, that has checked the proof for you, right? So I think that this is possible in principle.

• 1:15:51Speaker 00

  In practice, we are very far away from that. So at least in the short run, we want to have proofs that are at least, you know, interpretable at module boundaries. And then humans can be involved in designing the high-level process, and then the machine takes care of the low-level details.

• 1:16:12Speaker 00

  But I could imagine a world where humans are less and less involved, although you know, that would raise some questions about what's the point of this mathematics? You know, part of the reason for mathematics is that it's fun. It teaches us something about the world. But you know, if the point of mathematics is that it's purely an instrumental thing, that you are doing this mathematics so that you can predict whether or not, I don't know, a certain kind of chemical reaction is going to take place, then maybe that's something that you can allow the AI to do, just like today you use Mathematica or MATLAB to do a lot of that simulation.

• 1:16:51Tim Scarfe?

  So what are some of the advancements in this area? I mean, I know you've done a lot of work in this area. What should people look at?

• 1:16:57Speaker 00

  Right, so there are a few different directions. The direction that's the most well studied is theorem proving. And so here, there are a couple of versions. One version is that you are starting with a formal statement of the theorem in a language like Lean, and then you are searching for a proof of this theorem. So in a framework like Lean, a proof is just, it's just like code. It's a sequence of instructions, which are in that setting called tactics. And so you are finding a sequence of tactics that's going to lead the goal to be proven, which is really like finding a program that's going to achieve a certain specification.

• 1:17:40Speaker 00

  And there's a lot of work on this. The most promising approaches, they combine the use of a neural network with execution in the Lean environment. And you're getting some feedback as to whether or not, you know, the decision that you, the tactic that you applied led to good things or not. And then you would use that feedback to do more generation. So that's sort of what's going on there. There is also a body of work on informal theorem proving, where you have natural language problem statements, and you are using a lot of the times purely informal methods,

• 1:18:21Speaker 00

  like you know, the sort of variance of chain of thought to do math reasoning. But sometimes you're also combining these two approaches. So there was this nice paper by Sean Wallach and others on

• 1:18:35Speaker 00

  Doing, using a natural language model to come up with a high level proof sketch, and then using that proof sketch to drive a formal prover.

• 1:18:44Tim Scarfe?

  What was the name of that paper?

• 1:18:45Speaker 00

  Raft Sketch Prove.

• 1:18:46Tim Scarfe?

  Yeah.

• 1:18:47Speaker 00

  And so that's one direction, theorem proving, formal theorem proving and also informal theorem proving. There are also a lot of other interesting questions which are less explored. One direction that is really fascinating is sort of open ended exploration. If you think of what's really needed in mathematics, what can AI contribute? One big opportunity is in coming up with better conjectures, creatively coming up with better goals that you want to prove, not just the proofs themselves, but, but yeah, also the, also the statements of the theorems.

• 1:19:30Speaker 00

  So that's a direction that I think is extremely important. But unfortunately, there hasn't been that much on that so far. But there are several research groups that are very interested in that problem as well. And, and so, for example, there are these efforts where, you know, you have a, so Noah Goodman had this really nice recent paper on using intrinsic motivation to, to drive a prover. So the idea there is that you are, you have these two agents. So you have an agent that is coming up with new claims and you have a different agent that is trying to prove them.

• 1:20:12Speaker 00

  And so really, you know, you have this interplay between the process of conjecturing and the process of proving, which is really what happens in, in mathematics, if you think of it.

• 1:20:22Tim Scarfe?

  So last night I read your Copra paper, which, which was really, really interesting. And I mean, you already spoke about lean in, in high level terms, but maybe you could go into a little bit more detail. But essentially it was an algorithm to, you know, you have a theorem and then you have all of these obligations. And then the algorithm would resolve using a language model these lemmas. And then it would then recursively kind of call itself until it ran out of obligations. And I guess the heuristic part was was using the language model to find an appropriate lema from this lema database. And it's a fascinating architecture. Can you tell us about that?

• 1:21:06Speaker 00

  Sure. So one thing here that is in common with all of the other lean theorem improving or formal theorem improving efforts is that there is this overall structure of a formal prover. And the idea there is that you have a goal that you're starting out with, a top level theorem that you're starting out with. And then you're progressively applying these tactics, which are simplifying this goal into subgoals. Right? And after a while, assuming you have selected a good set of sequence of tactics, you have no more goal left to prove, and then you're done. Your theorem has been proved, QVD. Right? So this is just lean.

• 1:21:50Speaker 00

  This has nothing to do with AI. Now, the question is that how can you use AI to select tactics in a smart way? And there, the COPRA paper made a few contributions. One was that you are just using a large language model without any kind of fine tuning. You were just prompting it to guess tactics. And this is different from prior work where folks used models that were explicitly fine tuned on proof data, formal proof data. Now, what was sort of remarkable to us was that even just a black box model could predict

• 1:22:35Speaker 00

  reasonable tactics for for this sort of formal proof, even though the language is fairly esoteric. Now, an important point, though, is that it wasn't enough to just query the Language model, you also had to do this LLM modulo thing where you are getting the tactic predicted by the LLM and then you are using that to actually change the, you're executing that tactic in the underlying lean framework. And then you're getting back a new state, a new set of obligations to prove, and then you're going forward with that, right? And the LLM can actually see what the current obligations are and also actually some, it has some memory from the, from the past.

• 1:23:18Speaker 00

  And all of this is plugged into a bigger search, right? And this search process is doing backtracking, it's recording what failed, what didn't work, or what worked and what failed. And all of that information is being used to guide the generation process of the LLM. So that is one idea. And then the other idea is that you are doing retrieval. Now here, the intuition is that when you're doing math, typically you are using definitions from other projects and you're using lemmas from other projects. And the idea of using these, these sorts of external knowledge bases, this was used,

• 1:24:00Speaker 00

  originally introduced in this model called Reprover, led by Caillou Young, who's now at, at Meta, doing AI for maths research. And this Reprover model was fine tuned, but here what we wanted to explore was that could we just use a large language model in a few shot way to do the same sort of thing? And we found that, yes, it was able to use this retrieved knowledge from external databases. And so what that shows really is that in-context learning can go a long way, even in this sort of very esoteric setting of doing formal theorem proving.

• 1:24:39Tim Scarfe?

  Yes, and you, you tried it on GPT 3.5 Turbo and GPT 4. You noticed that there was a significant improvement of GPT 4. You, you ablated the retrieval. And the retrieval helped dramatically. I think you limited it to about sixty steps, but presumably if you went for longer, it would have been even better. And the backtracking presumably had some notion of I'm in a bad state, now I'm going to go back. How did that work?

• 1:25:06Speaker 00

  So the good thing about a formal framework like lean is that you are getting information about what is a, what kind of state is bad, right? So if you are, if you are at a certain state of the proof, you have a certain set of obligations to prove, now you take a tactic that's not helping, or in fact, that is just not applicable in the current state, then you're going to get feedback. Or for example, if you're finding that you are cycling back to something that you have already, a state that you had already seen, and so you're basically going to end up with an infinite loop in the, in the state space, then that is also something that you should avoid, right?

• 1:25:47Speaker 00

  And this kind of information you can get by explicitly embedding the LLM inside a broader search process. I think again, though, that the, that the main finding in that paper is that in-context learning can be interesting even in this setting. Now, we limited it to sixty because we were working with an academic compute budget, and also GPT-4 was fairly expensive at that time. But I think that going forward, as the models get cheaper, it would be really interesting to see how far this sort of LLM plus search plus external grounding through, through lean or other kinds of frameworks, how far this can be pushed.

• 1:26:30Speaker 00

  I think that it can actually go a long way, especially if you are willing to do expert iteration, which is that you collect data and then you use that to fine-tune the model further and you carry on like that.

• 1:26:40Tim Scarfe?

  Couple of things. So I'm interested in this concept of reachability.

• 1:26:43Speaker 00

  Uh huh.

• 1:26:44Tim Scarfe?

  So, so you have a whole bunch of tactics in a database, and then there's, there's some notion that we've been kind of pointing to about the convex hull of the tactics giving you some reachable space.

• 1:26:56Speaker 00

  That's right.

• 1:26:57Tim Scarfe?

  So, so maybe we should talk about that convex hull, but presumably there would be examples of the theorems that have a goal state which is not reachable with the tactics. I mean, could you talk through that?

• 1:27:08Speaker 00

  Right, so there are really low-level tactics that would.

• 1:27:14Speaker 00

  Enable you to really find anything. It's just that the there may exist a sequence of tactics that lead you to that goal state. But it may be so long and so complicated that your AI may not be able to find it. And that happens all the time. There are lots of statements that we are unable to prove. Now, I think one interesting question is that do you

• 1:27:43Speaker 00

  expect to do better if you were able to abstract these sorts of low level tactics into higher level tactics? And I think the answer is yes, right? If you think of how a mathematics student progresses, you start with really basic algebra and and or maybe even before that you start with arithmetic. And then you you get to algebra and then suddenly you have this big leap. And then you get to calculus and you know, you you learn probability. And then you get even more abstract. You go to complex numbers and and so there is this hierarchy of abstractions that a human student goes through while learning mathematics.

• 1:28:25Speaker 00

  And the purpose of these abstractions is that you are able to be more robust. You're able to handle more and more kinds of problems. So you're unifying a lot of sort of point solutions into into general solutions. And I can imagine that that approach would be valuable even in this context of AI for math, that you would start with some low level set of tactics. But then maybe in this kind of Dreamcutter way, you're going to discover more abstract tactics. And then you would be using those to do more succinct proofs. And then stuff would just explode at some point that you you'd be discovering new kinds of mathematics.

• 1:29:04Tim Scarfe?

  How does the resolution play into the leakiness? I mean, I'm certainly thinking about in physics, for example, there are, you know, Newtonian mechanics and relativity and so on. Do you do you introduce leakiness by relying on high level abstractions?

• 1:29:17Speaker 00

  Not in this setting of formal proofs. And the reason is that the way a framework like Lean or other there are other ones as well. These frameworks are architected. You have to have certainty all the way through. Otherwise, your proof is not going to be accepted. And so even if you are at a higher level of abstraction, you are. Going to have implementations of that high level primitive in terms of lower level primitives that actually are sound. Now that said, you could certainly imagine versions of this where that is not the case.

• 1:29:59Speaker 00

  So for instance, you could imagine a version of AI for mathematics where there are some low level or some proof obligations that are just sort of empirical, right? Imagine that I'm making a statement that, I don't know, maybe this is not a universal mathematical law, but maybe it's a property of a certain place and time, right? So maybe you are, you have a predicate that you are just evaluating empirically. Now, you could give it mathematical meaning by making it into a probabilistic predicate, but you don't know that, you know, the distribution that you have selected is the right one, right?

• 1:30:40Speaker 00

  So in that case, what would happen is that the more high level your resolution or the coarser your resolution, the more uncertainty there would be. But you would still have some amount of, if you're using, you know, formal mathematics above that level, you would still have some amount of assurance about the claims that you are making. So it would be not that different from, you know, when you're using math in a natural science. There are empirical observations that you're making and there is noise in that, right? But you are at some point abstracting them into this cleaner mathematical model

• 1:31:25Speaker 00

  and all the inferences that you're making based on that model, they're conditioned on your assumptions, your modeling being correct, right? And I think that it's not that different from this, that if you have two coarse grained a model.

• 1:31:41Speaker 00

  You are going to have, you know, more uncertainty regarding your conclusions, right? It's not a zero one, that it has to be either fully certain or completely uncertain.

• 1:31:51Tim Scarfe?

  I was speaking with David Spivak recently. He's very well known in applied category theory. And he was kind of saying that our entire epistemic framework almost derives from the questions that we ask. And I wonder whether it's a similar thing when we talk about theorems and the utility of theorems and the role of humans in creating these theorems. There must be some kind of, you know, reason why we're asking these questions. Where does that come from?

• 1:32:18Speaker 00

  I think that for a lot of mathematics, it's been inspired by the goal of solving real world problems. If you think of why people came up with geometry, why people came up with calculus, I think there was a very pragmatic goal that you wanted to understand how the world works and you wanted to then apply to do new things, to solve real world engineering challenges. And so I think that that's often the starting point. But then, of course, you know, there's this motivation of elegance as well, and curiosity,

• 1:33:01Speaker 00

  that you want to have elegant unified solutions rather than point solutions that are just hacked up. And you also are curious that, okay, so I have made these sorts of assumptions in this definition. What if I change these definitions in this way? What would happen? And I feel like if you just combine these ideas, the idea of modeling phenomena that are visible in our day to day lives and

• 1:33:40Speaker 00

  Combine that with these motivations of curiosity where you are just asking, okay, what if I did this, what would happen? And unification of point solutions into something more abstract. I think that you would get to a lot of mathematics that way.

• 1:33:56Tim Scarfe?

  Could you expand on that a tiny bit? So what, if you could break this down, what makes a really good mathematical theorem?

• 1:34:02Speaker 00

  I am not a professional mathematician, so I'm probably not the best person to ask this question. Maybe I can talk about computer science and, and I can try to answer this question for, let's say, theoretical computer science papers because I come from that community. So there, I would say that one question is whether or not this, there's this question of interestingness.

• 1:34:30Tim Scarfe?

  Yes, yes.

• 1:34:31Speaker 00

  So what is interesting? I think that it should be clean, the problem that you're trying to solve. It should be a clean statement. It shouldn't be that I've come up with this bizarro definition with N different cases and then I want to prove a certain theorem about that, right? So it should be something that is relatively succinct, elegant. And then it should be novel. So if it feels like I have seen N versions of this before and I can take a proof for one of those previous models and this, tweak it a little bit, and then the proof comes out, that's just not worth pursuing.

• 1:35:16Speaker 00

  So I think novelty and elegance are big criteria. Then I would say that in computer science specifically, utility is a consideration as well. The reason why computer scientists often care about certain kinds of theory is that that theory models real world computational processes. So there was an interest in, in say,

• 1:35:45Speaker 00

  Online algorithms because you know there were there were many practical computer systems that needed to process data online. There was an interest in interest in algorithmic game theory because the internet came about. And then all of a sudden, we were departing from this traditional centralized view of the of the computational world. Instead, the internet was this massive computer and you had all these agents that were driven by their own objectives, but they were coordinating using this, let's say, an ad auction or or any number of other kinds of online coordination mechanisms. Right.

• 1:36:26Speaker 00

  And that led to all of this interesting work on on algorithmic game theory where it was asked that, all right, so let's say that I have these K different agents and they are arriving at an equilibrium, right, which is this this market, right, the equilibrium of the market. But I want to now ask, in contrast to traditional game theory, can I reach an equilibrium in polynomial time? Right? Is this equilibrium not only reachable but computationally tractable to reach? So the way I see it, a lot of interesting computer science theory has happened by taking

• 1:37:08Speaker 00

  these sorts of longstanding principles in math and and prior computer science and then adapting them to these new settings, new models, which are inspired by practical problems on the ground in in in computer systems.

• 1:37:28Tim Scarfe?

  Game theory is a beautiful example, absolutely beautiful. I mean, I'm I'm interested in agent C. And that's a wonderful example of one of these just it's a phenomenon in the natural world.

• 1:37:39Speaker 00

  Yes.

• 1:37:40Tim Scarfe?

  And it beautifully demarcates certain dynamics of of behavior and so on. And then we create this game theory thing, which is also using the concept of an agent. And it's it has this unreasonable effectiveness of modeling many, you know, complex systems. Even though we choose to model the agents at different scales and even mixing different scales inside a model. But coming back to your definition of a really good theorem, though, you said clean. And I think you were talking about like parsimony, but you know, Chomsky says that L L M's aren't a theory of of language. Because they they don't have that clean demarcation. They don't, it doesn't demarcate what he thinks is language versus anything else, like an impossible language or something around it. So is there something about this this this demarcation?

• 1:38:24Speaker 00

  I think that L L M's would be, would produce whatever is, it's there in the in the training set, right? And and and some amount of composition thereof. So I think that if an L L M was primarily trained on beautiful theorems and beautiful literature. I think that you would see certain, certain aspects of that in the the text that they generate as well. However, I think that that clean, that elegance also, it's subtle.

• 1:39:03Speaker 00

  It's not just about following certain high level motifs of beauty, but it's also about being consistent. So a lot of the times, for example, when I use L L M's for writing, I find that, okay, this paragraph is really well written, nice. But then the next paragraph is somewhat different. It's it may be, you know, individually fine, but then when I put the two together, it just becomes something horrendous. Right? So I think that this idea of elegance, it's it's a sort of a global notion. But it's not just that, you know, little pieces of the theorem are cleanly stated. And therefore, the the entirety is cleanly stated as well.

• 1:39:44Speaker 00

  So I think that, to me, it's a very open question, that can an L L M come up with with elegant theorem statements?

• 1:39:55Speaker 00

  I don't know that the answer is is no or or yes.

• 1:40:00Tim Scarfe?

  And and just to close this off, because you you did sketch out in your ablation going all the way just to a zero shot, you know, blank slate, GPT four, or it wasn't GPT four, wasn't it? And I think it got something like 2.3% if I remember correctly, and then it sort of ranged all the way up to about 30% with with with all of this copper algorithm and the retrieval and the backtracking. The thing is that there's always this nagging thing in the back of our minds about the test set contamination.

• 1:40:27Speaker 00

  That's right.

• 1:40:27Tim Scarfe?

  And you and you did a little bit of work on on that. Could you talk talk about that?

• 1:40:32Speaker 00

  Yes, so this is a very difficult issue with LLLM based approach. There is always this worry that that the results you are seeing are because of contamination. Now, we did what we could to address this issue. And what that means is that so first we showed that if you strip out all of the extra pieces that we added, we just asked the LLM to go and produce the proof end to end, it wasn't successful. It got something like 2% as you as you mentioned. We also looked at a lot of the proofs that were generated and we looked very hard for

• 1:41:17Speaker 00

  for similar examples in the on the internet and we just didn't find any. So that is another indicator that the proofs that we were seeing were not just an artifact of contamination. Now that said, contamination could have played an indirect role. Maybe there are similar kinds of problems that the LLM has seen before that we just couldn't find. That's definitely a possibility. But I feel like at this point of history in AI research, we just have to be very aware of this risk, but still continue using LLMs.

• 1:41:57Tim Scarfe?

  Yes, when I spoke with Sabaral, he said when he was solving a planning problem in Blocks World, he made a mystery Blocks World version where he just scrambled all of the tokens. And apparently that that did cause a significant deterioration in performance. But it's so slippery, isn't it? It's very, very difficult. Yeah.

• 1:42:15Speaker 00

  Yes. Yes, on standard benchmarks, I think this is a big risk. Now, I think that one could imagine using synthetic benchmarks. Now, the approach that we took in the COPRA paper, I just don't think it's well designed for completely arbitrary synthetic benchmarks, because the whole point was that the prior knowledge inside the LLM helps with finding new tactics. But there is this other paper that we recently worked on, which is, it involves concept learning using an LLM in the context of symbolic regression.

• 1:42:55Speaker 00

  And there, we also used an LLM inside the search framework. It's this evolutionary search in this process, in that case. And I mentioned this paper earlier in our conversation. You are actually using the LLM to do concept abstraction as well. And you're using these abstract concepts to guide the search process. Now, in that case, we did experimentation with synthetic problems and we found that the LLM does help there as well. And the reason is that even if you are not using any sort of prior knowledge, the abstraction ability of the LLM,

• 1:43:36Speaker 00

  that is to come up with high-level concepts based on some examples of text, that is helpful. But that's not a part of the COPRA approach. And so there is no reason to believe that if you just come up with a completely synthetic. Problem, Copra would be able to do that well.

• 1:43:54Tim Scarfe?

  Amazing. And before we go, where can people find out more about you?

• 1:43:58Speaker 00

  Just Google my name and then you'll get to my website and all of my papers are are linked from there. And I also have a Twitter account, just Swarat. But if you really want to discuss something technical, just send me a message and I'd be happy to chat more.

• 1:44:19Tim Scarfe?

  Amazing. And we'll be putting the papers up on the screen as you mentioned it. Swarat, this has been a brilliant conversation. Thank you so much for joining us.

• 1:44:26Speaker 00

  Thank you so much for having me. I loved it as well.