You even notice that with the recent opus and fable models by Anthropic.
If you give them a wide open problem statement, they'll start talking a lot of semi intelligible gibberish.
My guess is that this happens because that's not what they are evaluated on anymore for these kinds of tasks. The generated code is evaluated (in this case the lean code). So talking a bit of gibberish in the language part so you have more test time compute is not punished.
As I understand it, the rough guess as to what's happening here is that most recent capabilities progress comes from specific verifiable-rewards reinforcement training (RL). The RL pressures are all about task performance, but (surprise surprise) highly human-legible English language usage isn't very important to the models abilities to address the tasks.
Weirdly enough, the pressures are having them drift toward novel dialects of English that work well for their own chains of thought. Open question about whether they'd drift all the way to a new language given enough time.
This is tricky, because we really want language-independent training of skills. We know that self-play type of reinforcement learning is incredibly effective when possible. But at the same time, they are our tools - so we need supervised language training for this reason? It's possible that training just needs to be rebalanced so that RL with rewards is balanced with rounds of language adjustment. And to really make that happen, benchmarks need to score the models on that.
If you give them a wide open problem statement, they'll start talking a lot of semi intelligible gibberish.
My guess is that this happens because that's not what they are evaluated on anymore for these kinds of tasks. The generated code is evaluated (in this case the lean code). So talking a bit of gibberish in the language part so you have more test time compute is not punished.