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

541–550 of 564 posts

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

#541

Post by snewman »

okintheory wrote: post #450
snewman wrote: post #400

Earlier quoted context omitted.

Why do you say these are problems that are already solved? Sure, they're often variations on existing themes, but the same is true for chess positions and, honestly, almost everything else in any field of human endeavor. Agreed that the absolute upper tier of chess players have trained longer and harder than most or all IMO contestants. Though I do wonder which (top-tier chess or the IMO) draws on a larger talent poo…

These problems are literally already solved? Of course, the IMO problem designers make sure the problems have solutions before the use them. That's very different than math research, where it's not known in advance what the answer is, or even that there is good answer.

I'm saying they weren't solved until the problem composer (created and) solved them. They're not, in general, problems for which solutions have been lying around. So "these are problems that are already solved" isn't introducing anything interesting or useful into the discussion. The post I was replying to was trying to draw a contrast with chess moves, presumably on the grounds that (after the opening) each position in a chess game is novel, but IMO problems are equally novel.

It's true that IMO problems are vetted as being solvable, but that still doesn't really shed any information on how the difficulty of an IMO problem compares to the difficulty of chess play.

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

#542

Post by Ericson2314 »

sebzim4500 wrote: post #367
Ericson2314 wrote: post #99

Earlier quoted context omitted.

Hehe, well, we'll need to have a tool-assited international math Olympiad then.

If the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.

Well, hopefully that changes soon :)

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

#543

Post by astromaniak »

SonOfLilit wrote: post #465
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…

I have met IMO competitors. They are insanely smart. I wouldn't imagine it's possible to be that smart before I started hanging in these circles. So more like 25% of 0.01% of high school students. Time is not a very interesting dimension here, because humans don't use the same CPU as huge GPU clusters. The binary "is it able to reach a solution given enough resources?" is more interesting (for GPT/Claude the answer i…

I've seen chess players, they are smart too. So what? Specialized model on commodity hardware beats most of them, if not all. This doesn't mean model is smarter. The same could be here. Is it possible that solutions are one step from model's database, or training set. Humans don't remember this much and have to do many more actions in their heads.

In other words model which can solve any/most school / college exam problem isn't necessarily smart. It can be just a database, or, in fact, a lookup table. Smarter version can be a lookup + 1 step test. Not saying it's bad, but it doesn't scale to less formalized domains. BTW, in this case formalization was done by humans.

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

#544

Post by necovek »

SonOfLilit wrote: post #465
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…

I have met IMO competitors. They are insanely smart. I wouldn't imagine it's possible to be that smart before I started hanging in these circles. So more like 25% of 0.01% of high school students. Time is not a very interesting dimension here, because humans don't use the same CPU as huge GPU clusters. The binary "is it able to reach a solution given enough resources?" is more interesting (for GPT/Claude the answer i…

You probably misinterpreted the above: 25% of the participants in IMO, who are generally high school students. Never claimed that 25% of all high schoolers would do better.

Now, you may say how time is not a useful dimension here, but really, this is where we are seeing a lot of these advances come from: general researchers today do get access to huge compute capability, allowing them to quickly iterate on different ideas. In a sense, they can be less smart about their use of resources and simply try things out: this does drive the innovation (compared to waiting for their turn on a supercomputer nearby).

And finally, time is essential even for humans: given a couple hundred years, they will find the proof for Fermat's last theorem, but they might not do it in 4.5h. Since we are comparing AI capabilities to humans in the article, it's very possible that increased compute will never allow AI to find novel proofs we have not come up with either. That's where the AI bit comes in: we know that brute searching through the entire possible space of proofs is still too expensive for our compute capabilities, so we need AI to emulate our "intuition" when looking for the direction to narrow down the search.

So there are really two reasons time matters: 1. getting enough of compute might still be far away (heck, prime factorization and elliptic curves are still the basis of the most of world cryptography for that reason) and 2. maybe it's not even enough to increase compute capability to make huge jumps in problem solving capabilities (iow, maybe we are reaching maximum of where the approach can take us).

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

#545

Post by highcountess »

