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

161–170 of 564 posts

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

#161

Post by pishpash »

kypro wrote: post #127
visarga wrote: post #106

Earlier quoted context omitted.

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

There's no problem with search. The goal is to search most efficiently.

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

#163

Post by dsign »

trotro wrote: post #122
10100110 wrote: post #83

Earlier quoted context omitted.

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)

I think you are correct though. We don't need new physics to cure cancer. But we may need information-handling, reasoning and simulation systems which are orders of magnitude bigger and more complex than anything we have this year. We also need to stop pussy-footing and diddling with ideologies and start working on the root cause of cancer and almost every other disease, which is aging.

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

#164

Post by blackbear_ »

lolinder wrote: post #71

This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extrem…

And why aren't you complaining that human participants could train and study for thousands of hours before attempting the problems? And that the training materials they used was itself created and perfected by hundreds of other people, after having themselves spend countless hours studying?

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

#166

Post by pishpash »

golol wrote: post #42
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 de…

Yet the facts at hand are the opposite of what you say. Reliable formalizer was the more difficult problem than solving formalized IMO problems, because they have not produced one.

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

#167

Post by ajross »

summerlight wrote: post #100
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…

To speak generally, that translation part is much easier than the proof part. The problem with automated translation is that the translation result might be incorrect. This happens a lot when even people try formal methods by their hands, so I guess the researchers concluded that they'll have to audit every single translation regardless of using LLM or whatever tools.

> To speak generally, that translation part is much easier than the proof part.

To you or me, sure. But I think the proof that it isn't for this AI system is that they didn't do it. Asking a modern LLM to "translate" something is a pretty solved problem, after all. That argues strongly that what was happening here is not a "translation" but something else, like a semantic distillation.

If you ask a AI (or person) to prove the halting problem, they can't. If you "translate" the question into a specific example that does halt, they can run it and find out.

I'm suspicious, basically.

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

#169

Post by Davidzheng »

lolinder wrote: post #71

This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extrem…

I can tell you that as someone who could have gotten bronze (i was too weak for the team) and is now a math phd--I would not have scored as well as alphaproof in three days most likely. In most problems either you find an idea soon or it can be much much longer. It's just not a matter of working and constant progress.

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

#170

Post by llwu »

thomasahle wrote: post #145
summerlight wrote: post #100

Earlier quoted context omitted.

To speak generally, that translation part is much easier than the proof part. The problem with automated translation is that the translation result might be incorrect. This happens a lot when even people try formal methods by their hands, so I guess the researchers concluded that they'll have to audit every single translation regardless of using LLM or whatever tools.

You'd think that, but Timothy Gowers (the famous mathematician they worked with) wrote ( https://x.com/wtgowers/status/1816509817382735986 ) > However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. So didn't actually solve auto…

> We don't have a way to verify formalizations the same way.

While there is no perfect method, it is possible to use the agent to determine if the statement is false, has contradictory hypotheses, or a suspiciously short proof.

Post reply on HN