An artificial intelligence developed by Google Deepmind, Google's AI research company, has managed to prove geometric theorems with better results than the average of the participants in the International Mathematical Olympiads, the most prestigious competition in the world in this field. The achievement, presented this Wednesday in the journal Nature, demonstrates the ability of AI to solve complex logical problems, a key milestone in this field of research.
AlphaGeometry, as the system has been named, has correctly solved 25 of 30 plane geometry problems proposed in the latest editions of the Olympics, a milestone only surpassed by the group of gold medalists who solved the same problems. In addition, he has found a new, more efficient way to solve one of them. His best predecessor only managed to prove 10 of the cases.
Reaching the level of the best participants in the Olympics is one of the objectives of research with artificial intelligence. Although the success of AlphaGeometry is partial, because it is limited to plane geometry theorems, the bases of which we learn in high school, and leaves out problems of another nature, such as algebra, number theory or combinatorics, it is notorious for how difficult it is to translate the problems. geometric to computational language.
This difficulty, which can be extended, although to a lesser extent, to any mathematical demonstration, is the reason why AI has not yet managed to generally surpass the best human specialists in solving theorems. The difficulty of translation means that there is very little data for machines to learn from, so training them is extremely difficult.
To achieve the leap in quality presented in the study, researchers have had to develop a completely new training system, which has been based on making the AI learn with data that it generates itself. This set of data that does not exist in the real world is known as synthetic data.
The development team only taught the system geometric and algebraic rules, which allow it to make logical reasoning based on a set of premises. For example, from the proposition “the distance from point A to point B is the same as from point B to point C”, the machine can conclude that “the distance between A and C is twice that of A to B.”
The training consisted of administering AlphaGeometry a random set of premises so that it could draw all the conclusions that can be drawn from them. Then, they made the machine analyze its own result, a kind of map of mathematical proposals linked together, to identify which premises led to each conclusion.
At the end of the cycle, the AI had identified some premises, some conclusions, and the logical procedures to move from one to another, the so-called demonstrations. The Google Deepmind team repeated this process over and over again, until they had given the system almost a billion geometric premises, and obtained 100 million conclusions and proofs.
The process that AlphaGeometry follows to prove the International Mathematical Olympiad theorems is similar to the training pattern. It is also based on the use of geometric and algebraic rules to draw the maximum possible conclusions from the premises of each problem.
The difference is that, when it reaches a dead point, where it can't go any further, the machine uses the data it has accumulated during training to create a new premise, which does not change the nature of the problem, but allows it to reach a solution. new conclusions. The operation is similar to ChatGPT, which predicts the next word based on the context of the previous ones and the knowledge you have acquired during your learning.
Each new premise that the machine adds expands more and more the number and diversity of logical conclusions it can reach. By testing each of the paths, AlphaGeometry is capable of proving extremely complex theorems for human beings. In one case, he even found a more generic and simple demonstration than what was known until now.
This ability to generate additional mathematical proposals that do not follow directly from the premises of the problem is the key that allows Google Deepmind's AI to reach a level similar to that of the best Olympic participants in theorem proving. This is an essential capacity also in other fields of mathematics, so the authors hope that their methodology will represent a leap in quality in the ability of artificial intelligence to solve complex mathematical problems.