dpbriggs wrote: post #142
highcountess wrote: post #32

[flagged]

This is more analogous to programmers working with copilot. There's an exciting possibility here of mathematicians feeding these systems subproblems to assist in proving larger theorums.

It was not meant to be a serious comment even though it seems it may have touched a nerve.

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

#546

Post by SonOfLilit »

Davidzheng wrote: post #524
SonOfLilit wrote: post #493

Earlier quoted context omitted.

I formalized it last night, to a level that an IMO trainer agreed was adequate. Took maybe 15 minutes. Find n such that p(n) and not p(n-1). p(n): exists(f: state -> move) such that solves(f, n) state: solved | illegal | (k, is_first_move in {T,F}, px in (1,2023), py in (1,2024+1), mapping from x,y to {T,F, ?}) initial_state(n): (n, T, 1, 1, {(x,y) -> ?}) move: U|D|L|R|(x in (1,2023)) power: ((a -> a), integer) -> (a…

I find it incredibly impressive you did this in 15 minutes! You should really help out in formalizing math (completely serious). Personally in the past I tried a few times to formalize some statements and sometimes I found that the mathlib libraries were pretty lacking in these more open-ended problems (I wanted to reason about lists and stuff). But it seems that I am just very bad at formalization lol.

Formalization is mechanical work, lets leave it for computers to do :)

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

#547

Post by Thorrez »

_heimdall wrote: post #531
Thorrez wrote: post #521

Earlier quoted context omitted.

>with a similar number of failed attempts as a human I'd be hard to know how many failed attempts the human made. Humans are constantly thinking of ideas and eliminating them quickly. Possibly to fast to count.

Ive never competed in math competitions at this level, but I would have expected it to be pretty clear to the human when they tested a different solution. As complex as the proofs are, is it really feasible that they are testing out a full proof in their head without realizing it?

Hmm, I think it comes down to what the definition of "testing" and "attempt". A human will generate many ideas, and eliminate them without creating full proofs, by just seeing that the idea is going in the wrong direction.

It sounds like AlphaProof will doggedly create full proofs for each idea.

Is what the human is doing testing attempts?

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

#548

Post by rldjbpin »

SonOfLilit wrote: post #462
rldjbpin wrote: post #446

Earlier quoted context omitted.

as a noob, i feel that formalizing is a major part of solving the problem by yourserlf. my assessment is that once you identify certain patterns, you can solve problems by memorizing some patterns. but people might me can struggle with the first stage and solve the wrong problem. still good progress nonetheless. won't call the system sufficient by itself tho.

My mathematician friend said problem 5 (I think? With the monsters) seems hard to formulate, so I spent 15 minutes formulating it in pseudo-haskell. Then he gave me a huge hint to the solution, after which it only took me a couple of hours to solve. (Formalizing the solution is of course the hardest part, and might serve as a good masters dissertation I think)

please pardon my ignorance, but to me a tower of hanoi question as a middle-schooler was the hardest thing to comprehend. but after learning about it, it is no longer quite as challenging to tackle.

i understand that there are very hard questions for the olympiad. but it might be possible to learn about some recurring types of them by looking at past instances. it may not be the meta for IMO but has been for other kinds of exams.

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

#549

Post by borggambit »

necovek wrote: post #350
apsec112 wrote: post #68

Earlier quoted context omitted.

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 milest…

Thanks for that what day was yesterday prompt. I have ran across these situations before but never quite like that.

What is great about that Thursday prompt is how naked the LLM is to the reality that it knows absolutely nothing in the way we think of "to know". The bubble we are in is just awesome to behold.

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

#550

Post by auggierose »

cynicalpeace wrote: post #523
auggierose wrote: post #395

Earlier quoted context omitted.

Funny how people don't understand basic logic. If it is a proof in a logic, and the machine checked that proof, it is a proof, no matter that no human actually understands it. A human doesn't need to understand the proof, they just have to understand why the proof is a proof.

We just have different definitions of what a proof is. Hence, semantics.

I would rather say that I actually have a definition of what a proof is, and you don't. But feel free to prove me wrong (pun intended), and tell me yours.
Post reply on HN