AlphaGeometry: synthetic proofs and the neuro-symbolic loop
DeepMind's system solved 25 of 30 olympiad geometry problems by pairing a language model trained on 100 million synthetic proofs with a symbolic deduction engine. The data generation was the contribution, and it set the pattern that later math systems followed.
The result
DeepMind published AlphaGeometry in Nature on January 17. On a benchmark of 30 olympiad geometry problems, solved under competition time limits, the system got 25. The previous best, based on Wu's method, got 10. The average human gold medallist on the same problems scores 25.9. The company says it is the first system to pass the bronze threshold at the 2000 and 2015 olympiads, with the caveat that geometry is roughly a third of the problems and the system does nothing on the rest. Code and model went up on GitHub.
The number is striking and it is not the reason we keep coming back to the paper. The reason is that the language model in the system was trained on no human proofs at all.
Two components and a loop
The architecture pairs a neural language model with a symbolic deduction engine. The engine is a rule-based prover. Given a diagram's premises it derives every fact that follows by applying geometric rules, exhaustively and correctly, until nothing new appears. What it cannot do is invent. Many olympiad proofs require adding something to the diagram, a midpoint, a circle, an auxiliary line, before the deduction goes through. Choosing that construction is the creative step, and it is the step the language model handles.
The loop is simple to state. The engine runs until it stalls. The language model looks at the current state and proposes a construction. The engine runs again with the construction added. Repeat until the goal is proved or the budget runs out. The model never has to be right about the proof, only about what to add, and the engine checks everything, so a bad suggestion costs time rather than correctness.
Where the training data came from
Training a model to propose constructions needs examples of proofs that used constructions. Human olympiad proofs in a machine-readable form number in the hundreds. DeepMind built the dataset instead. They generated a billion random diagrams, ran the symbolic engine to derive every relationship among the points and lines in each, and then traced back from each derived fact to the minimal set of premises and constructions it depended on. Each traceback is a theorem with a proof. Deduplicated, that gave 100 million training examples, of which 9 million involved an added construction. The model learned from those 9 million what a useful construction looks like.
This is the part that we think was the real contribution. The engine is decades old in spirit. The language model is a standard transformer. The idea that made them work together was to use the engine as a data factory, generating proofs that are correct by construction and then learning the one step the engine cannot take from the traces of the steps it can.
Why synthetic data worked here and often does not
Synthetic data has a bad reputation because a model trained on its own outputs tends to drift toward its own errors. AlphaGeometry avoids that for a specific reason. The generator was not the model. It was a symbolic system with a correctness guarantee, so every example was true, and the traceback ensured every example was minimal and therefore informative. The diversity came from random premises rather than from sampling a model, so there was no mode collapse to inherit.
The second reason is that the task has a verifier. A proposed construction either leads to a proof or it does not, and the engine says which. That means the model can be wrong most of the time and the system still works, as long as it is right often enough that the search finishes in time. Synthetic data fails when there is no checker between the data and the training signal. Here the checker sat at both ends.
The pattern, six months on
Adding this from a later vantage. On July 25, 2024, DeepMind reported that AlphaProof and AlphaGeometry 2 together scored 28 of 42 points at that year's IMO, one point below the gold threshold, solving four of six problems. AlphaGeometry 2 was trained on an order of magnitude more synthetic data, ran a symbolic engine two orders of magnitude faster, and improved from 53 to 83 percent on 25 years of historical IMO geometry problems, solving the 2024 geometry problem in 19 seconds. AlphaProof took the same shape into general mathematics: a language model proposes, Lean verifies, and every verified proof becomes training data for the next round, over millions of problems.
So the recipe generalised. Generate problems at scale, verify with a formal system, train the proposer on what verified, repeat. It is the same structure as reinforcement learning with a checker, and the same structure that reasoning models would later apply to text math with a much weaker verifier. What we would like to see is the same loop pointed at a domain without a formal prover, where the checker is a test suite or a physical measurement, to find out how much of AlphaGeometry's success came from the loop and how much from the fact that geometry can be checked exactly.
Sources
From the foundation