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

131–140 of 177 posts

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

#131

Post by ks2048 »

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 don’t get the criticism. It seems like basic research and the kind of thing that would lead the way to “AGI” (combining llm-style prediction with logical reasoning). Unless you’re talking about what’s the point of publishing Nature papers - then it’s probably that the people involved want some concrete recognition in their work up to this point. And I supposed tech/investor press until they get something useful out from it.

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

#132

Post by WalterSear »

mitthrowaway2 wrote: post #126
amelius wrote: post #98

Earlier quoted context omitted.

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.

Is that very different than the distillation and amplification process that happens during training? Where the neural net learns to predict in one step what initially required several steps of iterated execution.

IMHO, yes. It's not an (internal) invention occurring as a result of insight into the process - it's an (external) human training one model on the output of another model.

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

#133

Post by WalterSear »

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 same thing that happened when they allowed calculators in the classroom.

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

#134

Post by nybsjytm »

killerstorm wrote: post #99
jhrmnn wrote: post #86

Earlier quoted context omitted.

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

The search space here is not so large. Read this paper, a key part of the present work: https://doi.org/10.1023/A:1006171315513

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

#135

Post by nybsjytm »

margorczynski wrote: post #118
nybsjytm wrote: post #64

Earlier quoted context omitted.

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

Brute searching all possible mathematical constructs, theorems, etc. to see which one fits the problem would probably take you practiacally an infinite amount of time. This works tbh, how I see it, very closely to how a human does - via "instinct" it gathers relevant knowledge based on the problem and then "brute searches" some combinations to see which one holds. But this "intuition" is the crucial part where brute…

> Brute searching all possible mathematical constructs, theorems, etc. to see which one fits the problem would probably take you practiacally an infinite amount of time.

That's not the kind of search which is being done. Read this paper: https://doi.org/10.1023/A:1006171315513

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

#136

Post by gisearkr »

There's a worked example near the article's start proving that an isoceles triangle has equal angles: the so-called pons asinorum. The caption concludes with "In this example, just one construct is required."

That strikes me as odd, because I'd expect the symbolic engine to require zero such constructs to find a proof. Although dropping a bisector is the standard grade-school proof strategy, there's a well-known proof that defines no additional entities: since AB = AC, we have (by side-side-side) that △ABC ≅ △ACB, and therefore that ∠ABC = ∠ACB.

It's funny because what that proof is most famous for is having been rediscovered by an automated theorem prover in the 1950s-1960s. (Wikipedia states that this is a myth, and that it was only rediscovered by Marvin Minsky pretending to be an automated theorem prover... which is true; but then Herbert Gelernter later wrote such a theorem prover! [1])

[1] https://www.qedcat.com/function/27.3.pdf#page=18

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

#137

Post by szmerdi »

As a former problem designer for IMO and similar contests, I deeply enjoyed reading this paper. At the same time, I'd like to point out that it was clear Geometry had to be the first topic to give up against AI (i.e., smart knowledge and inference-method indexing) Among math olympiad topics, Geometry problems are often the most "mechanical." Once you can express the problem in terms of coordinates (think XY or complex plane) you're looking at a finite set of steps a computer can use to find a solution. Of course, time limits and human error get in the way of this being practical during the IMO itself. Back in the day, I'd use WolframAlpha to verify geometry proofs for problems I designed (+conjectures) using this approach.

Algebra (especially inequalities) can be similar – pull off some intense calculations and you often have your answer.

Where I'm really excited to see intelligent systems make progress is with Number Theory and Combinatorics problems. The search spaces are far more complex and they often require proving that something is impossible. These are the problems that would be difficult to solve with brute force computation.

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

#138

Post by gowld »

treprinum wrote: post #80
lacker wrote: post #79

Earlier quoted context omitted.

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.

That applies to most things humans so for fun.

No one needs these contest math problems solved -- by requirement, they are solved before any student attempts them.

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

#139

Post by uptownfunk »

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…

This I suspect is the closest chance to reaching some flavor of AGI

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

#140

Post by fovc »

szmerdi wrote: post #137

As a former problem designer for IMO and similar contests, I deeply enjoyed reading this paper. At the same time, I'd like to point out that it was clear Geometry had to be the first topic to give up against AI (i.e., smart knowledge and inference-method indexing) Among math olympiad topics, Geometry problems are often the most "mechanical." Once you can express the problem in terms of coordinates (think XY or comple…

As a consumer of those problems, first of all, thank you! Even decades on from high school I occasionally enjoy working on them.

But agree that geometry was obviously going to be first. From what I’ve gathered here, it’s not “brute forcing” in terms of relying on algebraic geometry, vectors, or complex number solutions, but it is brute force in that it’s exhaustively looking for “interesting” constructions.

Geometry was always my worst subject, but even so I felt like if given the right construction the problem was much easier. Unfortunately I never developed the intuition to hit on those constructions quickly. It seems this AI doesn’t either, but it can churn through them much faster — There are only so many perpendiculars and parallels and bisectors you can construct which you can more or less mechanically evaluate (map out all angles and ratios, try power of a point, etc.)

While this is incredibly impressive, it seems like Deep Mind:Kasparov::AlphaGeo:Terry Tao in the “engine vs AI” sense.

I agree Algebra is likely next. Like geometry, more often than not you “just” need a clever substitution or 3, of which there are only so many options to choose from.

Some combinatorics problems I think would also be amenable to this search strategy (e.g., finding things to count 2 ways), but that seems like a bridge further away, and only gets you a subset of problems.

Number theory would be my guess for the final frontier before a perfect 42.

Post reply on HN