gdm claims gold medal

Stream: IMO-grand-challenge

[Kunvar Thaman]

https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/

Very impressive (and respectful, to wait to announce results). I don't think this qualifies for the IMOGC, given the model is proprietary, but very impressive.

[Junyan Xu]

also no Lean, and also 35/42
solutions: https://storage.googleapis.com/deepmind-media/gemini/IMO_2025.pdf

[Kunvar Thaman]

Im surprised theres no non-lean rules requirements. The assumption that it would be formal proof system turned out to be weak.

[Junyan Xu]

What requirement? I'm not sure I understand.

[Junyan Xu]

"We can confirm that Google DeepMind has reached the much-desired milestone, earning 35 out of a possible 42 points — a gold medal score. Their solutions were astonishing in many respects. IMO graders found them to be clear, precise and most of them easy to follow."
IMO President Prof. Dr. Gregor Dolinar

[Kunvar Thaman]

I was referring to the GC rules.

"The challenge: build an AI that can win a gold medal in the competition.

To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol."

Turned out that receiving a formal representation of the problem was not required for the gold.

[Junyan Xu]

Yeah, OpenAI also showed this.

[Junyan Xu]

But IMO GC is sort of dead, the actually realized AIMO prize doesn't offer formal statements.

[Ad Astra]

Well, IMO GC has obviously grown into something much bigger than expected. Although formal rules were never officially established, I imagine the intent of this challenge was for an AI to achieve gold medal status using methods that were verifiable and reproducible. Open source is one way to accomplish that, but i do think the committee can loosen up the open source restriction a bit, now that AI labs are getting ~official invitations to the competition itself. And perhaps compromise on the Lean requirement as well. Of course, it’s ultimately up to the committee to determine what the spirit of this competition actually is.

[Junyan Xu]

Noam Brown from OpenAI said on x.com:

Also, pretty irrelevant but for completeness: the IMO reached out months ago offering to provide Lean versions of the problems immediately after the competition. We weren't planning on doing Lean so declined.

But DeepMind showed that they could still cooperate with IMO even without using Lean, and it's unclear why they didn't.

[Eric Wieser]

I don't think anyone is claiming that they have met the presumed conditions of the grand challenge, especially given the open-source requirement I believe it imposed.

[Kunvar Thaman]

Correct, no lean, no reproducability. thats 2/4 of the criteria

[Ad Astra]

Ad Astra said:

Well, IMO GC has obviously grown into something much bigger than expected. Although formal rules were never officially established, I imagine the intent of this challenge was for an AI to achieve gold medal status using methods that were verifiable and reproducible. Open source is one way to accomplish that, but i do think the committee can loosen up the open source restriction a bit, now that AI labs are getting ~official invitations to the competition itself. And perhaps compromise on the Lean requirement as well. Of course, it’s ultimately up to the committee to determine what the spirit of the competition was

As far as verifiability / reproducibility go…the whole purpose of the Lean requirement (as i underhand it) was for independent verification. But we know the IMO have already verified that the solutions from GDM are gold level. So if we did want to toy with the idea of incorporating closed source models that don’t use lean…GDM did announce that they will be inviting select mathematicians to demo this model before its public release. In that case, maybe not a bad idea for Kevin and co to link up and get their hands on the model? I’m sure Demis and GDM would be more than happy to accommodate.

https://x.com/demishassabis/status/1947337617231778168?s=46

[Mario Carneiro]

I find it a bit funny that they sell not using formal methods as a positive in the blog post

[Eric Wieser]

I think this community is quite biased, and the wider public viewed it as a weird restriction

[Kunvar Thaman]

So if we did want to toy with the idea of incorporating closed source models that don’t use lean

you cannot waive off the pre-agreed upon criteria post-hoc

[Kevin Buzzard]

Ad Astra said:

Well, IMO GC has obviously grown into something much bigger than expected. Although formal rules were never officially established, I imagine the intent of this challenge was for an AI to achieve gold medal status using methods that were verifiable and reproducible.

No, I am interested in promoting interactive theorem provers and open source methods, and the intent of the challenge at https://imo-grand-challenge.github.io/ was absolutely to demand the use of interactive theorem provers and open source methods.