How Google DeepMind’s AI system can solve geometry problems like a math Olympian

Cracking the Geometry Code

Geometry is one of the oldest and most beautiful branches of mathematics, but also one of the most challenging for both humans and machines. Solving complex geometry problems requires not only spatial intuition, but also logical reasoning and creativity.

That’s why the International Mathematical Olympiad (IMO), the world’s most prestigious math competition for high-school students, often features geometry problems that test the participants’ ability to discover and prove new geometric properties and relationships.

But what if an AI system could solve these problems too? That’s the question that researchers from Google DeepMind and New York University set out to answer in their latest paper published in Nature. They introduced AlphaGeometry, an AI system that can solve geometry problems at a level approaching a human Olympiad gold-medalist.

AlphaGeometry solving an Olympiad problem: Problem 3 of the 2015 International Mathematics Olympiad (left) and a condensed version of AlphaGeometry’s solution (right). The blue elements are added constructs. AlphaGeometry’s solution has 109 logical steps.

AlphaGeometry is a breakthrough in AI performance, as it surpasses the previous state-of-the-art approach for geometry problems, and demonstrates AI’s growing ability to reason logically and discover new knowledge.

In this #AI_Explained, I will explain you how AlphaGeometry works, how it was trained, and what it means for the future of AI and mathematics.

How AlphaGeometry works

AlphaGeometry is a neuro-symbolic system, which means it combines the strengths of two different types of AI methods: neural networks and symbolic logic.

Neural networks are powerful machine learning models that can learn from data and make predictions, but they often lack the ability to explain their decisions or reason rigorously. Symbolic logic, on the other hand, is based on formal rules and symbols that can be used to deduce conclusions and provide explanations, but it can be slow and inflexible when dealing with large and complex problems.

AlphaGeometry uses both methods in a complementary way: a neural network provides fast and intuitive suggestions, and a symbolic logic engine provides rational and verifiable proofs.

AlphaGeometry solving a simple problem: Given the problem diagram and its theorem premises (left), AlphaGeometry (middle) first uses its symbolic engine to deduce new statements about the diagram until the solution is found or new statements are exhausted. If no solution is found, AlphaGeometry’s language model adds one potentially useful construct (blue), opening new paths of deduction for the symbolic engine. This loop continues until a solution is found (right). In this example, just one construct is required.

The neural network is a language model, which means it can process natural language and generate text. The language model is trained to predict which new geometric constructs, such as points, lines, or circles, would be most useful to add to a given problem diagram, from an infinite number of possibilities.

The symbolic logic engine is a deduction engine, which means it can apply logical rules and axioms to derive new statements and proofs about a given problem diagram. The deduction engine can use the constructs suggested by the language model to make further deductions and find the solution.

The system works in a loop: the language model predicts a new construct, the deduction engine adds it to the diagram and tries to find a proof, and if no proof is found, the loop repeats until a solution is found or a time limit is reached.

How AlphaGeometry was trained

One of the challenges of training an AI system to solve geometry problems is the lack of data. Unlike other domains, such as natural language or vision, where there are large and diverse datasets available, geometry problems are scarce and hard to obtain.

To overcome this challenge, the researchers developed a novel method to generate synthetic data, that is, artificial geometry problems and solutions, without any human input.

The method is based on the idea of "symbolic deduction and traceback". The system starts by generating random diagrams of geometric objects, such as triangles, circles, and polygons, and then exhaustively derives all the possible relationships and proofs contained in each diagram, using the deduction engine

Visual representations of the synthetic data generated by AlphaGeometry

Then, the system works backwards to find out what additional constructs, if any, were needed to arrive at those proofs, using the language model. This way, the system can create a large and diverse dataset of geometry problems and solutions, with varying difficulty and complexity.

The researchers used this method to generate 100 million synthetic examples, of which nine million featured added constructs. They used this dataset to train the language model and the deduction engine, without any human demonstrations or guidance.

What AlphaGeometry means

AlphaGeometry is a remarkable achievement in AI and mathematics, as it shows that an AI system can solve complex and creative geometry problems that challenge even the best human mathematicians.

The system was tested on a benchmark of 30 Olympiad geometry problems, compiled from the Olympiads from 2000 to 2022, and solved 25 of them within the standard Olympiad time limit. For comparison, the previous state-of-the-art system, based on a method called “Wu’s method”, solved only 10 of these problems, and the average human gold medalist solved 25.9 problems.

In benchmarking set of 30 Olympiad geometry problems (IMO-AG-30), compiled from the Olympiads from 2000 to 2022, AlphaGeometry solved 25 problems under competition time limits. This is approaching the average score of human gold medalists on these same problems. The previous state-of-the-art approach, known as “Wu’s method”, solved 10.

The system’s solutions were checked and verified by computer, and also evaluated by Evan Chen, a math coach and former Olympiad gold-medalist, who praised the system’s output as "impressive, verifiable, and clean".

AlphaGeometry is not only a powerful tool for solving geometry problems, but also a potential source of inspiration and discovery for new mathematical knowledge. The system can generate novel and elegant proofs that humans may not have thought of, and can also tackle open problems in geometry that have not been solved yet.

Moreover, AlphaGeometry is an example of how AI systems can learn from scratch, using synthetic data and self-supervision, without any human intervention. This approach could open up new possibilities for AI research and applications across different domains and disciplines.

AlphaGeometry is also a step towards building more general and advanced AI systems that can reason across different fields of mathematics and science, and that can extend the frontiers of human knowledge and understanding.

The researchers have open-sourced the AlphaGeometry code and model, and hope that it will help the AI and math communities to explore and advance this exciting area of research.

You can read the full paper in Nature, and learn more about AlphaGeometry on the Google DeepMind blog.