Useful Direction.
AI Translates Math Problems into Code to Make Them Easier to Solve
New Scientist, Alex Wilkins, June 6, 2022
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.... '
No comments:
Post a Comment