Nature News: AI is close to human gold medalists in solving high school math Olympiad problems

Artificial intelligence (AI) has learned to solve difficult problems in the International Mathematical Olympiad, reaching a level close to that of human gold medalists.

This AI model, called AlphaGeometry, was developed by a joint team from Google DeepMind and New York University . It is an AI system that can solve geometry problems at the level of the International Mathematical Olympiad and was published in the top scientific journal Nature today .

It is reported that AlphaGeometry has solved 25 of the 30 latest Olympiad-level (a mathematics theorem proving competition for outstanding high school students) problems by autonomously synthesizing millions of theorems and proofs, which is close to the average performance of gold medalists in the International Mathematical Olympiad and far exceeds the best previous automated theorem proving system.

This breakthrough marks a significant advance in AI's ability to solve mathematical problems autonomously, allowing it to solve complex geometric challenges without the need for human demonstrations .

The research demonstrates the potential for AI to solve complex logic challenges at near-human levels — a major goal of AI research.

Notably, AlphaGeometry can generate human-readable proofs and even discovered a new version of a theorem from the 2004 International Mathematical Olympiad .

The related research paper, titled “Solving olympiad geometry without human demonstrations”, has just been published in Nature.

Is it difficult for AI to solve Olympiad math problems?

The pursuit of better theorem proving capabilities has been a focus of AI research since the 1950s. The Mathematical Olympiad is the world's most famous theorem proving competition, dating back to 1959, and plays an important role in discovering outstanding talents.

The questions in the International Mathematical Olympiad usually involve deep mathematical theories and abstract mathematical concepts, requiring independent thinking, creative problem solving and the use of intuition. These problems often require a high degree of logical reasoning and creative thinking, which are possessed by human mathematicians , but go beyond the application scope of traditional machine learning methods.

Furthermore, compared to other fields, the human process of solving mathematical problems is not easily translated into large-scale datasets that can be used for training. Geometry is particularly difficult to translate, and there are few examples of proofs in common mathematical languages. And the language of geometry has very precise definitions and cannot express many human proofs that use things outside of geometry, such as complex numbers.

Figure | Side-by-side comparison of human proofs and AlphaGeometry proofs for IMO2000P6. This is a harder problem (average human score = 1.05/7) with a large number of objects in the problem statement. Left, the human solution uses complex numbers. The problem is greatly simplified by a carefully chosen coordinate system, and the solution can be naturally derived through algebraic operations. Right, the AlphaGeometry solution involves two auxiliary constructions and more than 100 derivation steps, many of which are extremely tedious for humans. In this case, the search-based solution is much less readable and intuitive. A more structured organization, i.e., a high-level proof outline, can greatly improve the readability of the AlphaGeometry solution. Building many high-level derivation rules in AlphaGeometry helps reduce low-level derivations and simplify proof steps. (Source: the paper)

The lack of sufficient sample data, especially the solution process of human professional mathematicians, makes it difficult for machine learning models to learn and understand the solution methods . Therefore, current geometric methods still mainly rely on symbolic methods and manually designed hard-coded search heuristics.

Solve complex problems autonomously without humans

The key innovation of AlphaGeometry in this research is that it can synthesize millions of theorems and proofs of varying complexity and train itself using a neural language model trained from scratch. This means that AlphaGeometry can independently learn and solve a variety of complex problems without relying on human input.

Neural language models have unique advantages in guiding symbolic deduction engines (which can search for a large number of branch points in difficult problems). The introduction of neural models enables AlphaGeometry to make more accurate reasoning when dealing with challenging problems. This method of combining symbolic deduction engines and neural language models is one of the important innovations of this research.

Figure | Overview of AlphaGeometry and how it solves simple problems and IMO 2015 Problem 3. The top row shows how AlphaGeometry solves simple problems. a) Simple example and its diagram. b) The model starts the proof search by running the symbolic deduction engine. The engine exhaustively derives new statements from the theorem premises until the theorem is proved or the new statements are exhausted. c) As the symbolic engine fails to find a proof, the language model constructs an auxiliary point that increments the proof state before the symbolic engine tries again. The loop continues until a solution is found. d) For the simple example, the loop terminates after the first auxiliary construction “D as the midpoint of BC”. The proof includes two more steps, both of which exploit the midpoint property: “BD = DC” and “B, D, C are collinear”. The bottom row shows how AlphaGeometry solves IMO 2015 Problem 3 (IMO 2015 P3). e) IMO 2015 P3 problem statement and diagram. f The solution to IMO 2015 P3 has 3 auxiliary points. (Source: This paper)

Although AlphaGeometry has achieved remarkable success in solving Olympic-level geometry problems, it also has some limitations .

According to the paper, AlphaGeometry mainly focuses on solving Olympic-level geometry problems, and its application scope is relatively narrow . This limits the promotion of this method to other mathematical fields or practical problems. Future research needs to explore how to expand this method to cover a wider range of mathematical fields.

Moreover, the research team used large-scale artificial synthetic data to train AlphaGeometry. Although this provides a wide range of learning materials for the model, the synthetic data may still not fully cover the diversity and complexity of real mathematical problems . Therefore, the performance of the model in real scenarios may be affected by insufficient data.

Furthermore, while AlphaGeometry is able to generate human-readable proofs, the results it generates can become difficult to understand when dealing with extremely complex reasoning, making it difficult to track and interpret the model’s reasoning process in some cases .

AI has great potential in solving mathematical problems

In recent years, using AI technology to understand and prove mathematical theorems has been one of the research directions that scientists have focused on.

For example, AI can be used to develop automated theorem proving systems that can independently derive and prove mathematical theorems. This approach aims to reduce the burden of manual proof and provide more efficient proof methods.

In addition, AI can also be used to build mathematical knowledge graphs , which helps model the relationship between mathematical concepts into a graph structure. This graph can be used to improve the reasoning and proof of theorems, allowing the system to better understand the knowledge system in the field of mathematics.

AI also has a place in the development of creative thinking. Some studies use generative models, such as generative adversarial networks (GANs), to generate new theorems that conform to mathematical structures and norms . This approach helps to expand creative thinking in the field of mathematics and introduce new mathematical concepts and conclusions.

Of course, there is still a long way to go before AI can perform at the same level as top human mathematicians in mathematics.

Nevertheless, AlphaGeometry demonstrates the potential for the application of AI in mathematics. This achievement not only brings innovation to the field of mathematics, but also opens up new possibilities for the application of AI in other fields.

Paper link: https://www.nature.com/articles/s41586-023-06747-5