In other news today calculator solves math problem.
AI solves International Math Olympiad problems at silver medal level
431–440 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#432Is it really such a smart thing to train a non-human "entity" to beat humans at math?
Re: AI solves International Math Olympiad problems at silver medal level
#433Re: AI solves International Math Olympiad problems at silver medal level
#434Earlier quoted context omitted.
It's not an English LLM (Large Language Model). It's a math Language Model. Not even sure it's a Large Language Model. (Maybe shares a foundational model with an English LLM; I don't know) It learns mathematical statements, and generates new mathematical statements, then uses search techniques to continue. Similar to Alpha Go's neural network, what makes it new and interesting is how the NN/LLM part makes smart guess…
yeah but it doesn't understand the exact syntax on an absolute level, does it...? I understood this to be the same as any language model applied to programming languages (aka Formal Languages). Is that mistaken?
As far as I understand, and I may be wrong here, the system is composed of two networks: Gemini and AlphaZero. Gemini, being an ordinary LLM with some fine-tunes, only does translation from natural to formal language. Then, AlphaZero solves the problem. AlphaZero, unburdened with natural language and only dealing with "playing a game in the proof space" (where the "moves" are commands to the Lean theorem prover), does not hallucinate in the same way an LLM does because it is nothing like an LLM.
Re: AI solves International Math Olympiad problems at silver medal level
#435Earlier quoted context omitted.
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.
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.)
I don't see why we should take your word for it, as opposed to just asking AlphaProof to comment instead.
Re: AI solves International Math Olympiad problems at silver medal level
#436> As part of our IMO work, we also experimented with a natural language reasoning system, built upon Gemini and our latest research to enable advanced problem-solving skills. This system doesn’t require the problems to be translated into a formal language and could be combined with other AI systems. We also tested this approach on this year’s IMO problems and the results showed great promise. Wonder what "great promi…
I don't think that's what they mean.
They explicitly stated that to achieve the current results, they had to manually translate the problem statements into formal mathematical statements:
> First, the problems were manually translated into formal mathematical language for our systems to understand.
How I understand what they're saying is that they used gemini to translate the problem statement into formal mathematical language and let DeepMath do it's magic after that initial step.
Re: AI solves International Math Olympiad problems at silver medal level
#437Earlier quoted context omitted.
It's not an English LLM (Large Language Model). It's a math Language Model. Not even sure it's a Large Language Model. (Maybe shares a foundational model with an English LLM; I don't know) It learns mathematical statements, and generates new mathematical statements, then uses search techniques to continue. Similar to Alpha Go's neural network, what makes it new and interesting is how the NN/LLM part makes smart guess…
These kind of LLMs are also very interesting for software engineering. It's just a matter of replacing Lean with something that is more oriented towards proving software properties. For example, write a formal specification of a function in Dafny on Liquid Haskell and get the LLM to produce code that is formally guaranteed to be correct. Logic-based + probability-based ML. All GOFAI ideas are still very useful.
You can also verify software like compilers in Lean:
https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
Re: AI solves International Math Olympiad problems at silver medal level
#438Earlier quoted context omitted.
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 silv…
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.
To some extent, what they do is stronger that the other contestants, who I understand don’t formally prove their answers.
Re: AI solves International Math Olympiad problems at silver medal level
#439Theorem 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"?
Replace "this thing is better than Terrence Tao at maths" with "this thing is better than Garry Kasparov at chess" and your statement would sound equally reasonable in the early 90s.
Re: AI solves International Math Olympiad problems at silver medal level
#440This is quite cool! I've found logical reasoning to be one of the biggest weak points of LLMs, nice to see that an alternative approach works better!
I've tried to enlist gpt to help me play a android game called 4=10, where you solve simple math problems, and gpt was hilariously terrible at it. It would both break the rules I described, and make math mistakes, such as claiming 6*5-5+8=10
I wonder if this new model could be integrated with an LLM somehow? I get the feeling that combining those two powers would result in a fairly capable programmer.
Also perhaps a LLM could do the translation step that is currently manual?