Building an AI Mathematician with Carina Hong - #754

0:00I'd like to thank our friends at Capital One for sponsoring today's episode. Capital One's tech team isn't just talking about multi-agenticentic AI. they already deployed one. It's called Chat Concierge and it's simplifying car shopping. Using self-reflection and layered reasoning with live API checks, it doesn't just help buyers find a car they love, it helps schedule a test drive, get pre-approved for financing, and estimate trade-in value. Advanced, intuitive, and deployed. That's how they stack. That's technology at Capital One.

0:34This podcast is sponsored by Google. Hey folks, I'm Amar, product and design lead at Google DeepMind. We just launched a revamped vibe coding experience in AI Studio that lets you mix and match AI capabilities to turn your ideas into reality faster than ever. Just describe your app and Gemini will automatically wire up the right models and APIs for you. And if you need a spark, hit I'm feeling lucky and we'll help you get started. Head to ai.studio slash build to create your first app. Math and coding are two important, perhaps the two biggest parts of digital work. And coding is heavily invested.

1:15Math is not. Not that math is not trackable, but that math has not been turned into programming language yet. And there will be new markets and new use cases that get unlocked because of this.

1:41All right, everyone, welcome to another episode of the Twin Wall AI podcast. I am your host, Sam Charrington. Today, I'm joined by Karina Hong. Karina is founder and CEO at Axiom. Before we get going, be sure to take a moment to hit that subscribe button wherever you're listening to today's show. Karina, welcome to the podcast. Thank you for having me. Great to be here. I'm excited to dig into our conversation. We'll be talking about mathematical reasoning, which is what you are working on there at Axiom. And it is a very timely topic. Before we dig in, I'd love to have you share a little bit about your background.

2:20I love math as long as I can remember, when most people don't. And I feel like Olympic math training gives you this sense of like constant dopamine hit. Like you solve a problem and then you feel so good about yourself and then you move on to the next one. A bit later, I went to MIT and started a research mathematics career. And that was a lot more pain and suffering. You usually are stuck on a problem for months. And I remember I was working on a really hard problem for about like half a year. And I would meet with my advisor every week and have nothing to report. That's kind of the life of a research mathematician.

2:59What particular field in mathematics? Yeah, so I work on number theory and combinatorics. A lot of people who work in combinatorics come from the Olympic math background, so they can solve problems a lot faster than other combinatorics researchers. But number theory, hopefully, is better. You can read a lot of literature and make really interesting contributions without having this sort of outlier problem-solving skill. I took a real analysis class in grad school, and I think that was about enough for me. I love graduate analysis. I remember back then at the graduate analysis class, I don't know if it's because no one is quite following.

3:39We were just like passing note and saying that the professor looks like Winnie the Pooh.

3:48That must mean that the class was a lot easier for you than it was for me. Or maybe we're just completely lost. I don't know. Nice. So you're working on this hard problem at MIT. It took you half a year. Yeah. And then I think I realized at one point that wouldn't be great if you can just let your intuitions take you. You have some lemma that you want to prove instead of being stuck there constantly verifying the details. Wouldn't it be great to just, you know, think that there's a high chance if your intuition is right, that the lemma is correct and move on to the next one? A bit like, I mean, those creative AI arts startups, right?

4:32Like Pika, like you want to put a fox on the cartoon and then have the fox talk to a bunny instead of actually sketching it out like the cartoon creators. Say it and let it be so. Yeah, exactly. I think that might be the difference between, say, Terry Tao and Karina Hong, which is perhaps both can have some sort of lemma they want to prove, but Terry can just move on to the next one. And Karina needs to be stuck there for about six months before moving to the next one. You know, one thing that strikes me about what you're doing is that we seem to be in a particular moment with regards to math and AI and, you know, this confluence of math and reasoning.

