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

101–110 of 177 posts

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

#101

Post by empath-nirvana »

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.

I'm not sure why you are calling it non-AI. There's no reason why some AI system has to be some single neural network like GPT and not a hacked together conglomeration of a bunch of neural networks and symbolic logic systems. Like is it cheating to use a SAT solver? Is a SAT solver itself not artificial intelligence of a kind?

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

#102

Post by littlestymaar »

MrPatan wrote: post #96
amelius wrote: post #92

Earlier quoted context omitted.

Well, what's different is that humans invent new abstractions along the way such as complex numbers and Fourier transforms.

Not a lot of humans do

True, but we're talking about Olympiad level math skills here.

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

#103

Post by compthink »

Very interesting. I was suspicious they could get an LLM to do this alone, and reading the description they don't. It's still AI I would say, maybe even more so since it alternates between a generative machine learning model to come up with hypothesis points. But then it uses a optimizer to solve for those pointa and simplify the problem. So it really is a mathematical reasoning system. Also good to note that is tuned specificially to these types of geometry problems.

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

#104

Post by hiAndrewQuinn »

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?

I've accepted that the human form, with its ~3 pounds of not especially optimized brainpower, is basically going to be relegated to the same status as demoscene hardware for anything that matters after this century.

That's cool by me, though. This bit of demoscene hardware experiences qualia, and that combination is weird and cool enough to make me want to push myself in new and weird directions. That's what play is in a way.

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

#105

Post by jhbadger »

lacker wrote: post #79
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?

The incentive to compete in the IMO is that it's fun to do math contests, it's fun to win math contests, and (if you think that far ahead as a high schooler) it looks good on your resume. None of that incentive will go away if the computers get better at math contests.

People still compete in foot races even though cars can go faster. People still play chess and Go even though computers can beat them.

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

#107

Post by mb7733 »

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?

Like I said, it's got nothing to do with computers or AI. This point of view predates any kind of AI that would be capable of doing either.

The analogy is as follows. Like with with leetcode & job interviews is as follows, to excel at math competitions one must grind problems and learn tricks, in order to quickly solve problems in a high pressure environment. And, just like how solving leetcode problems is pretty different than what a typical computer scientist or software engineer does, doing math competitions is pretty different than what a typical mathematician does.

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

#108

Post by cubefox »

empath-nirvana wrote: post #101
gizmo686 wrote: post #19

Earlier quoted context omitted.

> 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. I'm not sure why you are calling it non-AI. There's no reason why some AI system has to be some single neural network like GPT and not a hacked together conglomeration of a bunch of neural networks and symbolic logic systems. Like is it cheating to use a SAT solver? Is a SAT solver itself not artificial intelligence of a kind?

In modern terminology, AI = machine learning model. The hand coded GOFAI from the past is just called software.

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

#109

Post by generationP »

What deductive system are they using to verify the proofs? I'm asking because the conventions of olympiad geometry are slightly different from those of the rest of mathematics (you can make informal "general position" arguments; you can pooh-pooh issues of sign and betweenness; you can apply theorems to unstated limiting cases; etc.), and it is far from obvious to me how this logic can be formalized without causing contradictions.

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

#110

Post by generationP »

qwertox wrote: post #58

Google DeepMind keeps publishing these things while having missed the AI-for-the-people train, that I'm getting more and more the feeling that they have such a huge arsenal of AI-tech piling up in their secret rooms, as if they're already simulating entire AI-based societies. As if they're stuck in a loop of "let's improve this a bit more until it is even better", while AGI is already a solved problem for them. Or th…

What they did here is one of the first steps towards an AI that generates nontrivial and correct mathematical proofs. (An alternative benchmark would be IMO-level inequalities. Other topics such as algebra, combinatorics and number theory are probably no easier than the rest of mathematics, thus less useful as stepping stones.)

And an AI that generates nontrivial and correct mathematical proofs would, in turn, be a good first step towards an AI that can "think logically" in the common-sense meaning of the word (i.e., not just mess around with words and sentences but actually have some logical theory behind what it is saying). It might be a dead end, but it might not be. Even if it is, it will be a boon to mathematics.

Post reply on HN