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

331–340 of 564 posts

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

#331

Post by Vinnl »

yalok wrote: post #314
onemoresoop wrote: post #295

Earlier quoted context omitted.

You probably mean envious not jealous.

I'm learning something new today. In some other languages these 2 are usually the same 1 word.

Huh. So I tried to look it up just now and I'm not sure if I understand the difference. (To the extent that there is one - apparently one can mean the other, but I imagine they're usually used as follows.)

It looks like "jealous" is more being afraid of losing something you have (most commonly e.g. a spouse's affection) to someone else, whereas "envious" is wanting what someone else has?

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

#332

Post by geysersam »

golol wrote: post #33

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…

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 system is able to translate parts of the problem to logic and find a solution, that might make the system much more reliable.

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

#333

Post by onemoresoop »

yalok wrote: post #314
onemoresoop wrote: post #295

Earlier quoted context omitted.

You probably mean envious not jealous.

I'm learning something new today. In some other languages these 2 are usually the same 1 word.

No worries. I learned this too a while ago (was also using jealous instead of envious and vice versa myself). From my understanding the use of jealous is when you have something but that is threatened by some external factor, eg a partner, a friend having more fun with somebody else. Envious is when you covet something that you do not have currently but wish to, which is in this case playing with exciting tech.

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

#334

Post by [deleted] »

camjw wrote: post #235
thrance wrote: post #230

Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. IMHO, the largest contributors to AlphaProof were the people behind Lean and Mathlib, who took the daunting task of formalizing the entirety of mathematics to themselves. This lack of formalizing in math papers was what killed any attempt at automation, because AI researcher had to wrestle wi…

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

[deleted]

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

#335

Post by onemoresoop »

Vinnl wrote: post #331
yalok wrote: post #314

Earlier quoted context omitted.

I'm learning something new today. In some other languages these 2 are usually the same 1 word.

Huh. So I tried to look it up just now and I'm not sure if I understand the difference. (To the extent that there is one - apparently one can mean the other, but I imagine they're usually used as follows.) It looks like "jealous" is more being afraid of losing something you have (most commonly e.g. a spouse's affection) to someone else, whereas "envious" is wanting what someone else has?

Correct.

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

#336

Post by creata »

geysersam wrote: post #332
golol wrote: post #33

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…

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.

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

#337

Post by necovek »

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 one problem and up to 3 days for each remaining problem" means that this is unfortunately not a true representation either. If these students were given up to 15 days (5 problems at "up to 3 days each") instead of 9h, there would probably be more of them that match or beat this score too.

It really sounds like AI solved only a single problem in the 9h students get, so it certainly would not be even close to the medals. What's the need to taint the impressive result with apples-to-oranges comparison?

Why not be more objective and report that it took longer but was able to solve X% of problems (or scored X out of N points)?

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

#338

Post by knotthebest »

Davidzheng wrote: post #169
lolinder wrote: post #71

This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extrem…

I can tell you that as someone who could have gotten bronze (i was too weak for the team) and is now a math phd--I would not have scored as well as alphaproof in three days most likely. In most problems either you find an idea soon or it can be much much longer. It's just not a matter of working and constant progress.

Skill issue tbh

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

#339

Post by muglug »

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.

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

#340

Post by panagathon »

ComplexSystems wrote: post #324
Ericson2314 wrote: post #99

Earlier quoted context omitted.

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

This is the greatest idea ever. Why doesn't this exist?

This does sound like a lot of fun. Since this AI only reaches silver level, presumably such a contest could be quite competitive, with it not yet being clear cut whether a human or a tool-assisted human would come out on top, for any particular problem.
Post reply on HN