5:16I recently had Christian Zegedi on the podcast. Like a week after we talked, he left to start another or he started another startup, Math Inc, to focus in this area. There's also Harmonic working on this area and probably Untold Others. I think the first thing I want to get your take on is why now? Why is so much investment and effort more broadly going into mathematics and AI? I think what we feel at Axiom is the timing is right. And the timing is right because of three reasons. We believe in AI mathematician being built by bringing three fields together, and that's AI, programming languages, and math.

6:03If you look at the current landscape, informal models are really good at reasoning. They're really good at math and coding. Informal models like LLMs. Yeah, so informal models, large language models, the old series of OpenAI really marked an era of post-training, reasoning, reinforcement learning. Like this is great technique breakthroughs. So that's number one. Number two is on the forebone side. Lean 4, which was rolled out September 2023, has been widely celebrated by the community. the number of people who learn Lean, use Lean on a daily basis have pretty much expanded. And a lot of mathematicians, field medalists are joining force and using Lean and seeing, okay, well, how can this formal language, this programming language help us verify math and, you know, hopefully have more and more digitalized mathematics.

7:03So that's number two. Number three, I would say, and this is maybe like Axiom's hot take, is by turning math into programming language, you really need a lot of the code gen techniques. And code generation has been crossing a threshold. We have seen really impressive performance of reinforcement applied to coding. And the hope is by turning math proofs into programming language and using a lot of the code gen techniques that we think are a bit kind of overlooked, we can have really amazing performance gains on math as well. So three things are really converging together. Are these code gen techniques overlooked in code gen or overlooked in application to math?

7:45In application to math. And for good reasons. If you look at, for example, there are probably more than a trillion tokens of Python code in the Internet. Yeah, that's pretty, that's a lower bound. I think there are about 10 million tokens of Lean code. So we have the Lean universe, which is the largest Lean dataset. The developer of Lean universe is currently at Axiom. And we kind of are estimating, wow, there is a 100 ,000 times data gap. And that's ridiculous. Like scaling can't quite work with this amount of data scarcity. Talk a little bit about Lean. I see that come up frequently in the conversation around mathematical reasoners.

8:27You know, it's a programming language. You know, what does it kind of look and feel like? You know, what problems is it trying to solve? Who's using it? Yeah, 100%. I think the magic of Lean is human mathematicians have been doing mathematical reasoning on pen and paper, literally, for thousands of years. And because of how they are trained, they do it in a very rigorous way. It is by humans to, you know, make sure that each step strictly follows a previous one. Lean makes this more like how computer programs work. You can write a proof in Lean, and the Lean proof will hopefully compile if the proof is correct.

9:07And if it's not, then it will report a bug, say a bug at line 37. Then you look at line 37 and you try to analyze exactly what the bug is about. It can be that you get the syntax wrong. So like every Python beginner gets the syntax wrong sometimes. It could be, you know, not the mathematical merit of the proof that's wrong, but just the syntax. Or it can be that the math is just wrong. And there's like a third kind of problem that's a bit more stubborn. That is, there's something about the types that are not matching. So Lint is built on something called dependency type theory. So then you have types associated to every object.

9:50And sometimes these sort of bugs are harder to fix. So by trying to feed the error message back into, say, your prompt, you can do inference with feedback and you can do the standard like RLEF type of stuff. And hopefully you can have the machine see more lean, learn more lean and generate more lean. So it kind of stops making those mistakes. That's at the syntax level. But whenever there is a mistake, you can be more confident that something about the math is wrong. And what does it look like? You know, I'm thinking about the math that we see in papers. And I'm also thinking about one of the first computer programming languages I learned in education was APL.

10:40Which has all kind of like weird symbols and stuff like that. And I'm wondering if Lean looks like that. Yeah, Lean has some interesting math symbols, like the inverse A, which is like for all. It basically looks like a programming language. It's definitely not quite readable. APL looked a little bit like hieroglyphics. Oh, okay. Yeah, it's very interesting to think about the abstraction of these languages, like with natural language being very readable, but not quite easy to compute, right? You can't actually do computation with English. and then you kind of go down the stack. You have programming language like Python, like Lean.

