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

71–80 of 177 posts

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

#71

Post by danielmarkbruce »

nybsjytm wrote: post #64
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…

This is at almost the polar opposite end of the spectrum from "AGI," it's centered on brute search.

They are not polar opposites.

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

#72

Post by artninja1988 »

nodogoto wrote: post #70
artninja1988 wrote: post #67

>To train AlphaGeometry's language model, the researchers had to create their own training data to compensate for the scarcity of existing geometric data. They generated nearly half a billion random geometric diagrams and fed them to the symbolic engine. This engine analyzed each diagram and produced statements about their properties. These statements were organized into 100 million synthetic proofs to train the lang…

What statements about properties of randomly generated code snippets would be useful for coding LLMs? You would need to generate text explaining what each snippet does, but that would require an existing coding LLM, so any IP concerns would persist.

Yeah, but couldn't some system be built that understands what the differnt code snippets do by compiling them or whatever?

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

#73

Post by achierius »

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…

I think Occam's razor would have something to say about the relative likelihood of those two options.

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

#75

Post by FranchuFranchu »

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.

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

#76

Post by lacker »

ipsum2 wrote: post #74

Do normal proofs for Olympiad level geometry questions require 150+ steps like the one that was generated here? It seems inelegant.

When a human solves these problems, you might state a "step" in natural language. Like, "apply a polar transformation to this diagram". But that same single step, if you translate into a low-level DSL, could be dozens of different steps.

For an example, check out this formalization of a solution to a non-geometry IMO problem:

https://gist.github.com/mlyean/b4cc46cf6b0705c1226511a2b404d...

Roughly the same solution is written here in human language:

https://artofproblemsolving.com/wiki/index.php/1972_IMO_Prob...

It's not precisely clear what counts as a "step" but to me this seems like roughly 50 steps in the low-level formalized proof, and 5 steps in the human-language proof.

So, my conclusion is just that I wouldn't necessarily say that a 150-step automated proof was inelegant. It can also be that the language used to express these proofs fills in more of the details.

It's like the difference between counting lines of code in compiled code and a high-level language, counting the steps is really dependent on the level at which you express it.

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

#77

Post by treprinum »

Agingcoder wrote: post #49
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 never studied math to become the best in the world !

Are you an Olympiad Gold Medalist? Did you move the field of math significantly (beyond a basic PhD)?

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

#78

Post by sangnoir »

artninja1988 wrote: post #67

>To train AlphaGeometry's language model, the researchers had to create their own training data to compensate for the scarcity of existing geometric data. They generated nearly half a billion random geometric diagrams and fed them to the symbolic engine. This engine analyzed each diagram and produced statements about their properties. These statements were organized into 100 million synthetic proofs to train the lang…

For language, the symbolic engine itself would likely be trained on copyrighted input, unlike the geometry engine, since math & math facts are not covered by copyright.

If you couple random text genrsrion and such an engine for language, you'd be laundering your training using the extra step (and the quality will likely be worse due to multiplicative errors)

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

#79

Post by lacker »

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.

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

#80

Post by treprinum »

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.

I'd be super demoralized if anything I could do a future pocket machine could do much better and faster. Like my very best is not enough to even tread water.
Post reply on HN