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

121–130 of 564 posts

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

#121

Post by Eridrus »

visarga wrote: post #106
golol wrote: post #33

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

Search is great, search works, but there was not a tonne to learn from the AlphaGeometry paper unless you were specifically interested in solving geometry problems.

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

#122

Post by trotro »

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.

The methods are know, but the solutions to the IMO problems weren't. So the AI did extrapolate a solution.

Also, there's no reason to affirm that an eventual cure for cancer requires fundamentally new methods. Maybe the current methods are sufficient, it's just that nobody has been "smart" enough to put the pieces together. (disclaimer: not an expert at all)

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

#123

Post by pclmulqdq »

Smaug123 wrote: post #78
dooglius wrote: post #52

Earlier quoted context omitted.

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

FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (which it sounds like they didn't).

Comparing "turn photo into LaTeX" to "translate theorems into Lean" is like comparing a child's watercolor drawing to the Mona Lisa.

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

#124

Post by mathnmusic »

golol wrote: post #102
lolinder wrote: post #95

Earlier quoted context omitted.

> 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. If this were the case then the headline would be "AI solves 4/6 IMO 2024 problems", it wouldn't be claiming "silver-medal standard". Medals are generally awarded by comparison to other contestants, not to the challenges overcome. > This can become a real mathematical assistant that…

At the IMO "silver medal" afaik is define as some tange of points, which more or less equals some range of problems solved. For me it is fair to say that "silver-medal performance" is IMO langauge for about 4/6 problems solved. And what's the problem if some clickbait websites totally spin the result? They would've done it anyways even with a different title, and I also don't see the harm. Let people be wrong.

No, "silver medal" is defined as a range of points to be earned in the allotted time (4.5 hours for both papers of 3 problems each).

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

#125

Post by [deleted] »

clbrmbr wrote: post #36
petters wrote: post #6

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

IIUC, a Gemini-based system could translate the natural language questions into Lean, but in the blog post they don’t really commit to whether this was done just to generate training data or was used in the competition.

[deleted]

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

#126

Post by pishpash »

nnarek wrote: post #53
ocfnash wrote: post #40

Earlier quoted context omitted.

The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.

formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it

Exactly, a problem and its answer are just different ways of describing the same object. Every step of a proof is a transformation/translation of the same object. It would be disingenuous to say that some heavy lifting isn't done in formalizing a problem but it seems that step is also performed by a machine:

"We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty."

I'm confused, is the formalization by Gemini or "manually"? Which is it?

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

#127

Post by kypro »

visarga wrote: post #106
golol wrote: post #33

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

My old AI professor used to say that every problem is a search problem.

The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.

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

#128

Post by visarga »

robinhouston wrote: post #87

Some more context is provided by Tim Gowers on Twitter [1]. Since I think you need an account to read threads now, here's a transcript: Google DeepMind have produced a program that in a certain sense has achieved a silver-medal peformance at this year's International Mathematical Olympiad. It did this by solving four of the six problems completely, which got it 28 points out of a possible total of 42. I'm not quite s…

> If the human competitors had been allowed that sort of time per problem they would undoubtedly have scored higher.

Or if AlphaProof used more compute they could have slashed that time to 1/10 or less. It's arbitrary as long as we don't define what is the compute the AI should be entitled to use here.

Post reply on HN