11:21We now think about, for example, Python being kind of translated almost to an intermediary language and then intermediary language and eventually the machine code that is doing the actual computation that's going down the stack. But it doesn't quite, there's some local examples where it goes up the stack a little, but it doesn't kind of like go fully up back to the Python stack. That's not how like compilers like work. On the other hand, if you think about the highest stack being like natural language math proof, and at the bottom you have like Lean proof, and in the middle you have things that are needed to convert, to formalize a natural language proof into Lean.

12:04You have maybe finer and finer blueprints, like math that are 10 times longer than the original paragraph of proof, it actually is able to go down and up the stack freely. And I think that's quite interesting. So auto-formalization is for a model to convert English proof into lean proof, and informalization is going back up. So then you have like a full bidirectional circle, which is very interesting because then you have human mathematicians, reasoning, high-level intuitions at the English layer, And then lean is proving at the bottom layer. And these sort of formal proving signals then can feed back in to advise the mathematician, okay, well, maybe this part of verification isn't quite working, to then guide the continuation of these high-level intuition.

12:58That process is very fun. It can actually be transferred to a lot of other settings as well, if you think about formal verification in other contexts, such as chip design, such as code verification. Those are quite interesting examples. Are you able to say conclusively that if a program compiles and runs in Lean, then the proof is without error mathematically? It seems like that in and of itself would be a research topic or a significant achievement, like having that one-to-one mapping between validity and the lean space and validity and the mathematical space? Yeah, so I think it's quite interesting that a lot of the mistakes actually happen at a misformalization of the statement.

13:44So if you're sure that your statement is like correctly formalized and your proof compiles, then congratulations, you have a correct proof. Now, there might be multiple correct proofs and there might be, for the same proof, multiple ways to write it in lean. So it's not one-to-one matching per se, but you do have the sort of provable guarantee that if your statement is correctly formalized and then you have a working lean program, then you have to prove right there. You talked a little bit about like the three elements that are coming together to make this an interesting time for mathematical reasoning.

14:23Lean being one of those pieces. And then, you know, we're talking now about auto-formalization like does auto-formalization is that is that part of lean as a package or is it something that folks are working on that kind of utilizes lean as a foundation and what's the current state of auto-formalization from your perspective we think of auto-formalization which is the process again for a model to convert natural language mass proofs into lean it's like surprisingly very hard. I mean, it's not just a translation problem. So I think there are two ways to think about other formalization. One is as a data bet, right?

15:05So you can convert a lot of math data in the informal space to the formal space. And then you kind of solve the data scarcity problem of formal math data. And so one way to think about it is it's a way to gather data. The other way to think about it is it is also a core technology in and itself. So auto-formalization and proving have very sort of entangled capabilities. Like I think a model that can auto-formalize very well likely can do better in proving and the other way around. So we strictly don't think that auto-formalization and proving should be trained separately. Like they should be in one loop.

15:44They should be in one model. So I think these are the two ways we think of auto-formalization. If you look at the entire mathematical archive, there are about like 30 to 70 million statements and proofs pairs. And none of these are like, you know, in lean. I mean, very basic stuff and domains that happen to be the domains that the lean developers, the lean MATLAB contributors like, such as algebraic number theory. Those are in, but like differential topology, for example, is not in. If you can do auto-formalization well, you can get these very high quality seed data at all levels of difficulties of math.

16:27And then you can convert these seed data into even more synthetic data. Then you can try to close the data gap we just talked about of math and coding. Lacking those, how do you approach closing that data gap? Yeah, I think auto-formalization is important. We also think that the other parts of, you know, the synthetic data generation, like after you have a lot of high quality data, how do you make it 100 times, 1000 times more? I think those are interesting as well. Maybe I'm not hearing this correctly, but part of what I'm hearing there is that we need more data to do to like do auto formalization.

17:06But then more data and auto formalization is needed to do proving. But, you know, in the first place, how do we get the data required to do auto formalization or more broadly, what approach are you taking to tackle auto formalization? I think it is a co-start problem, right? Like because machines have not seen enough lean, they don't know how to do lean well. So you do have that sort of like co-start chicken and egg problem. I think there are mature research techniques out there in the publication space that are trying to solve this problem by bringing the gap between natural language proofs and formal proofs closer.

