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.
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).
Sure, but I don't think theoretical guarantees are that important in practice. When I solve math problems, I don't personally use methods with such guarantees. Mathematica has certain guarantees for evaluating integrals, but that really doesn't help when it chokes for an hour on one. In practice what matters is computational complexity, and how well heuristics can help you narrow down your search space. And here IMO geometry problems have the enormous advantage that one knows there exists a short, purely synthetic solution.
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.
There is a Mathoverflow thread [0] about this. Discussion in the comments expresses skepticism because olympiad questions usually involve questions about choosing specific real roots of polynomials, not just arbitrary roots. The discussion there mostly suggests using some principles in real algebraic geometry, but these seem to be too slow and complicated to use in practice at this time.
I'm a little perplexed by the dismissiveness of your response (perhaps I'm misreading?). I'm not saying IMO problems will never be algorithmically approachable, just saying expressing these problems in terms of Grobner bases may be harder than is suggested here. Buzzard also expresses skepticism about using Grobner bases for these sorts of problems in the comments.
I wasn't trying to be dismissive, just saying that I didn't have much to add that wasn't already said there (and separately pointing out the connection between Buzzard and this thread).
What do you mean "by coordinates"? If you are asked to show that three points are on a line, having an accurate diagram is not enough, is it? Isn't the task to use the constraints presented (these lines are parallel, this is a right angle, etc) in a step-based reasoning for whatever you're asked to prove?
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 the end you calculate the coordinates of your three points and verify, symbolically, that they lie on the same line.
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".
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.
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]
> 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.
> 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"
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.
> 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.
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.
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.
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.
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)
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.
> 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.
This definitely depends on the country. There’s a reasonable amount of calculus in high school (strictly sixth form) mathematics in the U.K. The things one tends to see in university begin with (abstract) algebra and analysis with some “calculus” topics being things like vector calculus, more generic R^n->R^m calculus and contour integration.
I was thinking of mathematics more advanced than calculus, but it provides a good example. The IMO problems are designed to be done without it, but if I was programming a computer to solve IMO style inequality problems I would certainly want it to have the "Lagrange multiplier" method in its toolbox.
Depends on the textbook, of course. I've personally found that commonly-used university mathematics textbooks for standard courses to be of equal or poorer quality than high school texts.
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?
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.
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.
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 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.
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.
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.
That was an IMO problem? How long ago was this? I'm just surprised because I found the solution set + proof in like 5 minutes of writing elementary observations on a sheet of paper... (Very much unlike the IMO qualifying test I took a few years ago. Couldn't even produce a meaningful sketch of the geometry in question there...)
--- quick solution sketch ---
- every regular polygon is an obvious solution
- no three points can be collinear (can't have distinct parallel symmetry axes)
- for a given solution, look at all (3+) symmetry axes - they have to meet at the same point (easy to prove by contradiction)
- thus the angles between "neighboring" axes must be constant, namely PI / n for a solution with n distinct axes
- since any solution has to fulfill the above, for a given n > 2 we can draw all the axes (intersection point and "phase" are degrees of freedom). Add one point and mirror it on all axes - if no new axes are added (and you now have > 2 points, i.e. didn't put the initial point at the center) it's a valid solution. (You can't add another point afterwards - it would form a new axis with the first one).
- some footwork left to conclude that only "starting points" that produce regular polygons fulfill that. A proof by contradiction is pretty obvious in a sketch, but takes some effort to get even/odd n-gons covered correctly - there's probably something more elegant, but at this point you already know you've got the proof down.
While writing this out I realized that all the points must lie on a circle (apply circle chord perpendicular bisector theorem to "successive" point pairs) which should help simplify the proof.
(Please point out any mistake/misunderstanding - the solution seems way too trivial for an IMO problem. Well, a recent one at least.)
Making algebraic mistakes is always a possibility with human test-takers, but the questions are usually designed that the work isn't too bad. They could absolutely do a lot worse if they didn't try to make the math work out nicely. I'm more concerned about trying to teach computers which chain of transformations they should be looking into and how to perform them.
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.
That's a good point. If we assume each line of a publication is just applying an axiom, the complexity of such a search is clearly exponential in the length of an article. I feel like this wouldn't be better if we dropped the assumption.
