It's how RLVR works, when you have a task with a verified answer, you rerun the model on it and promote the reasoning chains that reach the answer. That way you can hill climb model capabilities on any problem you find, which generalises to new problems to solve, which you can then hill climb again and so on.
replySo since they are doing that task anyway (re-solving the problem increasingly more efficiently), this is a easy check point to publish to show how far they've gotten in that process.
deleted
reply> instead of doing something new
replyBecause current AI cannot do that, seems like it. Otherwise they would have done it.
... as a test / benchmark? Hard to make a comparison without a control...
replyYeah, but obviously doing a formalisation that has been done before is different than doing a new one since you have knowledge about the previous attempt. It also just seems less impressive than doing something new and the reason they are reporting this is marketing.
replydo you assume or do you know that the previous attempt is in the training data?
reply