Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AlphaGeometry: An Olympiad-level AI system for geometry

deepmind.google

Post reply on HN
Print view View original

21–30 of 177 posts

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#21

Post by adverbly »

empath-nirvana wrote: post #11

“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said. --- Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.

I guess it kind of depends on what a goal post should represent. If it represents an incremental goal then obviously you are correct.

I think the ultimate goal though is clearly that AI systems will be able to generate new high-value knowledge and proofs. I think the realistically the final goal post has always been at that point.

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#22

Post by mlyle »

chefandy wrote: post #17
1024core wrote: post #12

From the Nature article: > Note that the performance of GPT-4 performance on IMO problems can also be contaminated by public solutions in its training data. Doesn't anybody proofread in Nature?

Not a subject matter expert, so forgive me if the question is unintentionally obtuse, but It seems like a reasonable statement. They seem to be inferring that problems with existing public solutions wouldn't be a good indicator of performance in solving novel problems-- likely a more important evaluative measure than how fast it can replicate an answer it's already seen. Since you couldn't know if that solution was i…

They're referring to "performance of performance".

Not that it's a big deal. I notice problems like this slip into my writing more and more without detection as I get older :/

I don't see the sentence in the Nature paper, though.

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#23

Post by esafak »

mb7733 wrote: post #13
empath-nirvana wrote: post #11

“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said. --- Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.

No, that sort of thing has been said about math competitions for a long time. It's not a new argument put forward as something against AI. An analogy with software is that math competitions are like (very hard) leetcode. There was an article posted on HN recently that is related: https://benexdict.io/p/math-team

What is the argument; that math competitions are easy for computers but hard for humans?

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#24

Post by Imnimo »

I'm very curious how often the LM produces a helpful construction. Surely it must be doing better than random chance, but is it throwing out thousands of constructions before it finds a good one, or is it able to generate useful proposals at a rate similar to human experts?

They say in the paper, "Because the language model decoding process returns k different sequences describing k alternative auxiliary constructions, we perform a beam search over these k options, using the score of each beam as its value function. This set-up is highly parallelizable across beams, allowing substantial speed-up when there are parallel computational resources. In our experiments, we use a beam size of k = 512, the maximum number of iterations is 16 and the branching factor for each node, that is, the decoding batch size, is 32."

But I don't totally understand how 512 and 16 translate into total number of constructions proposed. They also note that ablating beam size and max iterations seems to only somewhat degrade performance. Does this imply that the model is actually pretty good at putting helpful constructions near the top, and only for the hardest problems does it need to produce thousands?

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#25

Post by jvanderbot »

gizmo686 wrote: post #19
marojejian wrote: post #3

Though this particular model doesn't sound generalizable, the neuro-symbolic approach seems very promising to me: - 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 g…

> 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. You do not need to solve everything at once. This approach has the potential to revolution both math and programming by moving formal verification from being a niche tool into a regular part of every practitioners toolbox. It al…

Moreover, it's not so recently that people began training networks to help make guesses for branch and bound type solvers.

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#27

Post by apsec112 »

albertzeyer wrote: post #16
apsec112 wrote: post #6

Interesting 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…

It's not tiny, this is a quite normal size outside the field of LLMs, e.g. normal-sized language models, or also translation models, or acoustic models. Some people even would call this large.

It's tiny by the standards of transformers, pretty sure most transformers trained (across all domains) are larger than this

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#28

Post by nitwit005 »

esafak wrote: post #23
mb7733 wrote: post #13

Earlier quoted context omitted.

No, that sort of thing has been said about math competitions for a long time. It's not a new argument put forward as something against AI. An analogy with software is that math competitions are like (very hard) leetcode. There was an article posted on HN recently that is related: https://benexdict.io/p/math-team

What is the argument; that math competitions are easy for computers but hard for humans?

It's a quote from the article. The argument is naturally there.

Re: AlphaGeometry: An Olympiad-level AI system for geometry

#29

Post by GPerson »

empath-nirvana wrote: post #11

“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said. --- Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.

I’m not sure if it’s goal post shifting or not, but it is a true statement.
Post reply on HN