News for hackers. Stuff that matters.

A comment on Mira Exits OpenAI. Parent comment

Re:Mira Exits OpenAI by boroboro4 on Friday September 27, 2024 @01:01AM (#41666427)
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.
[ Parent | on HN ]
Re:Mira Exits OpenAI by dartos on Monday September 30, 2024 @12:11PM (#41698811)
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.

[ Parent | on HN ]