Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI solves International Math Olympiad problems at silver medal level

deepmind.google

Post reply on HN
Print view View original

111–120 of 564 posts

Re: AI solves International Math Olympiad problems at silver medal level

#111

Post by visarga »

ZenMikey wrote: post #8
adverbly wrote: post #2

> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month fo…

I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?

> just fumbling its way around until it guessed correctly

As opposed to 0.999999% of the human population who can't do it even if their life depends on it?

Re: AI solves International Math Olympiad problems at silver medal level

#112

Post by golol »

riku_iki wrote: post #108
golol wrote: post #73

Earlier quoted context omitted.

I believe you are misreading this. First of all, this is not a sport and the point is not to compare AI to humans. The point is to compare AI to IMO-difficulty problems. Secondly, this is now some hacky trick where Brute force and some theorem prover magic are massaged to solve a select few problems and then you'll never hear about it again. They are building a general pipeline which turns informal natural lamguage m…

> They are building a general pipeline which turns informal natural lamguage mathematics but this part currently sucks, because they didn't trust it and formalized problems manually.

Yea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.

Re: AI solves International Math Olympiad problems at silver medal level

#113

Post by visarga »

10100110 wrote: post #83
adverbly wrote: post #2

> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month fo…

Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.

Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.

Re: AI solves International Math Olympiad problems at silver medal level

#115

Post by majikaja »

cygaril wrote: post #89
majikaja wrote: post #61

It would be nice if on the page they included detailed descriptions of the proofs it came up with, more information about the capabilities of the system and insights into the training process... If the data is synthetic and covers a limited class of problems I would imagine what it's doing mostly reduces to some basic search pattern heuristics which would be of more value to understand than just being told it can sol…

Proofs are here: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...

I found those, I just would have appreciated if the content of the mathematics wasn't sidelined to a separate download as if it's not important. I felt the explanation on the page was shallow, as if they just want people to accept it's a black box.

All I've learnt from this is that they used an unstated amount of computational resources just to basically brute force what a human already is capable of doing in far less time.

Re: AI solves International Math Olympiad problems at silver medal level

#116

Post by regularfry »

lolinder wrote: post #57
adverbly wrote: post #2

> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month fo…

It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theor…

I'm not sure it matters that it had access to a theorem prover. The fact that it's possible to build a black box that solves hard proofs on its own at all is the fascinating bit.

> it still took 8x as long to solve the problems as our best humans did without any computer assistance.

Give it a year and that ratio will be reversed. At least. But also it matters less how long it takes if doubling the number of things reasoning at a best-human level is pronounced "ctrl-c, ctrl-v".

Re: AI solves International Math Olympiad problems at silver medal level

#117

Post by visarga »

gjm11 wrote: post #72
wongarsu wrote: post #49

Earlier quoted context omitted.

The problem solved "within minutes" is also interesting. I'd interpret that as somewhere between 2 and 59 minutes. Given the vagueness probably on the higher end, otherwise they'd celebrate it more. The students had 6 tasks in 9 hours, so on average 1.5h per task. If you add the time a student would take to (correctly!) translate the problems to their input format, their best-case runtime is probably about as fast as…

They say "our systems" (presumably meaning AlphaProof and AlphaGeometry 2) solved one problem "within minutes", and later on the page they say that the geometry question (#4) was solved by AlphaGeometry in 19 seconds. So either (1) "within minutes" was underselling the abilities of the system, or (2) what they actually meant was that the geometry problem was solved in 19 seconds, one of the others "within minutes" (I…

Euclidian Geometry still requires constructions to solve, and those are based in intuition.

Re: AI solves International Math Olympiad problems at silver medal level

#118

Post by pclmulqdq »

dooglius wrote: post #52
Smaug123 wrote: post #35

So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The do…

The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent. However, it's unclear what initial format was given to the agents that allowed this step

So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?

Re: AI solves International Math Olympiad problems at silver medal level

#119

Post by visarga »

vlovich123 wrote: post #91
tsimionescu wrote: post #59

Earlier quoted context omitted.

That's patently false for many classes of problems. We know exactly how to solve the traveling salesman problem, and have for decades, but we're nowhere close to solving a random 1000 city case (note: there are approximate methods that can find good, but not optimal, results on millions of cities). Edit: I should say 1,000,000 city problem, as there are some solutions for 30-60k cities from the 2000s. And there are g…

We're not talking about mathematical optimality here, both from the solution found and for the time taken. The point is whether this finds results more cheaply than a human can and right now it's better on some problems while others it's worse. Clearly if a human can do it, there is a way to solve it in a cheaper amount of time and it would be flawed reasoning to think that improving the amount of time would be asymp…

> The point is whether this finds results more cheaply than a human can

If you need to solve 1000 problems in 3 days you wouldn't find the humans that can do it. So it would not be cheaper if it's not possible.

Re: AI solves International Math Olympiad problems at silver medal level

#120

Post by refulgentis »

Goalposts at the moon, FUD at "but what if its obviously fake?".

Real, exact, quotes from the top comments at 1 PM EST.

"I want to believe that the computer found it, but I can't find anything to confirm."

"Curing cancer will require new ideas"

"Maybe they used 10% of all of GCP [Google compute]"

Post reply on HN