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

41–50 of 564 posts

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

#41

Post by ozten »

balls187 wrote: post #39

What was the total energy consumption required to acheive this result (both training and running) And, how much CO2 was released into earths atmosphere?

Compared to all of the humans who compete at this level and their inputs and outputs for the trailing 5 years.

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

#42

Post by golol »

petters wrote: post #6

The problems were first converted into a formal language. So they were partly solved by the AI

Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini model which formalizes natural language problems, and this is how they generated training data for AlphaProof. I would therefore expect that they could have also formalized the IMO problems with that model and just did it manually because the point is not to demonstrate formalizing but instead proof capabilities.

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

#43

Post by Smaug123 »

rpois wrote: post #30
petters wrote: post #6

The problems were first converted into a formal language. So they were partly solved by the AI

Does this formalization process include giving it the answer it should try to prove?

Nope, per Oliver Nash who worked on the thing: https://news.ycombinator.com/item?id=41070372

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

#45

Post by nwoli »

Ericson2314 wrote: post #26
Ericson2314 wrote: post #23

The lede is a bit buried: they're using Lean! This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general. Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.

They're def gonna go after the Riemann hypothesis with this, hehe.

Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that

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

#46

Post by poincaredisk »

ComplexSystems wrote: post #25
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…

Or the simultaneous discovery of thousands of cryptographic exploits...

Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.

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

#47

Post by golol »

PaulHoule wrote: post #10

See https://en.wikipedia.org/wiki/Automated_Mathematician for an early system that seems similar in some way.

This Wikipedia page makes AM kind of comes across as a nonsense project whose outputs no one (besides the author) bothered to decipher.

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

#49

Post by wongarsu »

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…

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 a silver-medalist would take to solve the problem on their own.

But even if they aren't as fast as humans yet this is very valuable. Both as a stepping stone, and because at a certain scale compute is much easier to scale than skilled mathematicians.

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

#50

Post by vlovich123 »

nnarek wrote: post #37
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…

"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)

The thing is though, once we have a benchmark that we pass, it’s pretty typical to be able to bring down time required in short order through performance improvements and iterating on ideas. So if you knew you had GAI but it took 100% of all GCP for 3 years to give a result, within the next 5 years that would come down significantly (not least of which you’d build HW dedicated to accelerating the slow parts).
Post reply on HN