An AI system trained only on machine-made examples solved 25 of 30 olympiad geometry problems, close to the level of an average International Mathematical Olympiad gold medallist. The previous best program solved 10, and GPT-4 solved none.
The system, called AlphaGeometry, was built by Trieu Trinh, Yuhuai Wu, Quoc Le and Thang Luong of Google DeepMind and He He of New York University. They described it in a paper published in Nature on January 17, 2024.
100 million proofs, none written by people
Geometry has been hard for machine learning because there are very few human proofs written in a form a computer can check. The DeepMind team skipped human examples entirely.
They randomly sampled nearly 1 billion sets of geometric starting conditions and let a symbolic deduction engine work out everything that followed from each. Tracing back each conclusion to the minimum premises it needed produced more than 100 million unique synthetic theorems and proofs. The longest ran to 247 steps.
The key trick concerned auxiliary constructions, the extra points or lines a solver adds to make a proof work. About 9% of the synthetic proofs needed them, roughly 9 million examples. A language model trained from scratch on all the data, then fine-tuned on those 9 million, learned to suggest such constructions without ever seeing a human do it.
During a proof, the two parts take turns. The symbolic engine deduces everything it can; when it gets stuck, the language model proposes a new point, and the engine tries again.
How it compares on real olympiad problems
The test set, IMO-AG-30, contains 30 geometry problems from olympiads since 2000 that could be translated into the system’s specialized geometry language, about 75% of eligible problems.
- AlphaGeometry: 25 solved
- Strongest baseline, the team’s new symbolic engine plus human-designed heuristics on 250 parallel workers: 18
- Wu’s method, the previous state of the art: 10
- GPT-4 writing full proofs: 0
The language model’s constructions alone added 11 solved problems on top of the symbolic engine. Even with only 20% of the training data, or less than 2% of the search budget, the system still solved 21.
On a broader set of 231 geometry problems, including textbook exercises and famous theorems, it solved 98.7%, against 75% for Wu’s method.
Its proofs are readable. The team sent its solutions for the 2000 and 2015 olympiads, where it solved every geometry problem, to the USA IMO team coach, who recommended full marks. While extracting its proof for a 2004 problem, the system also noticed that one condition was unnecessary, giving a more general version of the theorem.
Limits of the comparison
The authors stress that the human comparison is approximate. Contestants read natural-language problems, face a 4.5-hour limit and must also handle algebra, number theory and combinatorics, while AlphaGeometry works on translated geometry statements only. They also note that it proves things with a much lower-level toolkit than humans use, which limits how readable its proofs are.
The hardest problems for humans, such as IMO 2000 Problem 6 and 2015 Problem 3, were also the ones that needed AlphaGeometry’s longest proofs.
Study Details:
- Title: Solving olympiad geometry without human demonstrations
- Authors: Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, Thang Luong
- Journal: Nature
- Publication Date: January 17, 2024
- DOI: 10.1038/s41586-023-06747-5