Example of proof from AlphaProof system: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
AI solves International Math Olympiad problems at silver medal level
31–40 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#32[flagged]
Re: AI solves International Math Olympiad problems at silver medal level
#33This 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 basic theory building like creating auxilliary definitions and Lemmas. I really think this is the holy grail of proof-assistance and will allow us to formalize most mathematics that we create very naturally. Humans will work podt-rigorously and let the machine asisst with filling in the details.
Re: AI solves International Math Olympiad problems at silver medal level
#34The problems were first converted into a formal language. So they were partly solved by the AI
Yes and it is difficult for me to believe that there is not useful human analysis and understanding involved in this translation that the AI is helpless without. But that I suppose is a problem that could be tackled with a different model...
Even so, having a human formalize the problems and an AI to find machine checkable proofs could be very useful for mathematicians.
Re: AI solves International Math Olympiad problems at silver medal level
#35So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing:
> First, the problems were manually translated into formal mathematical language for our systems to understand.
The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The downloadable solutions from https://storage.googleapis.com/deepmind-media/DeepMind.com/B... don't make it clear whether the set {foo} was decided by a human during this translation step, or whether the computer found it. I want to believe that the computer found it, but I can't find anything to confirm. Anyone know?
Re: AI solves International Math Olympiad problems at silver medal level
#36The problems were first converted into a formal language. So they were partly solved by the AI
IIUC, a Gemini-based system could translate the natural language questions into Lean, but in the blog post they don’t really commit to whether this was done just to generate training data or was used in the competition.
Re: AI solves International Math Olympiad problems at silver medal level
#37> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month fo…
"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)
Re: AI solves International Math Olympiad problems at silver medal level
#38That's great, but does that particular model also know if/when/that it does not know?
While that was probably meant to be rhetorical, the answer surprisingly seems to be an extremely strong "Yes, it does". Exciting times.
Re: AI solves International Math Olympiad problems at silver medal level
#39What was the total energy consumption required to acheive this result (both training and running)
And, how much CO2 was released into earths atmosphere?
Re: AI solves International Math Olympiad problems at silver medal level
#40So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The do…
The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.