Google DeepMind AI system reaches milestone in global math contest

It’s difficult to assess how smart AlphaProof really is, and the level of reasoning it has, just as looking at how ChatGPT does on the LSAT doesn’t offer a clear metric of its intelligence.

But being able to come to the correct answers on complex mathematical and reasoning problems may be a critical step in achieving the science fiction-like levels of AGI that companies like Google and OpenAI are chasing after. To be sure, it’s clear AlphaProof doesn’t solve math problems the same way humans do, using more brute force and guesswork in some cases. It generates proofs by searching and trying out various combinations of possible mathematical steps to arrive at the best solution.

Alex Davies, a research engineer at Google DeepMind, told Semafor that AlphaProof works a bit like the company’s previous model, AlphaGo, designed to play the strategy-based board game Go. Instead of searching over possible moves, however, AlphaProof tries to find the right sequence of proof steps. “In any given attempt at a problem, [it’s] limited to fewer moves than would be explored in chess or Go systems,” he said.

But human IMO participants rely on their knowledge of theorems, and develop an intuition for how to solve a problem. They don’t have to consider as many different possibilities, and in many ways, are more efficient and intelligent than machines. In one case, AlphaProof took three days to finally arrive at a solution, for example.

Still, general large language models that power AI chatbots often struggle with basic math. They hallucinate and cannot even accurately determine which number is larger than another sometimes. AlphaProof avoids these problems by generating its answers in code. If it manages to write a program that can be executed on a computer without errors, its solution may be correct; but if it can’t, its answer is definitely wrong.

The researchers generated synthetic data to train the system. It learned the geometric relationships in various shapes by inspecting 100 million randomly drawn diagrams, and their specific proofs to figure out how to solve new problems.

The system, however, revealed glimmers of brilliance, according to Sir Timothy Gowers, a combinatorics professor at Collège de France, and a Fields medalist, the top prize in math that’s often compared to a Nobel Prize in science, and IMO gold medalist.

Gowers said that in order to find a solution, mathematicians have to find clever tricks like “magic keys” that unlock the problem. Initially, he thought that finding these magic keys was “probably a bit beyond” AlphaProof’s abilities, but was surprised to see it had found them once or twice in its solutions.

“I find it very impressive, and a significant jump from what was previously possible,” he said.

Although AI has gotten much better at math, it’s not clear how these skills can be applied in the real world yet. Google DeepMind is looking at how AlphaProof may aid researchers as a “proof assistant.”

David Silver, VP, Reinforcement Learning at Google DeepMind, said that good mathematicians do a lot more than just solving problems. They also pose questions, and come up with fresh ways of thinking to invent new fields of mathematics. He said that AlphaProof was “not adding to the mathematical body of knowledge that humans have created” so far. No AI can do that yet.

Silver told me that it’d take a lot more breakthroughs in math and technology to reach that point. Maybe this should be the true test for whether we’ve reached AGI or not.