AlphaGeometry

A system with two halves

AlphaGeometry is a geometry-solving AI system announced by Google DeepMind on 17 January 2024, together with a paper published in Nature^[1]. It belongs to a line of work called neuro-symbolic AI: rather than relying on a single neural network, it pairs a neural language model with a symbolic deduction engine^[1]. The two halves do different jobs. The language model handles the part of a proof that looks like guesswork — which step or construction to try next — while the deduction engine applies formal rules one step at a time, so that each step is checked rather than merely predicted. The point of the pairing is that the neural half supplies flexibility and the symbolic half supplies certainty.

Trained from scratch on synthetic problems

The system was trained from scratch, with no human demonstrations^[1]. Its training data consisted of 100 million unique synthetic examples of varying difficulty, nine million of which featured added constructs^[1]. In other words, the examples were generated rather than collected from proofs written by people, and part of them include extra constructions — the auxiliary lines or circles that a geometry problem often requires but that are not present in the original figure^[1].

Results on a benchmark of olympiad problems

To measure progress, the team put together IMO-AG-30, a benchmark of 30 olympiad geometry problems compiled from Olympiads held between 2000 and 2022^[1]. On this benchmark AlphaGeometry solved 25 of the 30 problems within competition time limits^[1]. The previous best method, Wu's method, solved 10^[1]. For comparison, human gold medallists averaged 25.9^[1]. DeepMind said AlphaGeometry was the first AI model capable of passing the bronze medal threshold of the International Mathematical Olympiad in 2000 and 2015^[1].

Open code, open model

The code and the model were open-sourced^[1]. The paper's authors include Trieu Trinh, Yuhuai Wu, Quoc Le, He He and Thang Luong^[1].

AlphaGeometry 2

An improved version, AlphaGeometry 2, solved the geometry problem at the 2024 International Mathematical Olympiad within 19 seconds of receiving its formalisation^[2]. Across historical IMO geometry problems from the past 25 years, it solved 83%, against 53% for its predecessor^[2].

Why it matters

Geometry proofs are a demanding test for a machine: an answer is only the beginning, because every intermediate step has to be justified. A solver therefore needs both a way to find promising moves and a way to guarantee that what it finds is actually valid. AlphaGeometry connects the two — proposals from a language model, verification by a deduction engine — and on a curated set of olympiad problems it brought a machine to a level close to that of human gold medallists^[1]. The decision to release the code and the model let other researchers reuse and examine the approach^[1], and the later AlphaGeometry 2 extended the same line of work to a much larger share of historical olympiad geometry problems^[2].