9 ms·
At the International Mathematical Olympiad, computers prepare to go for the gold
- 1024core 6y agoI'm excited about seeing what the current learning algorithms can do in Math. Games like Chess, Go, Starcraft as "easy" (note the quotes) compared to mathematical theorem proving, and using the bag of tricks (known theorems and axioms) to solve new problems. Heck, even understanding a problem is a challenge in itself. Just look at the sample question provided: Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area. 99.9% of the people would have no idea what to do here.
- riku_iki 6y agowith AI system it is also hard, you need to have some knowledge graph which would explain what is plane, distance, etc, and map it on some set of axioms, theorems, predicates and functions.
- currymj 6y agothis is what Lean and other theorem provers are trying to build. which would be useful whether you have a human operator generating the proofs or some kind of automated system.
- est31 6y agoOne shouldn't use human concepts for "easy" vs "hard" when applied to AI capabilities. Machines aren't humans. Coal mining is hard for humans, but easy for a Bagger 288. Similarily, computers can do millions of floating point operations per second, where even a single operation would be very hard for humans, especially when larger numbers are involved. Doing the laundry, cleaning the toilet, etc. are all "simple" tasks but we don't have any humanoid robots yet that can do them. Also important to note: human capabilities are no natural constant. Once you reach human performance in some area, it's not guaranteed that you'll plateau, but instead likely that you'll outstrip human capabilities, especially in areas where there hasn't been billions of years of evolution led engineering like abstract thinking.
- ChuckNorris89 6y ago>Doing the laundry, cleaning the toilet, etc. are all "simple" tasks but we don't have any humanoid robots yet that can do them. That's because we have millions of unfortunate underpaid workers on the market with no better options that will do these chores cheaper than it costs to design, build and maintain a robot that can do such things. Hell, Atlas from Boston Dynamics can already do parkour so I'm sure they can program it to scrub toilets and do laundry but who would buy it for that when the minimum wage is what it is? The tech is nearly here, the business case isn't until the price comes orders of magnitude down.
- est31 6y agoThis is what the 3rd place winner of the World Robot Summit 2018 looks like cleaning a toilet: https://www.youtube.com/watch?v=vx3QdaPD8bw https://www.youtube.com/watch?v=vx3QdaPD8bw Your point about the workers is true, but there are economies of scale here. I don't think it's going to be different in robots than in other areas. As for the human competition, we often had cases where technology has put humans out of their job. They provide a baseline price that you need to undercut. Today we might use robots to clean nuclear waste sites. Tomorrow we use mass produce them and put them into people's homes. As long as you don't make a larger mess at the toilet than Fukushima you should be fine! :)
- Invictus0 6y agoI'm not a mathematician. Can I prove this by just providing an example? My points are (0,0), (0,sqrt(2)), (sqrt(8),0). This should give irrational side lengths of sqrt(2), sqrt(8), and sqrt(10). The area of this triangle is 2, which is rational. I solved this by guessing and checking the square roots of positive integers.
- im3w1l 6y agoThe question asks you to prove that it works for every n>=3. So you have to show it works also for n=4, n=5 etc. You are on the right track with square roots though.
- hugodutka 6y agoYou have proved it for n = 3, but you haven't for n >= 4, which the problem also requires.
- kosievdmerwe 6y agoYeah, an alternate phrasing could be "For all integers n >= 3, show that there exists a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area." For only having to find a specific n the phrasing would be something like "Find an integer n >= 3, such that ..." But in general a good heuristic is that if your solution is really simple odds are you've misunderstood the problem. IMO problems aren't easy. Even the "easy" ones take a bit of work.
- otoburb 6y agoDaniel would agree with you that this is an underappreciated and overlooked area of AI research. A 2018 blog post[1] gave an indication that he'd started to turn his attention to this particular area (mathematics) more forcefully. [1] https://dselsam.github.io/posts/2018-06-24-mathematics-our-overlooked-ability.html https://dselsam.github.io/posts/2018-06-24-mathematics-our-o...
- karmakaze 6y agoThe difference between being better than humans at simple games and harder games like Go is scale. We thought this wouldn't happen for generations but here we are. I don't see the how the sorts of problems presented as being qualitatively different as ones we can already solve. The problem is scale and having the problem formally defined. We'll separate the english-to-machine readable form as a separate step as I don't think that's the 'math' part of the challenge--specifically excluding math word problems. We will develop better representations and search strategies and meta-strategy searching abilities and make advances in improving their runtimes as hardware devices continue to get faster allowing research to accelerate. For the example question, a machine could have picked a special case, right triangles where a^2 + b^2 = c^2 and the area a*b/2. Now choose a^2, b^2 as whole numbers, say 2 and 3 ==> c = root(5) with area 3. As noted in other comments, it would then have to take this premise and algebraically extend to all n>3 which I believe we have inductive provers as one example can do.
- deleted 6y ago[deleted]
- remexre 6y agoHuh, was somewhat surprised to see that this uses Lean instead of something purely ML-ful, though I suppose GPT-{2,3} can't be "trusted" to output correct mathematics without something much more rigid to validate it.
- janekm 6y agoA seemingly obvious approach would be to try to get GPT-X to generate candidate proofs and then get a tool like Lean to validate them. Which presumably doesn't work or else I suppose the article would have been about that...
- iandanforth 6y agoFor reference here's a GPT-3 output for the sample question: Solution: Suppose the given set of n points is A = (a 1 , a 2 , …, a n ). Between any two points we will draw a line segment connecting them, and let the distance from a 1 to the line segment be d(a 1 ,a 2 ) and d(a 1 ,a 3 ) be the distance from a 1 to the line segment connecting a 2 and a 3. Since any two of the points determine a line segment connecting them, there are n–2 segments connecting the n–1 points. Let L be the common perpendicular bisector of two of these segments. So, d(a 1 ,a 2 ) = d(a 1 , L) and d(a 1 ,a 3 ) = d(a 1 , L). Now, we consider the triangle formed by the points (a 1 , a 2 ) and (a 1 , a 3 ). If we are given the points a 1 , a 2 and a 3 , we can easily find the sides of the triangle. Since d(a 1 ,a 2 ) + d(a 1 ,a 3 ) = d(a 1 , L) + d(a 1 , L) = 2d(a 1 , L), the triangle formed is right angled and therefore non-degenerate. We can easily calculate the rational area of such a triangle and the side lengths. Let us consider the simplest case when n = 3. We have three points (a 1 , a 2 , a 3 ) such that each of a 1 , a 2 and a 3 are different. Therefore, we can form a triangle by connecting a 1 , a 2
- pmiller2 6y agoThis is great. It looks like the confused ramblings of a student who has no clue.
- 6y ago
- dzdt 6y agoThe actual article title is "At the Math Olympiad, Computers Prepare to Go for the Gold" which also has the advantage of fitting the HN length requirement without a dangling "To".
- deleted 6y ago[deleted]
- jstanley 6y agoWell I for one sincerely hope it succeeds in
- JamesCoyne 6y agoSure, but it is concerning that
- im3w1l 6y ago> IMO problems are simple, but only in the sense that they don’t require any advanced math — even calculus is considered beyond the scope of the competition. I kind of disagree. IMO problems require a lot of studying and theory that an average person wont know.
- gowld 6y agoThey are elementary. They don't require advanced theory, but they require an extremely large breadth of mathematical knowledge or creative.
- SketchySeaBeast 6y ago"and each set of three points determines a non-degenerate triangle with rational area" <- that's not language I knew in elementary school. Just being able to read what the question wants is a skill that isn't available to most elementary students.
- saagarjha 6y ago"Elementary" in the sense of "introductory", not in the sense of "taught in elementary school".
- SketchySeaBeast 6y agoI understand that, but elementary quantum physics is still grossly past the level of the students and required more advanced theory just to get to that elementary level understanding of the subject.
- saagarjha 6y agoRight, but this is elementary mathematics that is specifically chosen so that university-level mathematics is not required. (And rarely helps.)
- 6y ago
- deleted 6y ago[deleted]
- deleted 6y ago[deleted]
- iop 6y agoAren't some IMO problems pretty easy if you can throw a computer algorithm at it? (for example geometry problems can be coordinate bashed?) Also I can't find an accompanying dataset from the link: https://imo-grand-challenge.github.io/ https://imo-grand-challenge.github.io/ EDIT: Nvm found it: https://github.com/IMO-grand-challenge/formal-encoding/blob/master/lean/problems/algebra/imo_2018_sl.lean https://github.com/IMO-grand-challenge/formal-encoding/blob/.... But there are only a handful of formal encodings of problems and last commit was from a year ago!
- dselsam 6y agoThat repository has rotted. Preliminary roadmap described in recent invited talk at AITP-2020 http://grid01.ciirc.cvut.cz/~mptp/zoomaitp/aitp_sep_15_1930.mp4 http://grid01.ciirc.cvut.cz/~mptp/zoomaitp/aitp_sep_15_1930....
- TheRealPomax 6y agoPrepares To... what? Can someone fix the title? =/
- mike00632 6y agoThis would surely be more impressive than playing starcraft. But I don't see how this is possible without AGI.
- gowld 6y agoIt needs a math dictionary and grammer primer, and a lot of math knowledge.
- bigpumpkin 6y agoCan AI even verify proofs now? Say it's presented with a solution, can it check for the internal consistency.
- pmiller2 6y agoDepending on what you call "AI" and "proofs," the answer is that you might be describing what's called a "proof assistant."
- YetAnotherNick 6y agoThat's why formal logic was invented(started by Aristotle!). There are computerized rules for checking that the formula is valid given proof.
- stephc_int13 6y agoAll those competions/olympiads are nothing more than glorified rat races. As such, they are somewhat low-hanging fruits for the AI field, but I wouldn't say that I'd found that impressive or game changing in any way.
- saagarjha 6y agoAn AI that can do well on the IMO can likely also be useful when applied to actual problems in mathematics. Also, calling the "IMO" an "glorified rat race" is fairly demeaning to those that compete in it.
- 317070 6y agoI have no doubt that we are not far away from winning an IMO gold medal with an AI algorithm. I am not so sure it will come from the lean-team though. There are more people working in the direction, with varying focus on the AI or the automated prover aspect of things. I have the suspicion that AI-mathematicians will be foremost AI, and only secondary theorem provers. This is because what is mentioned in the article, mathematicians first look for patterns in these questions, and then apply their toolset to them. Only the final step is what theorem provers are currently good in. But, only time will tell which team will make it first to the finish line.
- Someone 6y agoFTA: “For example, one of the oldest results in math is Euclid’s proof from 300 BCE that there are infinitely many prime numbers. It begins with the recognition that you can always find a new prime by multiplying all known primes and adding 1” So, if all the primes you know are 5 and 7, you can find a new one by computing 5×7+1? ;-) This is a very common error. The claim doesn’t even hold if you know the first n primes. The first counterexample is 2×3×5×7×11×13+1=59×509. All you can tell is that the result has at least one prime factor that’s not yet in your list.
- teraflop 6y agoIt's true that's a common error, but if we're going to be really pedantic: the article doesn't say that multiplying all known primes and adding 1 results in a prime number, it says it's a way to find a new prime. (In fact, all of the result's prime factors are primes that weren't in the list you started with.)
- Someone 6y agoBy that logic, picking random integers is a way to find new primes. But yes, the all part is a good way of being pedantic.
- saagarjha 6y agoPicking a random number isn't guaranteed to help you find a prime number. However, doing the "take all the prime numbers and multiply them and add 1" always produces at least one prime number; either the result or the factors of the number.
- arachnids 6y agoHere's a slightly more rigorous version of the proof for anyone interested: 1. Suppose the list of primes is finite, and that they are P_1, P_2, P_3 .., P_n 2. Consider the new number P_1 * P_2 * P_3 * .. * P_n + 1. None of the P_is divide this number. Therefore, by definition, it it is a prime. 3. The number we found in (2) is not any of the P_is, and it is a prime. This contradicts the assumption we made in (1). So, the assumption in (1) is wrong, there must be infinitely many primes The examples in parent's post do not work because they do not follow the framework of this proof. I see parent's point that the claim in the article isn't technically correct, but I think it's reasonable to allow some handwaving in an accessible article written in English :-)
- dselsam 6y agoOne of the founders of the IMO Grand Challenge here. FYI I presented the challenge along with a preliminary roadmap at AITP 2020 last week: https://youtu.be/GtAo8wqWHHg https://youtu.be/GtAo8wqWHHg. No way to know if gold is five years out or five hundred but I hope the challenge spurs progress in the field either way.