Sign In

Communications of the ACM

ACM TechNews

AI Translates Math Problems into Code to Make Them Easier to Solve

View as: Print Mobile App Share:

Asked to formalize a bank of 12,500 secondary school math competition problems, the Codex neural network was able to translate a quarter of the problems into a format compatible with the Isabelle formal proof solver program.

Credit: alengo/Getty Images

Google's Yuhuai Wu and colleagues used the Codex neural network of artificial intelligence (AI) research company OpenAI to translate mathematical problems from plain English into formal code.

Codex correctly translated 25% of 12,500 secondary-school math competition problems into a format compatible with a formal proof-solver program called Isabelle.

Wu said the system's inability to understand certain mathematical concepts was responsible for many of the unsuccessful translations.

The team then tested the process by applying Codex to problems pre-formalized by humans.

The network produced its own formal versions, and the researchers used the MiniF2F AI to solve both versions; the auto-formalized versions raised MiniF2F's success rate from 29% to 35%, suggesting Codex's formalization was superior to that of humans.

From New Scientist
View Full Article


Abstracts Copyright © 2022 SmithBucklin, Washington, DC, USA


No entries found