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

81–90 of 177 posts

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

#81

Post by treprinum »

jeanloolz wrote: post #61
treprinum wrote: post #47

What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?

Chess never faded away. It actually has never been as big as it is today.

That might be true in the number of active chess players, but it's no longer viewed as a peak intellectual game and the magic is long gone, just another intense hobby some people do, but basic machines can do better.

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

#82

Post by [deleted] »

treprinum wrote: post #47

What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?

[deleted]

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

#83

Post by initplus »

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…

>however that solution only works because we have a non AI system to prove correctness

But this is actually a really common scenario. Checking a solution for correctness is often much easier than actually finding a correct solution in the first place.

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

#84

Post by sdenton4 »

treprinum wrote: post #47

What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?

We just need a Netflix series about a geometry prodigy with excellent fashion sense.

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

#85

Post by somewhereoutth »

killerstorm wrote: post #68
nybsjytm wrote: post #50

If I read their paper right, this is legit work (much more legit than DeepMind's AI math paper last month falsely advertised as solving an open math research problem) but it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence. A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the e…

> it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence. How so? Reasoning is fundamentally a search problem. The process you described is exactly the process humans use: i.e. make a guess about what's useful, try to work out details mechanically. If get stuck, make another guess, etc. So the process is like searching through a tree. People figured out…

> Some magic device which can solve any problem using a single linear pass?

You mean like a calculator?

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

#86

Post by jhrmnn »

killerstorm wrote: post #68
nybsjytm wrote: post #50

If I read their paper right, this is legit work (much more legit than DeepMind's AI math paper last month falsely advertised as solving an open math research problem) but it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence. A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the e…

> it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence. How so? Reasoning is fundamentally a search problem. The process you described is exactly the process humans use: i.e. make a guess about what's useful, try to work out details mechanically. If get stuck, make another guess, etc. So the process is like searching through a tree. People figured out…

I think the intuition here is that an “intelligent” system would lean much more heavily on the heuristics than on the search, like humans. It’s hard to quantify in this case, but certainly in the case of chess, when engines were about as good as best human players, they were doing orders of magnitude larger search than humans. Which made them feel more like chess _engines_ than chess AI. AlphaZero certainly made a step in the right direction, but it’s still far from how humans play.

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

#87

Post by pk-protect-ai »

bnprks wrote: post #52

I appreciate that the authors released code and weights with their paper! This is the first high-profile DeepMind paper I can recall that has runnable inference code + checkpoints released. (Though I'm happy to be corrected by earlier examples I've missed) I don't yet see a public copy of the training set / example training code, but still this is a good step towards providing something other researchers can build on…

Yeap. I'm missing the datasets as well. They have generated 100M synthetic examples ... Were these examples generated with AlphaGeometry? Where is the filtering code and initial input to generate these synthetics?

Im I'm wrong that they are using t5 model? At least they are using the sentencepiece t5 vocabulary.

How many GPU hours have they spend training this model? Which training parameters were used?

Don't get me wrong, I find this system fascinating it is what applied engineering should look like. But I'd like to know more about the training details and the initial data they have used as well as the methods of synthetic data generation.

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

#88

Post by 1024core »

mlyle wrote: post #22
chefandy wrote: post #17

Earlier quoted context omitted.

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.

Paper: https://www.nature.com/articles/s41586-023-06747-5

Section title: Geometry theorem prover baselines

Second paragraph under that. 3rd sentence from the end of the para.

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

#89

Post by 1024core »

dr_kiszonka wrote: post #18
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?

Weird. I can't find the sentence you are quoting in the paper.

Paper: https://www.nature.com/articles/s41586-023-06747-5

Section title: Geometry theorem prover baselines

Second paragraph under that. 3rd sentence from the end of the para.

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

#90

Post by westcoast49 »

treprinum wrote: post #81
jeanloolz wrote: post #61

Earlier quoted context omitted.

Chess never faded away. It actually has never been as big as it is today.

That might be true in the number of active chess players, but it's no longer viewed as a peak intellectual game and the magic is long gone, just another intense hobby some people do, but basic machines can do better.

It’a still viewed as a peak intellectual game. And the magic is still there, just watch or listen to the fans of Magnus Carlsen when they’re viewing, discussing or analyzing his games.
Post reply on HN