Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Mira Exits OpenAI. Parent comment
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.
There are no comments on this comment yet.
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.