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

341–350 of 564 posts

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

#341

Post by Davidzheng »

necovek wrote: post #337

This is certainly impressive, but whenever IMO is brought up, a caveat should be put out: medals are awarded to 50% of the participants (high school students), with 1:2:3 ratio between gold, silver and bronze. That puts all gold and silver medalists among the top 25% of the participants. That means that "AI solves IMO problems better than 75% of the students", which is probably even more impressive. But, "minutes for…

In my opinion (not Google s) the only reason they didn't get gold this year (apart from being unlucky on problem selection) is that they didn't want to try for any partial credit in P3 and P5. They are so close to the cut off and usually contestants with a little bit of progress can get 1 point. But i guess they didn't want to get a gold on a technicality--it would be bad press. So they settled in a indisputable silver

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

#342

Post by Davidzheng »

sebzim4500 wrote: post #289
jeremyjh wrote: post #17

Earlier quoted context omitted.

Yes and it is difficult for me to believe that there is not useful human analysis and understanding involved in this translation that the AI is helpless without. But that I suppose is a problem that could be tackled with a different model...

It is vastly easier to do the formalization than to actually solve the problem. Any undergraduate with some lean familiarity could do it in minutes.

Disagree! Some problems are much harder than others. If you don't believe me please go formalize P5 in this year imo.

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

#343

Post by Davidzheng »

trotro wrote: post #132
petters wrote: post #6

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

But formalization is the easy part for humans. I'm sure every mathematician would be be happy if the only thing required to prove a result was to formalize it in Lean and feed it to the AI to find the proof.

Not sure every mathematician would be happy to do this... it sounds much less pleasant than thinking. It's like saying mathematicians would rather be programmers lol. It's a significant difficult problem which i believe should be left completely to AI. Human formalization should become dead

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

#344

Post by Davidzheng »

cygaril wrote: post #66
nnarek wrote: post #53

Earlier quoted context omitted.

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

Come up with many possible answers, formalize them all, and then try to prove or disprove each of them.

This is probably partially what they did idk why it's downvoted lol

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

#345

Post by Davidzheng »

booleandilemma wrote: post #329
lumb63 wrote: post #312

Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? For example, suppose a computer is asked to prove the sum of two even numbers is an even number. It could pull up its list of “things it knows about even numbers”, namely that an even number modulo 2 is 0. Assuming the first number is “a” and the second is “b”,…

Proofs require a certain ingenuity that computers just don't have, imo. A computer would never be able to come up with something like Cantor's diagonalization proof on its own.

Are you sure alphaproof can't

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

#346

Post by dinobones »

I see DeepMind is still playing around with RL + search algorithms, except now it looks like they're using an LLM to generate state candidates.

I don't really find that this impressive. With enough compute you could just do n-of-10,000 LLM generations to "brute force" a difficult problem and you'll get there eventually.

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

#347

Post by Davidzheng »

oXman038 wrote: post #227
quirino wrote: post #80

I honestly expected the IOI (International Olympiad of Informatics) to be "beaten" much earlier than the IMO. There's AlphaCode, of course, but on the latest update I don't think it was quite on "silver medal" level. And available LLM's are probably not even on "honourable mention" level. I wonder if some class of problems will emerge that human competitors are able to solve but are particularly tricky for machines.…

IOI problems are more close to IMO combinatoric problems than other IMO problem types. That might be the reason for that delay. I personally like only combinatoric problems in IMO. Thats why I drop math track and went IOI instead. I feel why combinatoric is harder for AI models is the same reason why LLM's are not great at reasoning anything out of distribution. LLM's are good pattern recognizers and fascinating at t…

Are you convinced there's a "reason " AI today is worse at combo? Like i don't see enough evidence that it's not an accident.

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

#348

Post by Davidzheng »

knotthebest wrote: post #338
Davidzheng wrote: post #169

Earlier quoted context omitted.

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.

Skill issue tbh

Agreed :'(

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

#349

Post by GuB-42 »

fancyfredbot wrote: post #70

I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.

I don't know about that. A lot of the work that should have been very satisfying turned out to be boring as hell, if not toxic, while at the same time, some apparently mundane stuff turned out to be really exciting.

I found the work environment to be more important than the subject when it comes to work satisfaction. If you are working on a world changing subject with a team of assholes, you are going to have a bad time, some people really have a skill for sucking the fun out of everything, and office politics are everywhere, especially on world changing subjects.

On the other hand, you can have a most boring subject, say pushing customer data to a database, and have the time of your life: friendly team, well designed architecture, time for experimentation and sharing of knowledge, etc... I have come to appreciate the beauty of a simple thing that just works. It is so rare, maybe even more rare than scientific breakthroughs.

Now, you can also have an awesome work environment and an awesome subject, it is like hitting the jackpot... and a good reason to be envious.

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

#350

Post by necovek »

apsec112 wrote: post #68
ToucanLoucan wrote: post #60

Earlier quoted context omitted.

I am so exhausted of the AI hype nonsense. LLMs are not fucking curing cancer. Not now, not in five years, not in a hundred years. That's not what they do. LLM/ML is fascinating tech that has a lot of legitimate applications, but it is not fucking intelligent, artificial or otherwise, and I am sick to death of people treating it like it is.

What observation, if you saw it, do you think would falsify that hypothesis?

It seems unlikely people will employ only ML models, especially LLM, to achieve great results: they will combine it with human insights (through direction and concrete algorithms).

It's obvious that's happening with LLMs even today to ensure they don't spew out too much bullshit or harmful content. So let's get to a point where we can trust AI as-is first, and let's talk about what's needed to achieve the next milestone after and if we get there.

And I love asking every new iteration of ChatGPT/Gemini something along the lines of "What day was yesterday if yesterday was a Thursday?" It just makes me giggle.

Post reply on HN