Solving olympiad geometry without human demonstrations
Written for the Research library (claude-opus-5-5) from the paper text. Original — nature.com/articles/s41586-024-07115-7.pdf
Summary
Automated proving of olympiad-level geometry has been limited by a lack of training data. Few human proofs exist in a machine-readable form, and translating them into formal language is expensive. The authors present AlphaGeometry, a theorem prover trained without any human demonstrations. They sample random geometric premises, run a symbolic deduction engine on them, and trace each derived fact back to the premises it depends on. This yields about 100 million synthetic theorems with proofs. When a proof requires extra points, that example teaches the system how to invent auxiliary constructions. A transformer language model trained from scratch on this data proposes new constructions. A symbolic engine, combining a deductive database with algebraic reasoning, carries out the rigorous deduction. The two take turns until the goal is proven. On 30 recent IMO geometry problems, AlphaGeometry solves 25. The previous best system solved 10, and the new result approaches the level of an average IMO gold medallist. The proofs it produces are readable by humans. The work shows that synthetic data can stand in for scarce human data in mathematical reasoning.
Key points
- Neuro-symbolic design: the language model suggests auxiliary points and objects, and the symbolic engine (DD + AR) derives all facts that follow from them.
- Synthetic corpus: about 100M unique theorem–proof examples generated from random premises; around 9M of them involve auxiliary constructions.
- Benchmark IMO-AG-30 (30 IMO geometry problems from 2000–2022): AlphaGeometry solved 25. The earlier state of the art, based on Wu's method, solved 10. Average gold medallists score about 25.9.
- Generalisation: the system found a more general version of a theorem from IMO 2004.
- Source caveat: the extract you supplied contains only the Feb 2024 Author Correction, which fixes the acknowledgement name "P. Pak" to "P. Bak", not the paper itself. This summary is based on the published article's content as I know it, so please check the figures against the full text.
Cited by
- Large Language Models for Mathematical Reasoning: Progresses and Challenges
- Large Language Monkeys: Scaling Inference Compute with Repeated Sampling
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models
- OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems
- MathVista: Evaluating Mathematical Reasoning of Foundation Models in Visual Contexts
- AlphaEvolve: A coding agent for scientific and algorithmic discovery
- DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
- Can LLMs Generate Novel Research Ideas? A Large-Scale Human Study with 100+ NLP Researchers
- Measuring Multimodal Mathematical Reasoning with MATH-Vision Dataset
- DAPO: An Open-Source LLM Reinforcement Learning System at Scale
Cite
@inproceedings{trinh2024solving,
title = {{Solving olympiad geometry without human demonstrations}},
author = {Trinh, Trieu H. and Wu, Yuhuai and Le, Quoc V. and He, He and Luong, Thang},
booktitle = {Nature 625},
year = {2024},
url = {https://www.nature.com/articles/s41586-024-07115-7}
}