Olympiad geometry solved without human demonstrations
Olympiad geometry solved without human demonstrations is graded peer reviewed on whataifound.org, with the AI's role graded search scaffold.
A language model trained purely on synthetic data, paired with a symbolic deduction engine, solved 25 of 30 olympiad geometry problems against 10 for the previous best automated system and 25.9 for the average human gold medallist.
- Verification
- Peer reviewed
- Autonomy
- Search scaffold
- Lab
- Google DeepMind
- Model
- AlphaGeometry
- Field
- Mathematics
- Date
- 2024-01-17
- Human collaborators
- Trieu Trinh, Thang Luong
What was found
Geometry proofs stall when they need an auxiliary construction — an extra point or line that is not in the problem statement. AlphaGeometry pairs a symbolic deduction engine, which exhausts what follows mechanically, with a language model that proposes constructions when deduction runs dry. The model was trained on 100 million synthetic proofs generated from random diagrams, with no human proof data, and its output is a symbolic proof that the deduction engine checks. Published in Nature.
Novelty check
Automated geometry provers date to Wu's method in the 1970s and to GEX/Java Geometry Expert; the prior state of the art solved 10 of the 30 benchmark problems. The benchmark is IMO geometry problems from 2000–2022 with known solutions, so the contribution is the method and the score, not a new theorem.
Caveats
Benchmark performance on solved problems, not a discovery. The domain is narrow: plane geometry expressible in the system's formal language, which excludes problems involving inequalities or variable numbers of points, and the benchmark set was filtered to what the language can state. Proof steps are machine-checked by the deduction engine, which is what carries the confidence; the peer-reviewed grade reflects Nature review of the system and results.
Sources
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is peer reviewed and search scaffold. Full definitions are in the methodology.
Cite this entry
whataifound.org (2024). Olympiad geometry solved without human demonstrations. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2024-01-17-alphageometry