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

151–160 of 177 posts

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

#151

Post by tsimionescu »

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 key insight is this whole thread is that this Alpha Geometry only works because the search field is not a googol combinations. So, it doesn't really generalize to many other fields of math. We shouldn't expect an AlphaCategoryTheory or AlphaNumberTheory anytime soon.

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

#152

Post by aldousd666 »

This is fascinating and inspiring progress! What's crazy to me is how many people are looking to put stakes in the ground in front of this, claiming breathlessly before anyone can speak, that this isn't real AI progress or this isn't actually doing it how humans supposedly do, and implying that therefore it's not a big deal. I'm sorry to break to you folks, this is just another sign post moment. One more event to mark our place in history as we sail on. And when we look back on it, there isn't going to be all the disclaimers people are trying to throw down now. We had imagenet and deep blue, we had alphazero, alphago, GPT4, alphafold, and now we have AlphaGeometry.As DJ Khaled likes to point out, this is.. Another one

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

#153

Post by dr_kiszonka »

1024core wrote: post #89
dr_kiszonka wrote: post #18

Earlier quoted context omitted.

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.

Thank you.

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

#154

Post by ChatGTP »

aldousd666 wrote: post #152

This is fascinating and inspiring progress! What's crazy to me is how many people are looking to put stakes in the ground in front of this, claiming breathlessly before anyone can speak, that this isn't real AI progress or this isn't actually doing it how humans supposedly do, and implying that therefore it's not a big deal. I'm sorry to break to you folks, this is just another sign post moment. One more event to mar…

This reads like another "edge lord" or "karma farming "comment. Seems to be more and more frequent here lately.

The point of the forum is that people who are interested in these things can discuss them together openly. People are having discussions about the way they interpret the paper and what they think it means. You seem to be telling those people that's pointless and we should just accept this as a breakthrough because you told us so. Which I think goes against the spirit of this forum and the ability for people to look at the world with an objective lens.

If this work is as good as you say it is, and it very well might be, it will stand on it's own no matter what people say about it. Time will tell if this was meaningful or not.

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

#155

Post by ChatGTP »

CamperBob2 wrote: post #148
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.

As soon as ChatGPT got released, I tried to make it solve IMO-style problems. It failed. Have you tried the same questions with ChatGPT 4? It is a transformational change (no pun intended) over the earlier releases, and over all open-source models. Just today, I needed to interpret some awkwardly-timestamped log data. I asked it a few questions along the lines of "What time it was 10,000 seconds before xx:yy:zz?" It…

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

#156

Post by xbmcuser »

Would something like this help ai/computer see the world better for robotics and self driving etc. I am not a programmer or in this field but I don't know why intuitally reading the headline alone made me feel the world of robotic and self driving etc ie where ai interact with the physical world is about to change.

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

#157

Post by killerstorm »

tsimionescu wrote: post #151
killerstorm wrote: post #99

Earlier quoted context omitted.

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

The key insight is this whole thread is that this Alpha Geometry only works because the search field is not a googol combinations. So, it doesn't really generalize to many other fields of math. We shouldn't expect an AlphaCategoryTheory or AlphaNumberTheory anytime soon.

"Brute force" = going through all combinations indiscriminately.

Using heuristics, beam search, etc, = "not brute force".

Calling something smart "brute force" is wrong.

> We shouldn't expect an AlphaCategoryTheory or AlphaNumberTheory anytime soon.

There's already a number of papers demonstrating use of LLMs for math in general:

"Autoformalization with Large Language Models" https://arxiv.org/abs/2205.12615

"Large language models can write informal proofs, translate them into formal ones, and achieve SoTA performance in proving competition-level maths problems!" https://twitter.com/AlbertQJiang/status/1584877475502301184

"Magnushammer: A Transformer-based Approach to Premise Selection" https://twitter.com/arankomatsuzaki/status/16336564683345879...

I find it rather sad that the reaction to amazing research is "but it's just..." and "it might not work on ...". Like, maybe appreciate it a bit and consider a possibility that something similar to it might work?

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

#158

Post by fovc »

fovc wrote: post #140
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…

Heh, can’t edit now, but s/Deep Mind/Deep Blue/

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

#159

Post by logicallee »

I wonder how well it would do with html page layout. It is nice to see advancements in geometric reasoning!

To give you a basis for comparison, I've found that (paid) ChatGPT even quite recently was not able to reason about simple html and css geometric constructs, such as what div is inside what container: with just two divs or containers on the page, it still applied styling to the wrong one and I had to move the line myself to the one it meant to style, even after I described to ChatGPT what the page currently looked like.

I just tried it again, it did succeed with this prompt:

"Create an HTML page that you divide in half vertically, you will set the background of divs to different colors. After dividing the page in half vertically, on the left half of the page put three different divs each taking up a third of the vertical space, color them red, orange, yellow. On the right half of the page create two different divs each taking half of the vertical space, color them green, blue. Within each div put a paragraph in black letters with the color and location of the div it is located in, such as "Left hand side, top div. This background is red." and so on for top, middle, and bottom on the left and top and bottom on the right, with the colors red, orange, yellow, green and blue respectively as their backgrounds. Reply with the complete html and css style page in single html file that I can copy and paste into a single file, when loaded it should show the layout I have described." When I try this right now I get a successsful page.

Here is the code it generated: https://paste.sh/drpp3Kci#FoQHQT6YtMknnI-y2N7beqAd which you can see created this https://ibb.co/NFwnvWL

It previously failed at similarly layout questions.

If ChatGPT had this "Olympiad-level" geometric reasoning it would be amazing for producing html pages that include complex layout. It currently doesn't always succeed at this.

Layout is the area that I've found ChatGPT is weakest in for generating code, which I chalk up to the fact that it doesn't have a vision subsystem so it can't really picture about what it's doing.

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

#160

Post by szmerdi »

Dracophoenix wrote: post #149
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…

How did you get into such a position? Is there an application process of some sort? After verifying solvability, what is the process for selecting the specific problems that will show up in the finished set? Is it by vote or some other evaluation?

Each year, national math olympiad committees submit their toughest problems to the IMO. A select group makes the "shortlist," a pool of ~32 questions (8 per geometry, algebra, number theory, combinatorics). From this pool, the final six IMO problems are chosen through a rigorous voting process.

What makes a great IMO problem? It's all about originality. Ideal problems aren't just about applying advanced theorems, but rather test creative thinking and mastery of fundamental principles. Of course, there were cases in which the IMO committee didn't realize a problem was an obvious corrolary of a grad-level theorem, and some well-read (highschool) students benefited from knowing that!

My Journey: I was once a top-ranked competitor myself. After high school, I joined my country's math olympiad committee.

Post reply on HN