Olympiad geometry solved without human demonstrations
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.
- 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 and known objections
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.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Peer reviewed and Search scaffold.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded peer reviewed for verification and search scaffold for autonomy. What these mean.
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-alphageometryBibTeX
@misc{whataifound-googledeepmind-2024-alphageometry,
title = {Olympiad geometry solved without human demonstrations},
author = {{whataifound.org}},
year = {2024},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Google DeepMind. Verification: Peer reviewed. Autonomy: Search scaffold.},
url = {https://whataifound.org/finding/2024-01-17-alphageometry}
}