Hubert: Formal math proofs enable self-improving reinforcement learning loops
Thomas Hubert · No Priors Ep. 90 | With Google's DeepMind's AlphaProof Team · Nov 14, 2024 · at 5:55
Google DeepMind researcher Thomas Hubert explains the core architecture of AlphaProof and how formal verification provides the feedback signal for reinforcement learning.
0:00 / 0:23exact quote · 23.8s
▶ Watch the full episode on YouTube → 720p mp4 · rendered on demand · StarZero watermark
“The advantage of that is that once kind of the proof is complete then you know, the machine would give you a signal back to say, yes, your proof is correct or not. And so we could search for kind of correct proofs. Once we find a correct proof, we can learn from it and get a better neural network and kind of go into this self-improving loop of tackling harder and harder problems and learning more and more about math.”
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 Thomas Hubert
Hubert: AlphaProof reached high school level but cannot rival Terence Tao
“And to be honest with you know, like kind of we, at the moment we can't rival at all with someone like Terry Tao. We, I think we demonstrated that what we've demonstrated is that we can learn general mathematics almost from scratch and arrive at kind of an imp…”
Hubert: Automated Formal Proof Checkers Enable Mass Crowdsourced Mathematics
“But if you instead relied on a formal system to check everyone else's work, then You could do a little bit like in astronomy where you could have an amateur kind of living in the middle of maybe nowhere and you, you've never met. And then you wouldn't have to …”
DeepMind's Hubert: Solving Harder Math Requires Introducing New Mathematical Objects
“To prove harder problems, you start to need to be able to introduce these new kind of mathematical objects to decompose the problems or problems. And we see that already happening for the IMO at a, you know, small scale.”