Mehta: AlphaProof Uses Test-Time RL on Problem Variations to Find Proofs
Rishi Mehta · No Priors Ep. 90 | With Google's DeepMind's AlphaProof Team · Nov 14, 2024 · at 8:13
Rishi Mehta, researcher at Google DeepMind, explains the test-time reinforcement learning mechanism enabling AlphaProof to tackle difficult math problems.
0:00 / 0:33exact quote · 34.0s
▶ Watch the full episode on YouTube → 720p mp4 · rendered on demand · StarZero watermark
“One of the ways in which it navigates this massive search space is via an idea that we came up with, which we call test time RL. So this is an idea where, like, let's say you're confronted with a problem that you don't know how to solve. And you know, you can do some search with your what you know right now, and you're not, not able to find a proof to it. What the agent then does is it constructs many variations of the problem in the vicinity of that problem and attempts to solve all of them. And if it manages to solve any of them, it learns from that experience and sort of comes closer and closer to solving the original problem.”
quote is from the automated transcript, cleaned for reading: filler sounds and stutters are removed, nothing is rephrased. names can be misheard (the analysis reads context, assessments check outside sources). how →
More from Rishi Mehta
Mehta: Specialist data seeds LLMs, but RL drives superhuman capability
“The specialist humans are gonna serve to, like, get the LLM from, like, just a bunch of weights that knows how to do nothing to, like, something that, like is, like, surprisingly strong. And then the RL is gonna take you from there to, like, something that's, …”
Mehta: AlphaProof's RL scaling and test-time compute generalize across domains
“Some of the sort of tech we developed here of like, you know, like scaling RL and like figuring out how to spend a lot of inference time compute stuff like this feels like it's Quite generally applicable to many other problems.”
Mehta: Fields Medalist Tim Gowers failed to find AlphaProof's IMO construction
“Tim Gowers, who was one of our judges and is also a fields medalist. Tried this question for a couple hours and he couldn't find the construction for function that had this property”
Mehta: As AI solves problems, human roles shift toward question framing
“As machines get better at finding the answers, like, we're going to have to get better at finding the questions. And, you know, like these systems don't have a, you know, their own sort of notion of what questions are interesting. And given a large question, h…”
Mehta: AlphaProof Is Strongest in IMO Algebra and Number Theory
“So the IMO problems have come in four categories. So there's algebra number theory, combinatrix, and geometry. The two that it's strongest at are algebra and number theory. It's relatively weaker at combinatrix, although it can do quite good at some IMO combin…”