5 ms·

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

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 silver

dooglius 2y ago
I don't believe anything was graded by the IMO, Google is just giving itself 7 for anything proved in Lean (which is reasonable IMO), so they can't really try for partial credit so much as choose not to report a higher self-graded number.
- utopcell 2y ago
  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."
  - dooglius 2y ago
    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.
    - utopcell 2y ago
      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!
llwu 2y ago
Partial credit is quite challenging to earn, per: https://www.imo-official.org/year_statistics.aspx?year=2024 https://www.imo-official.org/year_statistics.aspx?year=2024
- Davidzheng 2y ago
  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
  - llwu 2y ago
    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.
    - gus_massa 2y ago
      Problem 2 and 5 have a lot of 1s. Sometimes thre is an interesting advance that is easirr than the full solution. Also in problem 6 the only hope for most was to get that 1 point.
lozenge 2y ago
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.
- Davidzheng 2y ago
  I think it proves lemmas it can submit all the lemmas it proved lol
- snewman 2y ago
  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.)
  - saagarjha 2y ago
    I don't see why we should take your word for it, as opposed to just asking AlphaProof to comment instead.
    - topato 2y ago
      Well, he does have twice the amount of silver medals... And can speak the English language... Although, an AI attempting to speak with the human race entirely through an esoteric math-proofing language would be an interesting take on the whole, "humans make ET contact, interact through universal language.... pause for half of the movie, military hothead wanting to blow it out of the sky, until pretty lady mathematician runs into the oval office waving a sheet of paper... OF MATH!" trope.... But now, it's a race between you and I, to see who can write the screenplay first!
  - lupire 2y ago
    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.

dooglius 2y ago

I don't believe anything was graded by the IMO, Google is just giving itself 7 for anything proved in Lean (which is reasonable IMO), so they can't really try for partial credit so much as choose not to report a higher self-graded number.

utopcell 2y ago
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."
- dooglius 2y ago
  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.
  - utopcell 2y ago
    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!

llwu 2y ago

Partial credit is quite challenging to earn, per: https://www.imo-official.org/year_statistics.aspx?year=2024 https://www.imo-official.org/year_statistics.aspx?year=2024

Davidzheng 2y ago
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
- llwu 2y ago
  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.
  - gus_massa 2y ago
    Problem 2 and 5 have a lot of 1s. Sometimes thre is an interesting advance that is easirr than the full solution. Also in problem 6 the only hope for most was to get that 1 point.

lozenge 2y ago

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.

Davidzheng 2y ago
I think it proves lemmas it can submit all the lemmas it proved lol
snewman 2y ago
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.)
- saagarjha 2y ago
  I don't see why we should take your word for it, as opposed to just asking AlphaProof to comment instead.
  - topato 2y ago
    Well, he does have twice the amount of silver medals... And can speak the English language... Although, an AI attempting to speak with the human race entirely through an esoteric math-proofing language would be an interesting take on the whole, "humans make ET contact, interact through universal language.... pause for half of the movie, military hothead wanting to blow it out of the sky, until pretty lady mathematician runs into the oval office waving a sheet of paper... OF MATH!" trope.... But now, it's a race between you and I, to see who can write the screenplay first!
- lupire 2y ago
  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.