It is possible for a game-playing Artificial Intelligence to be able to tackle a Chatbot Blindspot

AlphaGo: A Language Model with a Novel Approach to Artificial Intelligence for Reasoning and Learning to Attempt to Resolve Mathematical Problems

A language model with a different approach to artificial intelligence, called Alphageometry was revealed by the company earlier this year. Alphageometry uses a program called Gemini that can be used to change geometry into a form that can be manipulated and tested. Google today also announced a new and improved version of AlphaGeometry.

Indeed, the research raises the prospect of addressing the worst tendencies of large language models by applying logic and reasoning in a more grounded fashion. As miraculous as large language models can be, they often struggle to grasp even basic math or to reason through problems logically.

In the future neural-symbolic method could be used to turn questions or tasks into a form that can be reasoned over in a way that produces reliable results. A system called “Strawberry” is rumored to be being worked on by Openai.

Training any language model requires massive amounts of data and not much mathematical proof existed in Lean. To overcome this problem, the team designed an additional network’ that attempted to translate an existing record of a million problems written in natural language into Lean — but without including human-written solutions, says Thomas Hubert, a DeepMind machine-learning researcher who co-led the development of AlphaProof. “Our approach was, can we learn to prove, even if we originally didn’t train on human-written proofs?” (The company had a similar approach with Go, where its AI learned to play the game by playing against itself, rather than from the way humans do.)

The world’s top students are poised to benefit from Google DeepMind’s success in mathematics, the company says.

The London-based machine-learning company announced on 25 July that its artificial intelligence (AI) systems had solved four of the six problems that were given to school students at the 2024 International Mathematical Olympiad (IMO) in Bath, UK, this month. The score for the proofs was just one point shy of a gold medal, and was marked by two top mathematicians.

There was a program that was created by the company called AlphaGo that was designed to play the board game Go with considerable skill through years of practice.

Pushmeet Kohli, vice-president of artificial intelligence for science at DeepMind, told reporters that there was a first time that any system had achieved medal-level performance. “This is a key milestone in the journey of building advanced theorem provers,” said Kohli.

In their latest effort, the researchers used AlphaGeometry2 to solve the geometry problem in under 20 seconds; the AI is an improved and faster version of their record-setting system, says DeepMind computer scientist Thang Luong.

AlphaProof, Numina and HuggingFace: Open-sourced IMO Systems, Incidents, Magic Keys, and Other Complex Problems

The team from Numina and HuggingFace won the intermediate AIMO progress prize based on simplified versions of the IMO problems, using a language model. The systems of the companies were made open-sourced. But the winners told Nature that to solve harder problems, language models alone would probably not be enough.

Many of the Lean translations were nonsensical, but enough were good enough to get AlphaProof to the point that it could start its reinforcement-learning cycles. At the press briefing, Gowers said that the results were better than expected. “Many of the problems in the IMO have this magic-key property. The problem looks hard at first until you find a magic key that unlocks it,” said Gowers, who is at the Collège de France in Paris.

“It’s clearly a very substantial advance,” says Joseph Myers, a mathematician based in Cambridge, UK, who — together with Fields Medal-winner Tim Gowers — vetted the solutions and who had helped select the original problems for this year’s IMO.

DeepMind computer scientist David Silver, who was one of the original researchers in developing AlphaGo, said that they were at the point where they can prove not open research problems, but some very challenging ones to the very best young mathematicians in the world.

The press briefing notes that it is not certain whether the techniques can be mastered to the point of doing research-level work in mathematics. Can it include other sorts of mathematics where there might not be a million problems to train on?