AlphaGeometry: An Olympiad-level AI system for geometry
1–10 of 177 posts
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#2Re: AlphaGeometry: An Olympiad-level AI system for geometry
#3- linking the (increasingly powerful) "system 1" tools that are most of current ML with more structured "system 2" tools, like logical proof generation, which can plan and and check the veracity / value of output. - System 2 chugs along 'till it gets stuck, then system 1 jumps in to provide an intuitive guess on what part of state space to check next. - Here they leveraged the ability to generate proofs by computer to create a data set of 100m proofs, enabling scalable self-supervised learning. Seem to me the symbolic domains are well formed to allow such generation of data, which while low value in each instance, might allow valuable pre-training in aggregate.
Putting these elements together is an approach that could get us quite far.
The key milestone will be moving away from the need to use specific formal / symbolic domains, and to generate a pretrained system that can generalize the skills learned from those domains.
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#4Re: AlphaGeometry: An Olympiad-level AI system for geometry
#5Re: AlphaGeometry: An Olympiad-level AI system for geometry
#6"We use the Meliad library for transformer training with its base settings. The transformer has 12 layers, embedding dimension of 1,024, eight heads of attention and an inter-attention dense layer of dimension 4,096 with ReLU activation. Overall, the transformer has 151 million parameters, excluding embedding layers at its input and output heads. Our customized tokenizer is trained with ‘word’ mode using SentencePiece and has a vocabulary size of 757. We limit the maximum context length to 1,024 tokens and use T5-style relative position embedding. Sequence packing is also used because more than 90% of our sequences are under 200 in length."
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#7($10m prize for models that can perform well at IMO)
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#8Interesting that the transformer used is tiny. From the paper: "We use the Meliad library for transformer training with its base settings. The transformer has 12 layers, embedding dimension of 1,024, eight heads of attention and an inter-attention dense layer of dimension 4,096 with ReLU activation. Overall, the transformer has 151 million parameters, excluding embedding layers at its input and output heads. Our cust…
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#9It’s our maths. No one else owns it?
Funny game the AI field is playing now. One-upmanship seems to be the aim of the game.
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#10See also https://www.nytimes.com/2024/01/17/science/ai-computers-math... (via https://news.ycombinator.com/item?id=39030186 , but we'll merge that thread hither)