7 ms·
IMO Grand Challenge
- nebulous1 7y agoSpeaking of the IMO, I saw this video recently and thought it was pretty interesting: https://www.youtube.com/watch?v=M64HUIJFTZM https://www.youtube.com/watch?v=M64HUIJFTZM
- th-th-throwaway 7y agoThere 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/why-human-level-performance-FWkpo 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 https://www.imo-official.org/hall.aspx)
- OscarCunningham 7y agoThe 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.
- saagarjha 7y 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.
- eru 7y agoI 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-problems/ https://terrytao.wordpress.com/books/solving-mathematical-pr...
- saagarjha 7y ago> I guess it depends on what you mean by university level mathematics. Calculus.
- dan-robertson 7y agoThis 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.
- eru 7y agoIn Germany we had plenty of calculus in the Abitur (like A-levels), too. Uni adds a much more axiomatic and formal approach.
- OscarCunningham 7y agoI 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.
- ngcc_hk 7y agoYes some are but not all. There are self learning one and there are one which human to id only.
- OscarCunningham 7y agoA 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.
- saagarjha 7y agoIMO problems are generally proof-based and don't always lend themselves well to brute force solutions using analytic geometry.
- throwaway-ai-ai 7y agoMany 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.
- lordnacho 7y agoWhat 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?
- eru 7y agoWell, 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 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.
- prvc 7y agoI see no reason why the difference between "textbook" and "contest" problems would be anywhere near as significant to computers as it is to humans.
- OscarCunningham 7y agoOne interesting thing about IMO problems is that they don't require any advanced mathematical knowledge, only problem-solving ability.
- saagarjha 7y agoDepends on the textbook, but most ones used in schools are quite formulaic while IMO problems generally require significant insight to solve.
- benkarst 7y agoThought this was a link to great reddit and youtube comments.
- throwaway-ai-ai 7y agoI'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 7y 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.
- NieDzejkob 7y agoI'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 7y 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.
- lordnacho 7y agoWhy 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-ai 7y agoSuppose 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.
- eru 7y agoWell, 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.)
- NieDzejkob 7y agoThat'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.
- 7y ago
- typon 7y agoThis 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 7y 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 7y agoIs Reid Barton back to doing academic mathematics?
- lacker 7y agoYea he just got an academic job
- oefrha 7y agoAn obvious extension / sister project: Putnam Grand Challenge.
- carapace 7y agoThe "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 7y agoI thought Reid Barton was at RenTech? He's back in academia?
- lacker 7y agoAFAIK he just got an academic job
- pirocks 7y agoI'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?
- mkagenius 7y agoNot 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 7y agoThis is explained in paragraph two of the post. No, that is not part of the problem.
- buyingarmor 7y 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 7y 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?