Communications of the ACM
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