Is it one of those slowly slowly then suddenly things? I hope so
AI solves International Math Olympiad problems at silver medal level
421–430 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#422Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
Eh, people definitely care. AI has completely changed chess. Non viable lines have been proven viable and vice versa. All the pros study and develop new lines with AI.
Re: AI solves International Math Olympiad problems at silver medal level
#423Like it understands any of it
Re: AI solves International Math Olympiad problems at silver medal level
#424Like it understands any of it
Do you understand any of it?
Re: AI solves International Math Olympiad problems at silver medal level
#425Please could someone explain, very simply, what the training data was composed of?
Re: AI solves International Math Olympiad problems at silver medal level
#426> 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 promise" entails. Because it's hard to imagine Gemini and other transformer-based models solving these problems with reasonable accuracy, as there is no elimination of hallucination. At least in the generally available products.
Re: AI solves International Math Olympiad problems at silver medal level
#427Earlier quoted context omitted.
I imagine a system like this to be vastly more useful outside the realm of mathematics research. You don't need to be able to prove very hard problems to do useful work. Proving just simple things is often enough. If I ask a language model to complete a task, organize some entries in a certain way, or schedule this or that, write a code that accomplishes X, the result is typically not trustworthy directly. But if the…
But for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.
My intuition is that a regular LLM is better att coming up with a correct task description from a fuzzy description than it is at actually solving tasks.
Re: AI solves International Math Olympiad problems at silver medal level
#428Earlier 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…
This is really interesting. I would have expected the understanding to be that humans make a guess, test it, and learn from what did or did not work. The lessons learned from the prior tests would impact future guesses. Do you know if a system like the OP is learning from failed tests to guide future tests, or is it a truly a brute force search as if it were trying to mine bitcoin?
This quote from the article sounds like it learns from failed tests:
>We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. 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.
Re: AI solves International Math Olympiad problems at silver medal level
#429The problems were first converted into a formal language. So they were partly solved by the AI
Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini model which formalizes natural language problems, and this is how they generated training data for AlphaProof. I would therefore expect that they could have also formalized the IMO problems with that model and just did it manually because the point is not to de…
If they could have solved it, they would have. But I agree that language models will be able to do it.
Re: AI solves International Math Olympiad problems at silver medal level
#430Earlier 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?
Yes, but the problem space means that invalid outputs can be quickly identified - whereas general programming isn’t necessarily amenable to rapid checks.