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

501–510 of 564 posts

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

#501

Post by lupire »

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…

But many more of those students (including many not in the contest) could solve those problems given more time than the 4.5hr sessions.

If these problems were important to solve, redundantly by thousands or millions of people (like the real work that most people do), far more people would put in the effort to learn how to solve these problems.

It's just a weird comparison. Contests are very artificially structured in ways that don't make sense for comparing to computers.

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

#502

Post by lupire »

snewman wrote: post #397
lozenge wrote: post #370

Earlier quoted context omitted.

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

You are a human, not an AI. You know whether your idea seems related to the solution. The AI has thousands of ideas and doesn't know which are better. Graders shouldn't accept a thousand guesses grubbing for 1 point.

If verifying a good idea is easy, then the evidence shows that the AI didn't have good ideas for the other 2 problems.

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

#503

Post by lupire »

awesomeMilou wrote: post #362
acchow wrote: post #352

Earlier quoted context omitted.

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)

Could you explain where the 40x speedup comes from, given that literally the biggest problem in semi conductors right now is smaller node size?

Improved parallelization. More cost in less time.

This is Nvidia's main area of research now.

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

#504

Post by _heimdall »

Thorrez wrote: post #428
_heimdall wrote: post #404

Earlier quoted context omitted.

This is really interesting. I would have expected the understanding to be that humans make a guess, test it, and learn from what did or did not work. The lessons learned from the prior tests would impact future guesses. Do you know if a system like the OP is learning from failed tests to guide future tests, or is it a truly a brute force search as if it were trying to mine bitcoin?

This quote from the article sounds like it learns from failed tests: >We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution…

Reading between the lines a bit, that does answer the question I had though don't think I I clarified very well.

I read that to say the model's token weights are adjusted as it goes, so in an LLM sense it is kind of learning. It isn't reasoning through an answer in the way a human does though. Meaning, the model is still just statistically predicting what an answer may be and checking if it worked.

I wouldn't chalk that up to learning at all. An AI solving complex math doesn't even seem too impressive to me with the predictive loop approach. Computers are well adept at math, throwing enough compute hardware at it to brute force an answer isn't suprising. I'd be really impressed if it could reliably get there with a similar number of failed attempts as a human, that could indicate that it really learned and reasoned rather than rammed through a mountain of failed guesses.

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

#506

Post by badrunaway »

lupire wrote: post #501
SonOfLilit wrote: post #465

Earlier quoted context omitted.

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…

But many more of those students (including many not in the contest) could solve those problems given more time than the 4.5hr sessions. If these problems were important to solve, redundantly by thousands or millions of people (like the real work that most people do), far more people would put in the effort to learn how to solve these problems. It's just a weird comparison. Contests are very artificially structured in…

I think what we need to look at is that AI systems were not able to do it before and now they are able to do it. Sooner these systems with millions of dollars of compute will just scale the algorithms and beat humans at this as well - just like they did for chess, go, shogi etc.

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

#507

Post by badrunaway »

lupire wrote: post #502
snewman wrote: post #397

Earlier quoted context omitted.

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

You are a human, not an AI. You know whether your idea seems related to the solution. The AI has thousands of ideas and doesn't know which are better. Graders shouldn't accept a thousand guesses grubbing for 1 point. If verifying a good idea is easy, then the evidence shows that the AI didn't have good ideas for the other 2 problems.

we are talking about lean proofs. Given a formal statement and a proof - the lean can verify whether it's correct or not. It's like generating computer programs to solve a problem - the problem lied in generating useful solutions/sub-solutions so that the search is effective. They achieve this via using gemini as a lean proof generator aka. using a world model LLM fine tuned to generate lean proofs in a more effective manner.

Humans are even better at this as you mention - but effectively the approach is similar. Come up with lot of ideas and see what proves it.

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

#508

Post by RealityVoid »

raincole wrote: post #247
camjw wrote: post #235

Earlier quoted context omitted.

> Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. This seems so weird to me - AGI is undefined as a term imo but why would you expect "producing something generally intelligent" (i.e. median human level intelligence) to be significantly harder than "this thing is better than Terrence Tao at maths"?

Because "Generally Intelligent" is a very broad and vague term. "Better than Terrence Tao at solving certain formalized problems" (not necessarily equal to "Better that Terrence Tao at maths) isn't.

Not to join the hate train but it probably isn't better than Terrence Tao at solving the problems either, since this Tao would have probably been able to solve the problem himself and would have probably taken less time. There were participants in this contest that were better than the AI.

Still, an impressive result for sure.

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

#509

Post by hyperbovine »

camjw wrote: post #292
hyperbovine wrote: post #275

Earlier quoted context omitted.

What if the proof were incomprehensible to humans?

I think that is unlikely to be the case - the classic example of a proof that human's "can't understand" is the Four Colour Theorem, but thats because the proof is a reduction to like 100000 special cases which are checked by computer. To what extent is the proof of Fermat's Last Theorem "incomprehensible to humans" because only like a dozen people on the planet could truly understand it - I don't know. The point of…

I think the 4-color theorem is rather different though. It reduced to a large number of cases that can in principle each be verified by a human, if they were so inclined (indeed a few intrepid mathematicians have done so over the years, at least partially.) The point of using a computer was to reduce drudgery, not to prove highly non-obvious things.

Thinking back to Wiles' proof of FLT, it took the community several years of intense work just to verify/converge on the correct result. And that proof is ~130 pages.

So, what if the computer produced a provably correct, 4000-page proof of the Goldbach conjecture?

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

#510

Post by humansareok1 »

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.

There's a lot of automated proof checkers out there. Presumably you would just run any solution from an AI through those.
Post reply on HN