What was the total energy consumption required to acheive this result (both training and running) And, how much CO2 was released into earths atmosphere?
AI solves International Math Olympiad problems at silver medal level
391–400 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#392Earlier quoted context omitted.
Partial credit is quite challenging to earn, per: https://www.imo-official.org/year_statistics.aspx?year=2024
Link isn't working for me can you summarize. What i heard ten years ago was that 1pt is quite common for a significant progress
Yeah, the progress has to be quite significant, no points are awarded for trivial observations. Thus scores are usually bimodal around 0 and 7. In the linked stats you can see that 1 point for P3/P5 was less common than full score on other problems.
Re: AI solves International Math Olympiad problems at silver medal level
#393Haha, what a dumb tincan (c) somebody on Twitter right now :D
Re: AI solves International Math Olympiad problems at silver medal level
#394Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
There are people that believe that mathematics is actually useful, in ways that chess or art are not. I know, most mathematicians don't think so. But let us just entertain this crazy thought for a moment. Then a proof is just a tool that tells us, oh, we have applied this piece of mathematics right. No understanding of the proof is actually required for that, and no one cares if some mathematician somewhere actually fully understands the proof. It will be OK, even expected, that the machine is better than us at finding and checking proofs.
Re: AI solves International Math Olympiad problems at silver medal level
#395Earlier quoted context omitted.
If it cannot explain how it was proven, was it actually proven?
No. Funny how these discussions too often devolve into semantics lol.
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.
Re: AI solves International Math Olympiad problems at silver medal level
#396If the system took 3 days to solve a problem, how different is this approach than a bruteforce attempt at the problem with educated guesses? Thats not reasoning in my mind.
Re: AI solves International Math Olympiad problems at silver medal level
#397Earlier quoted context omitted.
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…
The AI took a day on one of the problems so it must have generated and discarded a lot of proofs that didn't work. How could it choose which one to submit as the answer, except the objective fact of the proof passing in Lean.
When tackling IMO problems, the hard part is coming up with a good approach to the proof. Verifying your proof (and rejecting your false attempts) is much easier. You'll know which one to submit.
(Source: I am a two-time IMO silver medalist.)
Re: AI solves International Math Olympiad problems at silver medal level
#398Earlier quoted context omitted.
Also AlphaProof had to search for 60 hours for one of the IMO problems it solved.
And I understand the upper time limit for each question was 4.5 hours. So it solved one question almost immediately, two well over the allotted time (60 hrs), and two not at all. No medal for you, Grasshopper.
Contestants get 4.5 hours for each of the two days of competition. They have to solve three problems in that time, so on average you can spend 1.5 hours per problem (if you're aiming to finish all three).
That said, the gap from "can't do it at all" to "can do it in 60 hours" is probably quite a bit larger than the gap from 60 hours to 1.5 hours.
Re: AI solves International Math Olympiad problems at silver medal level
#399Why on earth did the "beastie" need the questions translating?
So it failed at the first step (comprehension) and hence I think we can request a better effort next time.
Re: AI solves International Math Olympiad problems at silver medal level
#400Earlier 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.
What makes solving IMO problems hard is usually the limits of human memory, pattern-matching, and search, not creativity. After all, these are problems that are already solved, and it is expected that many people can solve the problems in about 1 hour's time. That makes it, in principle, similar or even easier than a champsionship-level chess move, which often take more than 1 hour for a professional human (with more…
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 pool. To my understanding, a significant fraction of all high school students on Earth take some form of qualifying exam which can channel them into an IMO training program.
And as far as the being amenable to brute force (relative difficulty for humans vs. computers): it seems that chess was comparatively easier for computers, IMO problems are comparatively easier for humans, and the game of Go is somewhere in between.