At the International Mathematical Olympiad, computers prepare to go for the gold(quantamagazine.org)
quantamagazine.org
At the International Mathematical Olympiad, computers prepare to go for the gold
https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/
68 comments
One 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. 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.
FTA: “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.
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.
It'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.)
By that logic, picking random integers is a way to find new primes.
But yes, the all part is a good way of being pedantic.
But yes, the all part is a good way of being pedantic.
Picking 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.
Here'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 :-)
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 :-)
I seem to be associated with that quote (and of course I didn't say it -- indeed when I spoke to Quanta I used factorials plus one). When the article appeared I emailed Kevin Hartnett immediately to suggest replacing that line with something like "...using 1 plus the product of all known primes" but he seemed to be happy with what he'd written -- his argument was that what he wrote was ambiguous but not definitely wrong.
I 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.
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.
All 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.
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.
An 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.
I'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.
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.
One 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.
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.
>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.
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.
This is what the 3rd place winner of the World Robot Summit 2018 looks like cleaning a toilet: 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! :)
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! :)
The 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.
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]
Daniel 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-o...
[1] https://dselsam.github.io/posts/2018-06-24-mathematics-our-o...
I'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.
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.
The 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.
You have proved it for n = 3, but you haven't for n >= 4, which the problem also requires.
Yeah, 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.
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.
with 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.
this 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.
Huh, 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.
A 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...
For 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
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
This is great. It looks like the confused ramblings of a student who has no clue.
Always fun to grade these kinds of proofs with a bottle of wine at 2am.
I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
One of my math professors had a "BS" stamp for things like this. If it were worth X points, you'd lose X-5 when it was so obviously a rambling mess. He'd rather you just say "I don't know" than waste both your time and his. Perhaps that's just an advantage of tenure, though.
OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.com/spolu/status/1303693595833237504
I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.
I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.
The 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]
Well I for one sincerely hope it succeeds in
Sure, but it is concerning that
> 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.
I kind of disagree. IMO problems require a lot of studying and theory that an average person wont know.
Yeah, they do often require a lot of math. It's just a restricted set of topics. The IMO doesn't do any calculus or anything beyond calculus like real analysis, topology, etc. It does have a lot of geometry problems that use geometry that typically isn't in the American curriculum, and it has topics like number theory that aren't really in a standard high school curriculum either. But the topics are restricted so that they are pretty close to understandable by someone who has just done well in a standard high school mathematics curriculum.
Here's an example. For the problem they include in the article:
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.
This is a whole lot easier if you're familiar with Pick's Theorem, which gives you a formula for the area of a polygon whose corners are integer lattice points. In particular, any three integer lattice points define a triangle with rational area. So all you have to do is find n points that aren't colinear with each other and have irrational distance, and you'll solve the problem.
Technically, you could do this without Pick's Theorem, because you'll be able to find an equivalent formula for the area of these triangles. But it's much easier if you do know Pick's Theorem, and that's the sort of thing that you typically don't pick up in standard high school math, but you would pick up if you were practicing a bunch of different Olympiad-type problems.
Here's an example. For the problem they include in the article:
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.
This is a whole lot easier if you're familiar with Pick's Theorem, which gives you a formula for the area of a polygon whose corners are integer lattice points. In particular, any three integer lattice points define a triangle with rational area. So all you have to do is find n points that aren't colinear with each other and have irrational distance, and you'll solve the problem.
Technically, you could do this without Pick's Theorem, because you'll be able to find an equivalent formula for the area of these triangles. But it's much easier if you do know Pick's Theorem, and that's the sort of thing that you typically don't pick up in standard high school math, but you would pick up if you were practicing a bunch of different Olympiad-type problems.
Ha, Pick's theorem. Such hopelessly advanced problems (I'll give an example shortly) are well beyond what a cluster of ten thousand GPU's can solve today if trained for a thousand days on the types of math you've mentioned and then given a hundred hours to compute the answer to an infinitely, staggeringly and mind-bendingly intricate problem such as this one:
"Starting at 2, how many times must you double the number for the result to exceed 10?".
(Or a similarly trivial one.) Yeah. Really. Try it. They don't understand language at all. Just try to interact with any of the assistant or computational knowledge engines.
Here's what wolfram alpha gives you for that query:
Query:
Starting at 2, how many times must you double the number for the result to exceed 10?
Computed response:
1 | adjective | (especially of eyes) bulging or protruding as with fear 2 | adjective | appropriate to the beginning or start of an event 3 | noun | a turn to be a starter (in a game at the beginning)
"Starting at 2, how many times must you double the number for the result to exceed 10?".
(Or a similarly trivial one.) Yeah. Really. Try it. They don't understand language at all. Just try to interact with any of the assistant or computational knowledge engines.
Here's what wolfram alpha gives you for that query:
Query:
Starting at 2, how many times must you double the number for the result to exceed 10?
Computed response:
1 | adjective | (especially of eyes) bulging or protruding as with fear 2 | adjective | appropriate to the beginning or start of an event 3 | noun | a turn to be a starter (in a game at the beginning)
https://imo-grand-challenge.github.io/
For the challenge, they give the AI a formal representation of the problem in Lean. To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol.
For the challenge, they give the AI a formal representation of the problem in Lean. To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol.
thanks. that's really not the IMO though, is it? coming up with a formal representation is a large part of the challenge, isn't it?
∀n∈Z: n>=3 => ∃S∈(R^2)^n: [~∃p1∈S ∃p2∈S ∃p3∈S ∃a∈R: p1!=p2 & p2 != p3 & p3 != p1 & p1 + a(p2-p1) = p3] & [~∃p1∈S ∃p2∈S ∃a∈Z ∃b∈Z: |p1-p2| = a/b] & [∀p1∈S ∀p2∈S ∀p3∈S ∃a∈Z ∃b∈Z p1!=p2 & p2 != p3 & p3 != p1 => Area(p1, p2, p3) = a / b]
So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product.
∗Although I may have made some or many mistakes.
So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product.
∗Although I may have made some or many mistakes.
IMO problems are designed such that an average (ok, maybe slightly-above average) person can follow the solution, but it takes skill to come up with it in the first place. Just like calculus is standard curriculum for hundreds of thousands of high school students around the world, but we still think Isaac Newton and Gottfried Leibniz were genii for coming up with it.
They are elementary. They don't require advanced theory, but they require an extremely large breadth of mathematical knowledge or creative.
"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.
"Elementary" in the sense of "introductory", not in the sense of "taught in elementary school".
I 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.
Right, but this is elementary mathematics that is specifically chosen so that university-level mathematics is not required. (And rarely helps.)
Well, maybe not elementary school, but in highschool you should encounter those, especially second part. Non-degenerate in that case is fancy word for saying that those point cannot form a line (or a single point) - just that triangle is actually a triangle.
This is pretty common term when it comes to math Olympiad so in would be extremely unlikely that someone can get to imo without encountering that in the past during training
"'Elementary' means that very little is required to know ahead of time in order to understand it, except to have an infinite amount of intelligence."
In practice, yeah, "an average person" wouldn't know where to begin. And a brilliant high schooler who hasn't studied maths beyond the high-school curriculum won't ace the test. Though he could get a medal, particularly if the geometry and combinatorics questions are friendly.
But the conceit of the IMO has always been that the problems are drawn from a very limited selection of fields, which are/were commonly taught in high schools around the world. No need for complex numbers, calculus, abstract algebra, or trigonometry (though any of these may end up used in an alternative solution).
But the conceit of the IMO has always been that the problems are drawn from a very limited selection of fields, which are/were commonly taught in high schools around the world. No need for complex numbers, calculus, abstract algebra, or trigonometry (though any of these may end up used in an alternative solution).
Can't say I've seen inequality-problems like IMO has anywhere else.
But a surprising number of them can be solved with the insight only that x^2 >= 0. (Both Cauchy-Schwartz and AM/GM reduce to that if you squint hard enough). And that's accessible to any maths student.
They show up in a few other areas, like probabilistic analysis of algorithms or sketching (e.g. Chernoff bounds and definitely the Cauchy-Schwartz ineq.). But you're right, nothing heavyweight like Muirheads has many applications.
[deleted]
[deleted]
Aren'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/
EDIT: Nvm found it: 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!
Also I can't find an accompanying dataset from the link: https://imo-grand-challenge.github.io/
EDIT: Nvm found it: 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!
That repository has rotted. Preliminary roadmap described in recent invited talk at AITP-2020 http://grid01.ciirc.cvut.cz/~mptp/zoomaitp/aitp_sep_15_1930....
Prepares To... what? Can someone fix the title? =/
Can AI even verify proofs now? Say it's presented with a solution, can it check for the internal consistency.
Depending on what you call "AI" and "proofs," the answer is that you might be describing what's called a "proof assistant."
That's why formal logic was invented(started by Aristotle!). There are computerized rules for checking that the formula is valid given proof.