Solving olympiad geometry without human demonstrations

Trieu H. Trinh (), Yuhuai Wu, Quoc V. Le, He He and Thang Luong ()
Additional contact information
Trieu H. Trinh: Google Deepmind
Yuhuai Wu: Google Deepmind
Quoc V. Le: Google Deepmind
He He: New York University
Thang Luong: Google Deepmind

Nature, 2024, vol. 625, issue 7995, 476-482

Abstract: Abstract Proving mathematical theorems at the olympiad level represents a notable milestone in human-level automated reasoning1–4, owing to their reputed difficulty among the world’s best talents in pre-university mathematics. Current machine-learning approaches, however, are not applicable to most mathematical domains owing to the high cost of translating human proofs into machine-verifiable format. The problem is even worse for geometry because of its unique translation challenges1,5, resulting in severe scarcity of training data. We propose AlphaGeometry, a theorem prover for Euclidean plane geometry that sidesteps the need for human demonstrations by synthesizing millions of theorems and proofs across different levels of complexity. AlphaGeometry is a neuro-symbolic system that uses a neural language model, trained from scratch on our large-scale synthetic data, to guide a symbolic deduction engine through infinite branching points in challenging problems. On a test set of 30 latest olympiad-level problems, AlphaGeometry solves 25, outperforming the previous best method that only solves ten problems and approaching the performance of an average International Mathematical Olympiad (IMO) gold medallist. Notably, AlphaGeometry produces human-readable proofs, solves all geometry problems in the IMO 2000 and 2015 under human expert evaluation and discovers a generalized version of a translated IMO theorem in 2004.

Date: 2024
References: Add references at CitEc
Citations: View citations in EconPapers (3)

Downloads: (external link)
https://www.nature.com/articles/s41586-023-06747-5 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:nat:nature:v:625:y:2024:i:7995:d:10.1038_s41586-023-06747-5

Ordering information: This journal article can be ordered from
https://www.nature.com/

DOI: 10.1038/s41586-023-06747-5

Access Statistics for this article

Nature is currently edited by Magdalena Skipper

More articles in Nature from Nature
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().