The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.
AlphaGeometry: An Olympiad-level AI system for geometry
41–50 of 177 posts
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#42I'm very curious how often the LM produces a helpful construction. Surely it must be doing better than random chance, but is it throwing out thousands of constructions before it finds a good one, or is it able to generate useful proposals at a rate similar to human experts? They say in the paper, "Because the language model decoding process returns k different sequences describing k alternative auxiliary construction…
thanks TIL what Beam search is https://en.wikipedia.org/wiki/Beam_search
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#43It was interesting. One of the reviewers noted that one of the generated proofs didn’t seem that elegant in his opinion.
Given enough compute, I wonder how much this would be improved by having it find as many solutions as possible within the allotted time and proposing the simplest one.
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#44Earlier quoted context omitted.
No, that sort of thing has been said about math competitions for a long time. It's not a new argument put forward as something against AI. An analogy with software is that math competitions are like (very hard) leetcode. There was an article posted on HN recently that is related: https://benexdict.io/p/math-team
What is the argument; that math competitions are easy for computers but hard for humans?
The usual argument is:
We test developer skill by giving them leetcode problems, but leetcode while requiring programming skill is nothing like a real programmer's job.
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#45Euclidean geometry is decidable. Does that make it easier for computers, compared to other IMO problems?
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#46It was interesting. One of the reviewers noted that one of the generated proofs didn’t seem that elegant in his opinion. Given enough compute, I wonder how much this would be improved by having it find as many solutions as possible within the allotted time and proposing the simplest one.
Elegance would require more than this. Reasoning, for one.
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#47What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#48I'm very curious how often the LM produces a helpful construction. Surely it must be doing better than random chance, but is it throwing out thousands of constructions before it finds a good one, or is it able to generate useful proposals at a rate similar to human experts? They say in the paper, "Because the language model decoding process returns k different sequences describing k alternative auxiliary construction…
IMHO: this bumps, hard, against limitations of language / human-machine analogies.
But let's try -- TL;DR 262,144, but don't take it literally:
- The output of a decoding function is a token. ~3/4 of a word. Let's just say 1 word.
- Tokens considered per token output = 262,144 Total number of token considerations for 1 output token = beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144.
- Let's take their sample solution and get a word count. https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
- Total tokens for solution = 2289
- Total # of tokens considered = 600,047,616 = 262,144 * 2289
- Hack: ""number of solutions considered"" = total tokens considered / total tokens in solution
- 262,144 (same # as number of tokens we viewed at each iteration step, which makes sense)
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#49What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?
I never studied math to become the best in the world !
Re: AlphaGeometry: An Olympiad-level AI system for geometry
#50If I read their paper right, this is legit work (much more legit than DeepMind's AI math paper last month falsely advertised as solving an open math research problem) but it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence.
A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the elementary geometry context has both a necessarily elementary structure and can be easily symbolically judged as true or false. When the brute search fails, an extra geometric construction is randomly added (like adding a midpoint of a certain line) to see if brute search using that extra raw material might work. [edit: as corrected by Imnimo, I got this backwards - the brute search is just pure brute search, the transformer is used to predict which extra geometric construction to add]
Also (not mentioned in the blog post) the actual problem statements had to be modified/adapted, e.g. the actual problem statement "Let AH1, BH2 and CH3 be the altitudes of a triangle ABC. The incircle W of triangle ABC touches the sides BC, CA and AB at T1, T2 and T3, respectively. Consider the symmetric images of the lines H1H2, H2H3, and H3H1 with respect to the lines T1T2, T2T3, and T3T1. Prove that these images form a triangle whose vertices lie on W." had to be changed to "Let ABC be a triangle. Define point I such that AI is the bisector of angle BAC and CI is the bisector of angle ACB. Define point T1 as the foot of I on line BC. Define T2 as the foot of I on line AC. Define point T3 as the foot of I on line AB. Define point H1 as the foot of A on line BC. Define point H2 as the foot of B on line AC. Define point H3 as the foot of C on line AB. Define point X1 as the intersection of circles (T1,H1) and (T2,H1). Define point X2 as the intersection of circles (T1,H2) and (T2,H2). Define point Y2 as the intersection of circles (T2,H2) and (T3,H2). Define point Y3 as the intersection of circles (T2,H3) and (T3,H3). Define point Z as the intersection of lines X1X2 and Y2Y3. Prove that T1I=IZ."