AI solves IMO problems at silver medal level

Re:AI solves IMO problems at silver medal level by ZenMikey on Thursday July 25, 2024 @11:55AM (#41070126)

I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by qsort on Thursday July 25, 2024 @12:05PM (#41070256)

I can't find a link to an actual paper, that just seems to be a blog post. But from what I gather the problems were manually translated to Lean 4, and then the program is doing some kind of tree search. I'm assuming they are leveraging the proof checker to provide feedback to the model.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by tsoj on Thursday July 25, 2024 @12:38PM (#41070642)

This is NOT the paper, but probably a very similar solution: https://arxiv.org/abs/2009.03393

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by visarga on Thursday July 25, 2024 @01:06PM (#41070933)

> just fumbling its way around until it guessed correctly

As opposed to 0.999999% of the human population who can't do it even if their life depends on it?

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by logicchains on Thursday July 25, 2024 @04:14PM (#41072882)

I guess you mean 99.9999%?

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by dsign on Thursday July 25, 2024 @01:45PM (#41071324)

I was going to come here to say that. I remember being a teenager and giving up in frustration at IMO problems. And I was competing at IPhO.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by kevinventullo on Thursday July 25, 2024 @07:43PM (#41074606)

Yeah, as a former research mathematician, I think “fumbling around blindly” is not an entirely unfair description of the research process.

I believe even Wiles in a documentary described his search for the proof of Fermat’s last theorem as groping around in a pitch black room, but once the proof was discovered it was like someone turned the lights on.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by lacker on Thursday July 25, 2024 @01:21PM (#41071103)

The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.

So they had three days to keep training the model, on synthetic variations of each IMO problem.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by thomasahle on Thursday July 25, 2024 @01:49PM (#41071357)

They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect.

Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by utopcell on Thursday July 25, 2024 @07:46PM (#41074629)

I'm at work and reading this article is the first thing I did this morning. What's your point ?

[ Parent | on HN ]