acm-header
Sign In

Communications of the ACM

ACM TechNews

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


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

Sign In for Full Access
» Forgot Password? » Create an ACM Web Account