IMO Grand Challenge

https://imo-grand-challenge.github.io

by panic • 7 years ago

128 73 7 years ago

imo-grand-challenge.github.io

nebulous1• 7 years ago

Speaking of the IMO, I saw this video recently and thought it was pretty interesting: https://www.youtube.com/watch?v=M64HUIJFTZM

th-th-throwaway2• 7 years ago

There was a good link about why AI algorithms tend to approach human level performance rapidly for some tasks: https://www.coursera.org/lecture/machine-learning-projects/w...

The answer turns out to be pretty boring: As long as humans are still better than machine, humans can provide algorithmic insights and be a source of cheap labels.

So I am pretty pessimistic about this particular task. There are only a small handful of humans in the world who are qualified to help! (according to IMO scores: https://www.imo-official.org/hall.aspx)

OscarCunningham9• 7 years ago

The pool of people who can solve IMO problems is much larger than the pool of people who can solve IMO problems at the rate of one every 90 minutes.

Also consider that fact that human IMO contestants have little training in university-level mathematics. The problem setters try to choose problems where knowledge of advanced mathematics doesn't help, in order to produce a level playing field which only measures raw problem-solving ability. But I suspect that postgraduate-level mathematics will nevertheless be useful in programming the AI.

saagarjha10• 7 years ago

Also consider that fact that human IMO contestants have little training in university-level mathematics.

I don't think this is true, as in my experience many of the contestants have already cultured a background in calculus but refrain from using it as the problems are usually designed to actively discourage its use.

ngcc_hk• 7 years ago

Yes some are but not all.

There are self learning one and there are one which human to id only.

OscarCunningham9• 7 years ago

A lot of IMO geometry problems are easy for computers because they can simply use coordinates to convert the problem to algebra (this approach is computation heavy which is why humans don't use it even though it's guaranteed to work given enough time). So in a good year the computer might get two out of the six problems without having to do anything clever.

saagarjha10• 7 years ago

IMO problems are generally proof-based and don't always lend themselves well to brute force solutions using analytic geometry.

throwaway-ai-ai5• 7 years ago

Many IMO geometry problems involves proving things like:

these three points are on one line

these three lines intersect at one point

these two lines are parallel

these four points are on a circle

these two angles are equal

etc ...

There are things that absolutely can be done via coordinates, if one can brute force large algebraic expressions.

OscarCunningham9• 7 years ago

The kind of problems I'm thinking of are those like 2 and 6 on this year's IMO.

You have a bunch of points, lines and circles in some configuration and you have to prove that some condition holds. So you assign symbols to represent the coordinates of each of these points and you represent each fact you are told about them by some equation. The condition you are trying to prove is also represented by some equation. After multiplying up to get rid of square roots each of these equations is setting a polynomial equal to 0. So you are just trying to prove that some polynomial must be 0 if a bunch of other polynomials are 0, which can be done algorithmically via Gröbner bases.

knzhou2• 7 years ago

I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and purely synthetic/geometric solutions as "insightful". But there's no reason that a computer would find the second way more difficult. After all, synthetic geometry is just another system of rules, like ordinary algebra.

Us humans might fall back on coordinate bashing, but that's just because we have a lot of practice with the rules of algebra. To a computer, one rule set is as good as any other. What we call geometric insight boils down to pattern matching configurations to previously seen ones, combined with search in the space of possible moves, both of which computers can do.

OscarCunningham9• 7 years ago

The current situation doesn't reflect that though. We have a algorithm (Gröbner bases) for doing coordinate bashes which is guaranteed to succeed, whereas as far as I know we don't have an analogous algorithm in terms of synthetic geometry (other than the direct translation of coordinate bashing).

prvc• 7 years ago

I see no reason why the difference between "textbook" and "contest" problems would be anywhere near as significant to computers as it is to humans.

OscarCunningham9• 7 years ago

One interesting thing about IMO problems is that they don't require any advanced mathematical knowledge, only problem-solving ability.

saagarjha10• 7 years ago

Depends on the textbook, but most ones used in schools are quite formulaic while IMO problems generally require significant insight to solve.

eru6• 7 years ago

School math textbooks are quite formulaic.

University math textbooks less so.

benkarst• 7 years ago

Thought this was a link to great reddit and youtube comments.

throwaway-ai-ai5• 7 years ago

I'm curious: what are people's predictions for when it will be possible to run some program XYZ on a $10/hr EC2 machine and have it beat humans on the IOI/ICPC ?

Furthermore, suppose such an open source program existed, how long would it take for it to start replacing remote contractors and then in-office programmers? ["start replacing" as in, say, 10% of human programmers]

ai_ia• 7 years ago

What are people's predictions for when it will be possible to run some program XYZ on a $10/hr EC2 machine and have it beat humans on the IOI/ICPC ?

A chess program can be trained on a EC2 instance that can possibly beat most grandmasters. My best guess, people will get over it and move on to more difficult challenges. The field of AI has a notorious record of shifting goalposts whenever something previously thought unattainable is achieved.

how long would it take for it to start replacing remote contractors and then in-office programmers?

Although I don't think it's possible to replace "programmers", if such scenario does evolve, we would have come up with newer jobs that didn't existed before. Podcasting, Youtuber, UX Designers didn't exist 20 years back. Hard to guess what will come forth.

NieDzejkob2• 7 years ago

I'm not sure if you're trying to imply the shifting of goalposts is bad, but it sure does sound like it.

I would argue that all of research is like that - once something is achieved, people will want to do better things.

After all, it's not an argument.

eternalny1• 7 years ago

Furthermore, suppose such an open source program existed, how long would it take for it to start replacing remote contractors and then in-office programmers?

Until AI can create an Angular application with a .Net Core Azure back-end that meets ever-changing customer requirements ("can we remove the need for Bootstrap 4? Can we make the integration with Active Directory seamless?") on short notice, not very soon at all!

I'm throwing that out there because that's just one of my current projects, but a lot of programmers do things daily that AI simply isn't intended for.

Or college courses, for that matter. Although since you mentioned 10% you probably mean more in the area of research science, which may be a different story.

throwaway-ai-ai5• 7 years ago

Until AI can create an Angular application with a .Net Core Azure back-end that meets ever-changing customer requirements ("can we remove the need for Bootstrap 4? Can we make the integration with Active Directory seamless?") on short notice, not very soon at all!

I think you are arguing for "Not all programming tasks that can be automated away by a bot that can win IOI / ICPC."

However, what I'm asking is: "Does there exist 10% of programming that can be automated away by a bot that can win IOI / ICPC" ?

Furthermore, I think you are also assuming that human programmers remain static, while the AI has to be a 'drop in replacement for humans.' On the other hand, if we look at AWS -- AWS didn't build some AI that is a drop in replacement for sys admin work. AWS built their own API, humans adapted to it.

It seems to me that in a world where such an IOI/ICPC winning bot existed, programmers would adapt to it (just as programmers have adapted to AWS), by figuring out "how can I leverage this API so that I don't have to hire someone to do FOOBAR"

saagarjha10• 7 years ago

I was nowhere near anywhere good enough to participate in an IMO officially, but judging by the types of problems they ask I'm not super optimistic. This might come back to bite me, but I'd predict that EC2 won't be around when this is solved.

throwaway-ai-ai5• 7 years ago

I would guess that a computer beats humans on the IMO before a computer beats humans on the IOI/ICPC -- but also think that the latter would have far greater impact.

eru6• 7 years ago

Well, we are constantly replacing programmers by computers.

Think of eg compilers and interpreters. Thanks to them, perhaps you need only one guy to write software to solve a problem that used to take 10 people: 9 people replaced.

deepnotderp• 7 years ago

Program synthesis of large programs is an incredibly difficult problem. I could definitely be wrong but I don't think it's solvable with current AI techniques.

lordnacho4• 7 years ago

Why would this be hard for the machines? A lot of math contest problems are about trying some rearrangements or substitutions, using a few principles to guide you towards the solution.

If you give the machine some equations, wouldn't it find a path to the solution pretty fast? Aren't there solvers that aren't considered AI that do that sort of thing?

I did some math contests in school, and a lot of the problems needed some brute force element along with a bit of overview so you didn't waste too much time. Often there'd be a problem that you'd look at and think "hmm this will solve via integration by parts" but the thing was complex enough that you'd potentially screw something up.

I looked in the Gitlab, it seems the problems are already encoded in Lean. Haven't you solved a major part of the problem already if you can formally encode it like that? Half the fun of math contests is getting over the WTF feeling.

throwaway-ai-ai5• 7 years ago

Suppose your assertion about this problem being easy was true.

Most research papers in Math / Theoretical CS are < 50 pages, while many IMO problems have solutions > 1 page. So it's only a factor of 50 "more complex."

Then, we should be able to encode open problems / conjectures in Math / Theoretical CS into Lean, run this brute fore approach, and have it start auto generating new publications.

To the best of my knowledge, no one has done this yet.

eru6• 7 years ago

Well, the IMO problems are constructed with a solution in mind.

Also, who says that efforts goes up linearly with size?

(Not necessarily agreeing with lordnacho here, just saying that your argument ain't a good one.)

oefrha3• 7 years ago

Complexity is a terrible measure of mathematical value. Length of exposition is even worse.

saagarjha10• 7 years ago

hmm this will solve via integration by parts

The AMC/AIME/USAMO/IMO set of exams can all be solved without calculus and are not what I'd call "brute force". Perhaps you have experience with a different type of mathematical competition?

lordnacho4• 7 years ago

Perhaps brute force is the wrong term, but at least they would require a chain of transformations that a human could easily mess up. Rearranging, substituting, etc. A machine wouldn't get that wrong ever, whereas a human would have wasted a fair bit of time.

Well I did miss the IMO team narrowly, but I didn't think those questions were all that different in nature. Quirky questions you'd never see in school, but solvable with school tools. And I'm pretty sure that while you didn't NEED calc and higher subjects, having studied them would give you some edge.

typon• 7 years ago

This seems impossible for current ML architectures, but I want to be proven wrong. If the AI can't query the internet, does it have a limit of the model size and the computation capability? I feel like letting an AI use megawatts of power isn't quite fair.

ivanbakel• 7 years ago

I feel like letting an AI use megawatts of power isn't quite fair.

Based on what? An AI which could reliably produce proofs for these problems would be at the cutting edge of research. Putting additional constraints on it for "fairness" just increases the likelihood of failure. It's not as if there's already some competition to measure up against.

hyperbovine• 7 years ago

Is Reid Barton back to doing academic mathematics?

lacker3• 7 years ago

Yea he just got an academic job

oefrha3• 7 years ago

An obvious extension / sister project: Putnam Grand Challenge.

carapace• 7 years ago

The "Reproducibility" proposed rule is very exciting IMO.

The AI must be open-source, released publicly before the first day of the IMO, and be easily reproduceable. (sic) The AI cannot query the Internet.

throwawaymath• 7 years ago

I thought Reid Barton was at RenTech? He's back in academia?

lacker3• 7 years ago

AFAIK he just got an academic job

pirocks• 7 years ago

I'm curious as to whether LEAN is the right choice for this. LEAN is rather hard to parse, and complex, as a consequence of being designed for use by humans. Perhaps specifying the problem(s) in a small superset of first order logic would be better?

andrepd• 7 years ago

The people promoting this are the Lean developers... :p

lacker3• 7 years ago

I don’t think you can express IMO problems in a simple subset of first-order logic.

mkagenius• 7 years ago

Not sure if reading the problem text and understanding what it is asking is part of the problem or not. If it is, well, good luck collecting data for it.

monktastic1• 7 years ago

This is explained in paragraph two of the post. No, that is not part of the problem.

buyingarmor• 7 years ago

10 minutes (which is approximately the amount of time it takes a human judge to judge a human’s solution)

Hah, some student solutions take hours to read...

robocat• 7 years ago

but there are no other limits on the computational resources it may use during that time

I am guessing that defining a CO₂ or $ limit causes problems.

They could specify that the solution must be CO₂ neutral e.g. suggest an official CO₂ offset provider?

IMO Grand Challenge

Related Stories