Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

IMO Grand Challenge

imo-grand-challenge.github.io

Post reply on HN
Print view View original

21–30 of 75 posts

Re: IMO Grand Challenge

#21

Post by saagarjha »

OscarCunningham wrote: post #5
th-th-throwaway wrote: post #3

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

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.

Re: IMO Grand Challenge

#22

Post by throwaway-ai-ai »

lordnacho wrote: post #18

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.

Re: IMO Grand Challenge

#23

Post by saagarjha »

lordnacho wrote: post #18

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…

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

Re: IMO Grand Challenge

#24

Post by throwaway-ai-ai »

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.

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.

Re: IMO Grand Challenge

#25

Post by typon »

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.

Re: IMO Grand Challenge

#26

Post by lordnacho »

saagarjha wrote: post #23
lordnacho wrote: post #18

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…

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

Re: IMO Grand Challenge

#27

Post by lordnacho »

throwaway-ai-ai wrote: post #24
saagarjha wrote: post #17

Earlier quoted context omitted.

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

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?

Re: IMO Grand Challenge

#28

Post by saagarjha »

lordnacho wrote: post #26
saagarjha wrote: post #23

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…

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.

Re: IMO Grand Challenge

#29

Post by eru »

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?

Well, you can do that reasoning algebraically as equations on the coordinates. So you translate the constraints into equations. See https://en.wikipedia.org/wiki/Analytic_geometry

If memory serves right, there's a certain subset of geometry that decidable in that way. Ie you can just run an algorithm.

Re: IMO Grand Challenge

#30

Post by eru »

throwaway-ai-ai wrote: post #22
lordnacho wrote: post #18

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.

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

Post reply on HN