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

161–170 of 177 posts

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

#161

Post by sdenton4 »

skepticATX wrote: post #124
MrPatan wrote: post #96

Earlier quoted context omitted.

Not a lot of humans do

Every single human has abstractions that are unique to them. Your world model isn’t the same as mine. It’s just that usually these abstractions are fuzzy and hard to formalize, so they aren’t shared. It doesn’t mean that they don’t exist.

This is laughable... Neural networks also have basically unknowable abstractions encoded in their weights. There was some work not long ago which taught an ANN to do modular arithmetic, and found that it was doing Fourier transforms with the learned weights....

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

#163

Post by aconz2 »

summary: generate 500M synthetic examples where you start with random constructions, deduce (not sure until saturation or fixed depth) and use each conclusion along with its dependency graph and original premises as a training example. The 500M reduces to 100M after dedupe and they used 7.5M CPU hours. 9M/100M used auxiliary/exogenous constructions (which I think of as like if you're doing this on program search and the program requires some constant pi that isn't derivable from the inputs). They encode the examples for a transformer and finetune on the auxiliary construction subset to eek out 2 more problems. Then beam search using the model to generate next term and logic engine to expand the closure until the conclusion is in the set.

They make a big deal about these auxiliary constructions but I'm not sure the results back that up. I also don't understand what the "without pretraining" means; they say without pretraining it gets 21 problems, without fine-tuning 23 problems, and altogether 25. So are they getting 21/25 without their synthetic data at all??

I want to look at how the dependency graph is encoded in the training examples and whether you might expect different results from different encodings. Ideally I'd think you'd want that part of the model/embedding to be invariant across all possible (big number!) of encodings.

The human comparisons are really weak in Fig 2 and unfortunately is probably what the media mainly focuses on. I do find the results interesting and wonder how well this translates into program synthesis for example. The paper mentioned in these comments which I have yet to read more "Language Models Can Teach Themselves to Program Better" sounds related. I'd be very interested to see more methods that are very different from LLM heuristic beam search, even though it does seem compelling and they get to publish lots of papers with it.

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

#164

Post by tsimionescu »

killerstorm wrote: post #157
tsimionescu wrote: post #151

Earlier quoted context omitted.

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

AlphaGeometry works, in simplified terms, in two stages:

1. Heuristically add a candidate construction using an NN (a transformer)

2. Brute force search through all possible deductions from the current set of constructions using a symbolic solver

If you don't find a solution after step 2, repeat. There may be some backtracking involved to try a different set of constructions as well.

This approach only works because, in geometry, the set of possible deductions from a given construction is actually quite small.

Also, note that this approach overall is essentially an optimization, not amazing new capabilities. Replacing step 1 with a random construction still solves 10 problems on average in the given time, compared to 30 with the new approach. The existing algorithm, relying mostly on brute force search, is probably able to solve all of the geometry problems if given, say, 10 times as much time as the olympiad students (so not some absurd amount of time).

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

#165

Post by lacker »

zodiac wrote: post #41

The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.

Yes, and even the non-neural-network, symbolic plus linear algebra component of AlphaGeometry is able to outperform the previous state of the art. So a decent amount of work here went into the components that aren't neural networks at all.

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

#166

Post by lacker »

generationP wrote: post #109

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

They built their own symbolic geometry engine, called DDAR. The IMO judges will typically let you get away with much less rigor than a symbolic engine like this produces, so I don't think they are taking advantage of any of these conventions.

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

#167

Post by CamperBob2 »

ChatGTP wrote: post #155
CamperBob2 wrote: post #148

Earlier quoted context omitted.

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

"Also, the C++ code this talking dog wrote for me is full of buffer overflow vulnerabilities, and my Commodore 64 still can't run Crysis. There's nothing but hype here, move along."

News flash: either AI gains the ability to postulate theorems, generate proofs, and validate them, or mathematics is as dead as Latin. Humans have reached their limit.

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

#168

Post by generationP »

lacker wrote: post #166
generationP wrote: post #109

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

They built their own symbolic geometry engine, called DDAR. The IMO judges will typically let you get away with much less rigor than a symbolic engine like this produces, so I don't think they are taking advantage of any of these conventions.

Ah, thanks! It seems to be this one http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf plus some algebra for adding angles and lengths. As I hoped, they are using oriented angles mod 180° ("full-angles") to get rid of betweenness conditions. They are also using evaluations at rational (I think) coordinates to check that nondegenerateness conditions are satisfied when the data is in general position. This is not as nice as I had hoped for, but certainly no worse than what contestants do at the IMO. And because a bunch of methods are off-limits (congruence criteria, probably anything involving undirected unsquared lengths), I'm not surprised that their proofs are longer/slower than human ones -- they're better proofs.

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

#169

Post by generationP »

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…

I expected three-number inequalities to give in first, as there is less of a question about what counts as a proof. I didn't know that the latter problem was already solved in 2000 ( http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf ).

Someone really should make an adventure game out of synthetic geometry, as it allows for a proof-writing language simpler than Lean's and allows for nice visuals.

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

#170

Post by generationP »

zodiac wrote: post #41

The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.

This is nice, but I suspect that a barycentric coordinate bash with the formulas in Evan Chen's book could also do 30% of the IMO (seeing that most of it is about triangles) on a modern laptop.
Post reply on HN