Live data from Hacker News

IMO Grand Challenge

imo-grand-challenge.github.io

41–50 of 75 posts

Re: IMO Grand Challenge

#41
post #35

Earlier quoted context omitted.

It is done using symbolic algebra, not just assigning specific coordinates if that's what you're asking. Let's say you're given three parallel lines. You can put your x axis along the first line. Then its equation is y = 0. The other two lines necessarily have equations y = a and y = b for some reals a and b. Then you calculate the other quantities involved via a and b and other parameters you have to introduce. At t…

Yes, that's right. You end up with a system of equations and solve it. So what does "by coordinates" mean? Is the original commenter simply saying that the machine will always be able to solve that system? He's right if that is what he means. Originally it sounded like "the machine can read the diagram accurately".

>Is the original commenter simply saying that the machine will always be able to solve that system?

Yes.

Re: IMO Grand Challenge

#42

Earlier quoted context omitted.

> 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?

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 solv…

You should take a look at the IMO problems - they are generally very different from any sort of math problem you’ve ever seen before.

For instance: Determine all finite sets S of at least three points in the plane which satisfy the following condition: for any two distinct points A and B in S, the perpendicular bisector of the line segment AB is an axis of symmetry for S.

This is a deeply abstract and complex problem.

Re: IMO Grand Challenge

#43
post #25

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.

>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.

Re: IMO Grand Challenge

#44

Earlier quoted context omitted.

> 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?

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 solv…

Not sure what your “chain of transformations”, “rearranging, substituting, etc.” refer to. IMO is never about painful and tricky computations; if there’s such a problem it’s really a failure of the Problem Selection Committee. IMO is all about elegant problems in elementary mathematics that require unusual insight (which does tend toward usual when you’ve seen enough of them, but there are always surprises), spark of genius if you may. The best problems tend to be blissfully obvious in hind sight.

While you may argue that, for instance, for elementary number theory there are only so many theorems and tricks you can perform, and in fact you can compile such a list right now (which obviously won’t work for combinatorics), brute forcing your way by applying every trick to every degree of freedom of a problem will probably lead you nowhere.

Re: IMO Grand Challenge

#46

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 neede…

Suppose your assertion about this problem being easy was true. Most research papers in Math / Theoretical CS are 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.

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

Re: IMO Grand Challenge

#47

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.

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.

Re: IMO Grand Challenge

#48
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.

Re: IMO Grand Challenge

#49
post #47

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.

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 ba…

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).

Re: IMO Grand Challenge

#50
post #11

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]

> 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 though…

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.

Post reply on HN