Short answer: Carina says LLMs write natural-language proofs that are hard to verify, while Axiom's output is an executable Lean program, so no LLM or human judge is needed. She expects formal systems to scale better on harder problems.
Watch this answer from Episode 22 (starts at 15:18) · Episode 22 notes and transcript
From Episode 22: Let's do the Math!, starting at 15:18.
Jordan Metzner [15:18]: Awesome. How these, like, LLMs compare to, like, figuring out math versus, like, what you guys are doing? Because I think that's, like you know, this is the whole clip of, like, what's exciting. Right? Like, if anybody doesn't know about math and they have no idea what you're doing and they're just like a layman who's into tech and AI, and they say, okay, what is this what's the difference between this and ChatGPT? Like, what's the difference between like an LLM and what you guys are trying to do?
Carina [15:40]: Large language models are doing math in the informal space. They produce proofs in natural language that is English, and they will give you a multistep reasoning traces if they're a deep sea, but they will only give you, say, like, numerical answer if you're, change your beauty. And the numerical answer is a verifiable output, which is something that you can, grade. Like, 971 is 971. The problem is without the sort of very detailed step by step deduction, it's hard to verify all these intermediate reasoning traces. So it's very difficult for an expert or a layman to know whether there might be a hidden bug among, like, a 3,000 line math proof. On the other hand, what Axiom, the informal formal hybrid prover system we are building is to make sure that the output we give are programmatically verified. Verified. There is a Lean program underneath it, and the Lean program is executable. So in a way, we do not need an LLM judge or a human judge.
Carina [16:45]: We just run it like you run a Python computer program. I think that's the biggest difference between these formal models and the large language models. In the formal model states, we know that Google DeepMind AlphaProof system, the system that got Silver Medal, actually, one score below the gold cutoff is a formal system. This year, they have the Gemini system, and also OpenAI has the strawberry team's IMO team. These are informal system that got really good scores on IMO. Difficulty is IMO and other Olympiad math benchmarks sort of half a curriculum, a set sort of syllabus of things that they're testing all, which limits their search space quite a bit. When the proof gets very complex and multistep, requires really hard math capability, and we believe that formal system gonna be extremely helpful in scaling, continuing to scale on those harder problems.
Jordan Metzner [17:43]: That's that's so so cool. Obviously, math's the backbone of kind of all technology, so it seems like there's some, mathematical breakthroughs on the edge here that, once these things really get their power, they can really turn out some new opportunities. That's super cool. Alright, Carina. Well, thank you for telling us about Axiom.
