I'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.
AI solves International Math Olympiad problems at silver medal level
251–260 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#252Earlier quoted context omitted.
> 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"?
My intuition tells me we humans are generally very bad at math. Proving a theorem, in an ideal way, mostly involves going from point A to point B in the space of all proofs, using previous results as stepping stones. This isn't particularly a "hard" problem for computers which are able to navigate search spaces for various games much more efficiently than us (chess, go...). On the other hand, navigating the real worl…
I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving them often relies on a combination of experience with rigorous mathematics and very good intuition [1] as well as many, many steps. One example is the classification of all finite simple groups [2], which took about 200 years and a lot of small steps. I guess maybe brute forcing for 200 years with the technology available today might work. But I'm sceptical and sort of hope that I won't be out of a job in 10 years. I'm certainly curious about the current development.
[1] https://terrytao.wordpress.com/career-advice/theres-more-to-...
[2] https://en.m.wikipedia.org/wiki/Classification_of_finite_sim...
Re: AI solves International Math Olympiad problems at silver medal level
#253Earlier quoted context omitted.
FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (which it sounds like they didn't).
Comparing "turn photo into LaTeX" to "translate theorems into Lean" is like comparing a child's watercolor drawing to the Mona Lisa.
I think that's exagerating a bit. If you are familiar with both Lean and LaTeX then I think transcribing these problems to Lean only takes about twice as long as transcribing them to LaTeX.
Re: AI solves International Math Olympiad problems at silver medal level
#254Machines 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.
> This principle is broadly extensible to work and art
Nah, as a consumer it makes no difference to me if a meat packing factory or Amazon warehouse employs 5000 or 5 people. To art, this principle is totally real, but for work, it only applies to some/most of it.
Re: AI solves International Math Olympiad problems at silver medal level
#255> 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…
Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.
new doesn't necessarily mean "an extremal point that's not the average of two existing points". The set of existing knowledge is not necessarily continuous; the midpoint between two known points may be unknown, and thus would be a "new" point that could be obtained by interpolation.
Re: AI solves International Math Olympiad problems at silver medal level
#256Earlier quoted context omitted.
Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.
Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.
no, search is not extrapolation. Extrapolation means taking some data and projecting out beyond the limits of that data. For example, if my bank account had $10 today and $20 tomorrow, then I can extrapolate and say it might have $30 the day after tomorrow. Interpolation means taking some data and inferring the gaps of that data. For example, if I had $10 today and $30 the day after tomorrow, I can interpolate and say I probably had $20 tomorrow.
Search is different from either of those things, it's when you have a target and a collection of other things, and are trying to find the target in that collection.
Re: AI solves International Math Olympiad problems at silver medal level
#257Earlier quoted context omitted.
(You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)
If they're talking to the people who are part of the project I'd hope the answer would contain detail and not expect to be taken as authoritative.
[flagged]
Re: AI solves International Math Olympiad problems at silver medal level
#258I'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.
I think mathematicians will still care
Re: AI solves International Math Olympiad problems at silver medal level
#259I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
Best we can do then is keep ourselves up to date and give our support!
Re: AI solves International Math Olympiad problems at silver medal level
#260Earlier quoted context omitted.
> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.
My old AI professor used to say that every problem is a search problem. The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.
I would argue that no actually searchable solution space is really infinite (if only because infinite turing machines can't exist). Finite solution spaces can get more than large enough to be intractable.