[dead]
AI solves International Math Olympiad problems at silver medal level
411–420 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#412Earlier quoted context omitted.
> However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually so…
> A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually solve them? Formal proofs can be mechanically checked if it's correct or not. We just don't know what's the answer. Think it as an extremely rigorous type system that typically requires really long type annotations, like annotation itself is a comple…
Ah, thanks. That makes a lot of sense now.
Re: AI solves International Math Olympiad problems at silver medal level
#413> The system was allowed unlimited time; for some problems it took up to three days. The students were allotted only 4.5 hours per exam.
I know speed is just a matter of engineering, but looks like we still have a ways to go. Hold the gong...
Re: AI solves International Math Olympiad problems at silver medal level
#414I'm still unclear whether the system used here is actually reasoning through the process of solving the problem, or brute forcing solutions with reasoning coming in during the mathematical proof of each potential proof.
Is it clear whether the algorithm is actually learning from why previously attempted solutions failed to prove out, or is it statistically generating potential answers similar to an LLM and then trying to apply reasoning to prove out the potential solution?
Re: AI solves International Math Olympiad problems at silver medal level
#415Earlier quoted context omitted.
C'mon you're meant to be re-configuring 3,292,329 line of YML for K8s. (/s)
It's funny that if I could describe my entire career, it would probably be something similar to software janitor/maintenance worker. I guess I should have pursued a PhD when I was younger.
In another universe, this comment would be "With low pay and few academic jobs going for PhD was the worst decision of my life"
Re: AI solves International Math Olympiad problems at silver medal level
#416Earlier quoted context omitted.
Read the next sentence: "We only care about machines insofar as it serves us." Imagine a machine doing "work" that only serves itself and other machines that does no service to humanity. It would have no economic value. In fact the whole concept of "work" only makes sense if it is assigned economic value by humans.
Then we agree, but your chess example made it sound like if a machine could automatically pack meat with little human intervention, people wouldn't want it. That's also not the next sentence. How is it broadly applicable to work?
[deleted]
Re: AI solves International Math Olympiad problems at silver medal level
#417I'm curious if we'll see a world where computers could solve math problems so easily, that we'll be overwhelmed by all the results and stop caring. The role of humans might change to asking the computer interesting questions that we care about.
The next step will be having an AI come up with the problems.
Re: AI solves International Math Olympiad problems at silver medal level
#418This 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 bas…
As resident strident AI skeptic, yeah, this is real.
But MCTS was always promising when married to large NNs and DeepMind/Brain were always in front on it.
I don’t know who fucked up on Gemini and it’s concerning for Alphabet shareholders that no one’s head is on a spike. In this context “too big to fail” is probably Pichai.
But only very foolish people think that Google is lying down on this. It’s Dean and Hassabis. People should have some respect.
Re: AI solves International Math Olympiad problems at silver medal level
#419Earlier quoted context omitted.
Very few humans can after years of training. Please don't trivialize.
To mathematicians the problems are basically easy (at least after a few weeks of extra training) and after having seen all the other AI advances lately I don't think it's surprising that with huge amounts of computing resources one can 'search' for a solution.
Sorry that's wrong. I have a math phd and i trained for Olympiads in high school. These problems are not easy for me at all. Maybe for top mathematicians who used to compete.
Re: AI solves International Math Olympiad problems at silver medal level
#420Earlier quoted context omitted.
This is disingenuous. People who train are already self selected people who are talented in math. And in the people who train not everyone gets to this level. Sadly i speak from personal experience.
This school is full of people talented at math — you can't get in if you don't pass a special math exam (looking at the list, out of Serbia's 16 gold medals, I can see 14 went to students of this school, and numerous silver and bronzes too — Serbia participates as an independent country since 2006 with a population of roughly 7M, if you want to compare it with other countries on the IMO medal table). So in general, o…
[deleted]