Comment by softwaredoug
10 hours ago
I wonder how long it'll pay for frontier labs to use compute this way?
I'm reminded of the Apollo program that was cool for a while, but eventually the public lost interest.
Maybe it becomes cheaper? Maybe other labs want to prove their worth will pick up the slack when another loses interest?
the presumption is that these results are a side-effect of reinforcement learning to make the models smarter.
Uh no, reinforcemnt learning doesn't magically pop out math proofs. OpenAI has a ton of mathematicians on staff and is spending millions of dollars in compute to pursue these solutions.
Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh
2 replies →
That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.