A team of researchers recently created an artificial intelligence that can translate math problems written in English to formal code, making it much easier for computers to solve. This process is called ‘formalization’.
Computers have only been able to solve and verify mathematical problems if the problems are prepared in a specifically designed proving language, and it takes years of work just for a single proof.
Yuhai Wu and his colleagues at Google made use of a neural network called Codex created by OpenAI, an AI research company. The network was trained on large amounts of programming data and text from the web. Programmers can also use it to generate workable code.
The team tested Codex to see if it could formalize a bank of 12,500 high school math competition problems. The Codex was able to translate a quarter of the problems into a format compatible with a formal proof solver problem called Isabelle. Wu said, ‘If you show the model with an example that explains that concept, the model can they quickly pick it up.’
To test how effective the auto-formalization process was, the team applied Codex to some problems already formalized by humans. Codex generated formal versions of these problems, while the team used another AI called MiniF2F to solve both versions.
MiniF2F’s success rate of the auto-formalized problems improved from 29% to 35%, which suggests that Codex is better at formalizing these problems than humans.
Wu said that the team’s work is only proof of a concept. ‘If the goal is to train a machine that is capable of doing the same level of mathematics as the best humans, then auto-formalization seems to be a very crucial path towards it,’ said Wu.
Albert Jiang, team member at the University of Cambridge, believes that enhancing the success rate would allow AIs further compete with human mathematics. ‘If we get to 100%, we will definitely be creating an artificial intelligence agent that’s able to win an International Maths Olympiad gold medal,’ he said.
Although the current goal is to enhance the auto-formalization, there could be larger implications. Wu believes the models could also uncover areas of mathematics unknown to humans.
The reasoning capacity of the machine makes it a suitable fit for verification tasks. ‘You can verify whether a piece of software is doing exactly what you asked it to do, or you can verify hardware chips, so it has applications in financial trading algorithms and hardware design,’ said Jiang.
According to Yang-Hui He at the London Institute for Mathematical Sciences, the real challenge could be using the model on mathematical research, most of which is written in LaTeX, a typesetting system. ‘We only use LaTeX because it types nicely, but it’s a natural language in some sense, it has its own rules,’ said He.
By Marvellous Iwendi
Source: New Scientist