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

531–540 of 564 posts

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

#531

Post by _heimdall »

Thorrez wrote: post #521
_heimdall wrote: post #504

Earlier quoted context omitted.

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

>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?

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

#532

Post by _heimdall »

sdenton4 wrote: post #520
_heimdall wrote: post #504

Earlier quoted context omitted.

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

Computers are good at arithmetic, not math... There's definitely an aspect of this that is 'airplanes, not birds.' Just because the wings don't flap doesn't mean it can't fly, though.

That's totally fair, though wouldn't the algorithm here have to reduce the math proofs to arithmetic that can be computed in silico?

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

#533

Post by mensetmanusman »

muglug wrote: post #339
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…

> What's the need to taint the impressive result with apples-to-oranges comparison? Most of DeepMind’s research is a cost-centre for the company. These press releases help justify the continued investment both to investors and to the wider public.

Cost centers are profit centers when R&D is successful.

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

#534

Post by bbor »

danielheath wrote: post #430
bbor wrote: post #405

Earlier quoted context omitted.

yeah but it doesn't understand the exact syntax on an absolute level, does it...? I understood this to be the same as any language model applied to programming languages (aka Formal Languages). Is that mistaken?

Yes, but the problem space means that invalid outputs can be quickly identified - whereas general programming isn’t necessarily amenable to rapid checks.

I mean, aren’t you just describing formal language syntax? Seems like a fundamentally similar situation —- the computer can automatically flag any syntax errors in a millisecond by checking it against the generating grammar for that language. Thats what makes a formal language in the first place, I think!

I do think this language is considerably more robust than the typical programming language, which means a sound program is more likely to end up being valid/“correct”. But still, that’s a difference of degree, not kind, IMO

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

#535

Post by YeGoblynQueenne »

lucioperca wrote: post #487
YeGoblynQueenne wrote: post #482

Earlier quoted context omitted.

Sure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).

https://github.com/leela-zero/leela-zero You can just use another implementation nowadays.

And how does Leela compare to AlphaGo?

(We don't know because we can't run AlphaGo to compare them).

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

#536

Post by utopcell »

dooglius wrote: post #385
utopcell wrote: post #361

Earlier quoted context omitted.

From the article: "Our solutions were scored according to the IMO’s point-awarding rules by prominent mathematicians Prof Sir Timothy Gowers, an IMO gold medalist and Fields Medal winner, and Dr Joseph Myers, a two-time IMO gold medalist and Chair of the IMO 2024 Problem Selection Committee."

Fair enough. Although I think the question is whether P3/P5 were given zero points vs not evaluated vs evaluated but not published. I don't think it is surprising that Lean-verified proofs get a 7.

It is an interesting question: how this new system quantifies progress and whether it can detect that a chain of reasoning is close to the solution. Although it was just 2 points shy of a golden medal (1 point partial credit per problem not solved?), I'd suspect that the team would want a clean victory, given the magnitude of the claim. I bet next year's results would be 42/42. Deep Mind is unstoppable!

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

#537

Post by SJC_Hacker »

The kicker with some of those math competition problems, there will be problems that reduce to finding all natural numbers for which some statement is true. These are almost always small numbers, less than 100 in most circumstances.

Which means these problems are trivial to solve if you have a computer - you can simply check all possibilities. And is precisely the reason why calculators aren't allowed.

But exhaustive searches are not feasible by hand in the time span the problems are supposed to be solved - roughly 30 minutes per problem. You are not supposed to use brute force, but recognize a key insight which simplifies the problem. And I believe even if you did do an exhaustive search, simply giving the answer is not enough for full points. You would have to give adequate justification.

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

#540

Post by gowld »

Smaug123 wrote: post #29
Ericson2314 wrote: post #23

The lede is a bit buried: they're using Lean! This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general. Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.

That's not necessarily an edge. https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-math...

has the example:

  0 ≤ x^2 if x : ℝ
which humans simply use without proof. The IMO doesn't challenge participants to prove everything, only the main ideas.
Post reply on HN