TIL Math Olympiad problems are simple grammar exercises.

dartos · 2024-09-26T02:21:49 1727317309

They do way more than correcting grammar, but tbf, they did make something like 10,000 submissions to the math Olympiad to get that score.

It’s not like it’ll do it consistently.

Just a marketing stunt.

boroboro4 · 2024-09-27T05:01:47 1727413307

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 · 2024-09-30T16:11:01 1727712661

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.