Sartran: Translating all known human proofs would save years of compute
Laurent Sartran · No Priors Ep. 90 | With Google's DeepMind's AlphaProof Team · Nov 14, 2024 · at 26:07
Laurent Sartran of DeepMind discusses the utility of formalizing human expert mathematical data versus relying purely on reinforcement learning search.
0:00 / 0:16exact quote · 16.1s
▶ Watch the full episode on YouTube → 720p mp4 · rendered on demand · StarZero watermark
“With more supervised data, we can avoid the exploration problem, and we could translate all the proofs that are known to man, and that certainly would make the agent much better, and that would save us years of compute for sure.”
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 Laurent Sartran
Sartran: AlphaProof develops an alien style by learning from self-discovered proofs
“The way alpha proof currency operates there is that it discovers its own proofs, and when they are valid, it learns from them and develop its own style which has been commented upon as looking, yeah, quite, quite alien.”
Sartran: Human creativity matters more in theory building than theorem proving
“It seems that there is more room for human creativity, human taste human skill in building theories than in the proof part.”