On: Mira Murati leaves OpenAI

[boroboro4]

You’re talking about informatics Olympiad and O-1. As for Google’s DeepMind network and math Olympiad it didn’t do 10000 submissions. It did however generated bunch of different solutions but it was all automatic (and consistent). We’re getting there.

[dartos → boroboro4]

I wouldn’t really put AlphaProof in the came category as o1, Claude, or llama.

It was trained to generate text in the lean language (https://www.lean-lang.org/) which is specifically used for formal proofs.

It’s not a natural language model.

Source: https://deepmind.google/discover/blog/ai-solves-imo-problems...

Google seems to mainly be playing the game of more specialized models (AlphaGo, AlphaProof) with general training methods (AlphaZero)

I do think it’s kind of funny that they mention AGI in that article, but the model is specifically not general.