AlphaGeometry2
A stronger AlphaGeometry: a Gemini-based model proposes constructions, several search trees share what they learn, and a symbolic engine checks the proof.
The loop
- Proposes
Auxiliary constructions for geometry problems, from a Gemini-architecture language model
- Judged by
An improved symbolic deduction engine
- Steers
Parallel search trees share facts (SKEST), so one tree's findings guide the others
Headline result
Solves 42 of 50 IMO geometry problems from 2000 to 2024 (IMO-AG-50); the paper states an overall solving rate of 84% on geometry problems from the last 25 years versus 54% for the original, and says AG2 surpasses an average gold medalist. The formal language now covers 88% of those problems, up from 66%.
What this does not prove
Geometry only. The paper reports progress toward, not completion of, a fully automated pipeline from natural-language problem statements. The AG2 system was also part of the IMO 2024 silver-medal-standard result.
How it generalizes the harness
- The algorithm is the solver
- Inverted control
- A domain authority judges
- The output outlives the model
- Search over a population
Same symbolic-engine-in-charge design as the original, now with a population of search trees that exchange knowledge.
Classification
| What it proposes | Mathematical construction |
|---|---|
| Generative model | Gemini-architecture language model trained on synthetic data |
| Algorithmic authority | Symbolic deduction engine |
| Feedback | Proof state |
| What gets updated | Search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Successor |