AI solves International Math Olympiad problems at silver medal level

Post by awesomeMilou » Thu, Jul 25, 2024, 11:21 PM UTC

acchow wrote: post #352

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…

But computers get faster each year, so even with zero progress in actual AI, this will reach human-student speeds in a few years (need a 40x speed up)

Post by sebzim4500 » Thu, Jul 25, 2024, 11:25 PM UTC

golol wrote: post #64

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

I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like {Formal description of the set in question} = ? And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above. I doubt they would claim to solve the problem if they provided half of the answer.

Post by lanstin » Thu, Jul 25, 2024, 11:26 PM UTC

creata wrote: post #336

geysersam wrote: post #332

Earlier quoted context omitted.

I imagine a system like this to be vastly more useful outside the realm of mathematics research. You don't need to be able to prove very hard problems to do useful work. Proving just simple things is often enough. If I ask a language model to complete a task, organize some entries in a certain way, or schedule this or that, write a code that accomplishes X, the result is typically not trustworthy directly. But if the…

But for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.

Post by [deleted] » Thu, Jul 25, 2024, 11:31 PM UTC

Davidzheng wrote: post #347

oXman038 wrote: post #227

Earlier quoted context omitted.

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.

Post by lozenge » Thu, Jul 25, 2024, 11:38 PM UTC

Davidzheng wrote: post #341

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