AlphaGeometry
A language model suggests extra points and lines for a geometry figure, and a symbolic engine checks what follows.
The loop
- Proposes
Auxiliary constructions (new points and lines) for an Olympiad geometry problem
- Judged by
A symbolic deduction engine that derives all consequences and decides whether the goal is proved
- Steers
The enlarged figure goes back to the language model for the next construction, under beam search
Headline result
In the paper's evaluation on a test set of 30 olympiad-level geometry problems (IMO-AG-30), AlphaGeometry solves 25, versus ten for the earlier Wu's method baseline and 18 for the strongest baseline (DD + AR + human-designed heuristics). Symbolic deduction with algebra (DD + AR) alone solves 14.
What this does not prove
The 30-problem set is geometry only, translated into the system's own formal language. The language model is trained once on synthetic data before the search runs; it is not retrained by the search results. A later study (Sinha et al., arXiv:2404.06405) reports that Wu's method alone solves 15 of the same 30 problems, so the ten-problem baseline is contested.
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
The symbolic engine does the proving and calls the language model only when it is stuck, and the result is a human-readable proof that stands without the model.
Classification
| What it proposes | Mathematical construction |
|---|---|
| Generative model | Transformer language model trained from scratch on synthetic theorems and proofs |
| Algorithmic authority | Symbolic deduction engine (DD + AR) |
| Feedback | Proof state |
| What gets updated | Search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |