IMO Grand Challenge • Hacker News Board

Re: IMO Grand Challenge

#31

Post by eru » Sat, Oct 26, 2019, 1:22 PM UTC

throwaway-ai-ai wrote: post #10

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]

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.

Re: IMO Grand Challenge

#32

Post by eru » Sat, Oct 26, 2019, 1:25 PM UTC

saagarjha wrote: post #21

OscarCunningham wrote: post #5

Earlier quoted context omitted.

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

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

I guess it depends on what you mean by university level mathematics.

Terrence Tao definitely says that doing university math changed his approach to these problems. See https://terrytao.wordpress.com/books/solving-mathematical-pr...

Re: IMO Grand Challenge

#33

Post by eru » Sat, Oct 26, 2019, 1:26 PM UTC

saagarjha wrote: post #15

prvc wrote: post #6

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.

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

School math textbooks are quite formulaic.

University math textbooks less so.

Re: IMO Grand Challenge

#34

Post by hyperbovine » Sat, Oct 26, 2019, 1:27 PM UTC

Is Reid Barton back to doing academic mathematics?

Re: IMO Grand Challenge

#35

Post by owaty » Sat, Oct 26, 2019, 1:29 PM UTC

lordnacho wrote: post #27

throwaway-ai-ai wrote: post #24

Earlier quoted context omitted.

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.

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.

Re: IMO Grand Challenge

#36

Post by saagarjha » Sat, Oct 26, 2019, 1:29 PM UTC

eru wrote: post #32

saagarjha wrote: post #21

Earlier quoted context omitted.

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

I guess it depends on what you mean by university level mathematics. Terrence Tao definitely says that doing university math changed his approach to these problems. See https://terrytao.wordpress.com/books/solving-mathematical-pr...

> I guess it depends on what you mean by university level mathematics.

Calculus.

Re: IMO Grand Challenge

#37

Post by saagarjha » Sat, Oct 26, 2019, 1:30 PM UTC

eru wrote: post #33

saagarjha wrote: post #15

Earlier quoted context omitted.

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

School math textbooks are quite formulaic. University math textbooks less so.

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.

Re: IMO Grand Challenge

#38

Post by OscarCunningham » Sat, Oct 26, 2019, 1:43 PM UTC

saagarjha wrote: post #21

OscarCunningham wrote: post #5

Earlier quoted context omitted.

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

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

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.

Re: IMO Grand Challenge

#39

Post by lordnacho » Sat, Oct 26, 2019, 1:49 PM UTC

owaty wrote: post #35

lordnacho wrote: post #27

Earlier quoted context omitted.

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

Re: IMO Grand Challenge

#40

Post by OscarCunningham » Sat, Oct 26, 2019, 1:56 PM UTC

saagarjha wrote: post #17

OscarCunningham wrote: post #4

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.

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

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.