17:49We think, you know, broadly reinforcement learning is an important part of that. How do you see RL playing in this space? So we have seen really amazing scores on various benchmarks from models that use reinforcement learning to do proving well. We have seen, for example, Seed Prover is a really strong paper by Dan Seed Foundation. There's that Hilbert Prover. Before that, there is Kimina Prover, Dipsic Prover. We have seen reinforcement learning applied on formal math having pretty good results. And is there a general approach that is being taken to apply RL to formal math? I think people try different things, actually.

18:38There are many different sort of designs. There are more Monte Carlo Tree Search-based models, and there are more sort of creative agent design one can do. And there are interesting RL training recipes that each lab chooses to take. I think it's more like an art than a science. How do folks approach objective design with proofs? Is there a kind of standard way to think about that? Yeah, I think there is a difficulty. I think it's that the signal can be quite fast, right? So once the proof gets incredibly complicated, it's a little bit hard to get it to work. So some people do see that as a challenge.

19:20But I mean, it's a very rapidly evolving field and people have been trying to, you know, define good curriculums for the model to hill climb. So currently, math models, formal math models are doing quite well. In the high school Olympiad math level, you have seen two formal models actually do spectacularly in the IMO. And then beyond that, you can have more fine-grained curriculum to try to teach the model harder and harder math, actually across two axes. One is how abstract the mathematical object is. The other one is how sort of eureka moment, how creative the proof is. And IMO is something that is low abstraction, high creativity, requires a lot of genuine, like, you know, innovative approach.

20:08And then you have, for example, PhD qualifying exam. That could be relatively straightforward if you know all the concepts. And that's at a higher abstraction level than IMO. And you can define curriculums for the model to do better and better on both axes. And what are the two models that have done well on the IMO through formal methods? I think, for example, the seed prover model is doing pretty well and Aristotle is also doing pretty well. What can you say about those models? Like what approaches have they taken that you think differentiate them among other attempts at this? I think so. Both are industry labs with more compute and data budget resources.

20:50Always helps. Always helps. We have seen, for example, the Aristotle one being more Monte Carlo tree search based. And then the SeedProver one having pretty, I think, intricate designs, system design. So they have a lemma pool, they have very different sort of designs for their light, medium and heavy inference tiers. So I think really there are many ways. And eventually, I think people will just try everything and see like which one works better. And so taking it back to Axiom, it sounds like you've got this, you know, this big problem that you're going after and a lot of tools in various tool chests to kind of apply to the problem, a lot of levers to pull.

21:39Like, how do you think about, you know, where you invest or, you know, what bets you place or what needs to work well for you in order to be successful? Like, what general direction are you taking through all this? We believe in a system that can prove and conjecture and self-improve by having the prover and conjecture talk to each other. I think verification, which, you know, exists here and in the domain of formal math and self-play really tie together. You can have the prover as the reward signals for the conjecture. And that is not a new idea. It hasn't been an idea that worked well in other domains.

22:25before. And we want to take pretty bold bets on the data end as well through auto-formalization and synthetic data generation. So I think of like our approach as sort of, we do a lot of things and they all eventually fit together pretty nicely and cognizantly. You know, use auto-formalization to generate a lot of data and to expand that data by a hundred times, a thousand times through synthetic data generation methods, and then have a really strong prover that shows capabilities across benchmarks that test different capabilities, do benchmark and evaluation very carefully, and then eventually have the prover talk to the conjecture for the conjecture to propose new problems and new curriculums, and the prover to then prove it and then form like a self-improving loop as the prototype of self-improving AI.

