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

91–100 of 177 posts

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

#91

Post by 1024core »

chefandy wrote: post #32
mlyle wrote: post #22

Earlier quoted context omitted.

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.

Ah-- I've got super bad ADHD so I usually don't even catch things like that. I'm a terrible editor. I wouldn't be surprised if the paper authors were paying attention to this thread, and gave a call to Nature after seeing the parent comment.

The text is still there.

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

#92

Post by amelius »

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…

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

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

#93

Post by 1024core »

FranchuFranchu wrote: post #75

As soon as ChatGPT got released, I tried to make it solve IMO-style problems. It failed. If this is legit, this is huge. Finding geometric proofs means proving things, and proving propositions is what an intelligence does. In my opinion, this is the closest we have gotten so far to AGI. Really excited to see what the future holds.

From the paper:

> When producing full natural-language proofs on IMO-AG-30, however, GPT-4 has a success rate of 0% ...

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

#94

Post by gowld »

amelius wrote: post #92
killerstorm wrote: post #68

Earlier quoted context omitted.

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

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

A neural network is nothing but a heap of new abstractions from data.

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

#95

Post by gowld »

somewhereoutth wrote: post #85
killerstorm wrote: post #68

Earlier quoted context omitted.

> 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?

A calculator that can solve any problem human could, and more? Sure.

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

#96

Post by MrPatan »

amelius wrote: post #92
killerstorm wrote: post #68

Earlier quoted context omitted.

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

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

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

#97

Post by gowld »

FranchuFranchu wrote: post #75

As soon as ChatGPT got released, I tried to make it solve IMO-style problems. It failed. If this is legit, this is huge. Finding geometric proofs means proving things, and proving propositions is what an intelligence does. In my opinion, this is the closest we have gotten so far to AGI. Really excited to see what the future holds.

Proving propositions has been computer work for several decades.

This is not a pure LLM. Search algorithms are obviously incredibly powerful at solving search problems. The LLM contribution is an "intuitive" way to optimize the search.

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

#98

Post by amelius »

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

When a human has done the same thing many times they tend to try to generalize and take shortcuts. And make tools. Perhaps I missed something but I haven't seen a neural net do that.

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

#99

Post by killerstorm »

jhrmnn wrote: post #86
killerstorm wrote: post #68

Earlier quoted context omitted.

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

The comment above mentions "brute force" incorrectly. It's fundamentally impossible to brute force googol combinations...

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

#100

Post by senseiV »

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…

> simulating entire AI-based societies.

Didnt they already have scaled down simulations of this?

Post reply on HN