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
Sources
Original work
Announcement
Challenge
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. An independent re-evaluation found the symbolic baseline much stronger than reported: Wu's method alone solves 15 of the 30, not 10, and with classical synthetic methods 21, which narrows the margin the headline comparison implies. 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.
Independent checks
Sinha, Prabhu, Kumaraguru, Bhat and Bethge (re-evaluation of the benchmark): Revisited IMO-AG-30 and found Wu's method alone solves 15 problems, not the 10 reported as the baseline, and with classical synthetic methods solves 21 of 30 on a CPU-only laptop, four fewer than AlphaGeometry; combined with AlphaGeometry it reaches 27. · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
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.
History of this entry
- ChallengedCited an independent re-evaluation of the benchmark finding the symbolic baseline stronger than reported, 21 of 30 rather than 10. No grade moved. source ↗
- 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.
Community discussion
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}
}