23:22And do you approach all of those in parallel or is there a particular starting place and that's kind of foundational that you tackle first? we currently are doing more than one thing for sure uh but as you you know as you're you're right startup is always like a kind of constraint optimization problem um we currently feel like um the the the you know the different parts are all very important um and by kind of not you know like constantly thinking about these these ideas and staffing those teams um actually it's a very kind of cohesive picture even though like obviously for an early stage startup there's too many ideas for us to to execute all at once but we're trying our best you mentioned that one of the elements of a solution that you think is important is self-play i think we've seen some significant successes there through like the alpha go alpha zero style of models like do you once you have the pieces is it you know a straightforward thing to set them against each other and say you know go off and talk to one another and figure this out or is there also a lot of you know technical challenges just in like setting up your self play you know system and environments for sure I think that is there are quite a few you know difficulties there um you know for example right if you okay if they just cannot prove like is is it the fault of the conjecture or is it the fault of the the prover is it that okay well this problem is just bad or is it just that it's a good problem then your prover like i think disentangling them there are a lot of like open research directions i think that are under under explored but i think like the general idea, which I think is quite creative and novel, is that through math, we can try all these things.

25:30It's a sandbox for trying self-improving AI. And the conjecture proposes new conjectures. And based on the current knowledge base of math and that knowledge base is evolving, it is expanding and contracting, expanding because of new things being proven, contracting because, well, maybe some of them are, you know, low merit. And then provers prove or disprove these conjectures. The results added back to the knowledge base and the cycle repeats and expanding the body of knowledge. And I think we're going to see some difficulties in judging what is good mathematics from, you know, by the model, you know, what is elegance?

26:13what is novelty? There are certain sort of rough proxy measures that we can try, but not like a conclusive, you know, definition. I mean, there are other papers out there. I think Yosha Bengio has this paper on, you know, looking at building AI mathematicians through the lens of compression. Well, is the first order logic viewpoint satisfying or not really, right? If you have a theorem and then because of including that in your knowledge base many theorems are then born um is that is that you know is that end all be all for like elegance um you know there may be probably some statements that are extremely elegant from the perspective of human mathematicians um that don't actually that kind of like conclude things right like like close like a thread like you know, nuke a field after we know this, like there's nothing new to be born.

27:10So I think that might be a human mathematician sort of like alignment problem with like what is what is good? Like taste, I think is still very, very hard to measure. It tastes is something that I think we're grappling with across a lot of different fields in AI, and it's not clear how we necessarily get there beyond more data that somehow exemplifies better taste, which kind of brings us back to the data problem in your field. And I think the data problem in our field is like for the really not so complicated, not like frontier research math, like just undergrad textbook, there haven't been that much data.

27:51We're having this conversation in the context of, you know, the post-LLM, you know, AI era, if that's what we want to call it. And a lot of that was kind of this unlock of self-supervision through, you know, next token prediction, that kind of thing. Like, do you see an opportunity for like self-supervised data exploitation in mathematics? Like we've got this tremendous, you know, there are tons of papers, You know, many of them are digitized in mathematics. Even the, you know, the ML papers that we look at, like, have lots of math in them. You know, there's narrative about those proofs. You know, can we use that without necessarily requiring Axiom or Math, Inc.

28:42or everyone else to, like, take those manually, convert them into lean and, like, build these supervised data sets? Do you think anything's there? We at Axiom actually believe in the informal part of reasoning being also important in the loop. I think if you have the informal data and quite aligned with your formal proof and you train them on the verified pairs, it's great. We think that's a good idea. If you look at even not talking about math verification, just talking about Python, right? There is this paper, R-star Math, I remember was earlier this year in April or something. Microsoft Asia paper, they see that a small model can achieve on par with O1 performance.

29:27Back then, O1 was still very, very impressive. It's amazing how fast the field moves. But training on the pair data of informal solution to high school math problems in the Python one, yeah, I think that's interesting, right? And you also see papers like Lego Prover trying to have the informal proof as aligned with the formal proof as possible. We don't believe in only formal. We don't believe in purely informal for sure. We believe in kind of taking a hybrid approach and the strength of the informal models, especially maybe in high-level intuitions that could be very interesting to do that together with the formal side as well.