The paper discusses the capacities and limitations of current artificial intelligence (AI) technology to solve word problems that combine elementary knowledge with commonsense reasoning. No existing AI systems can solve these reliably. We review three approaches that have been developed, using AI natural language technology: outputting the answer directly, outputting a computer program that solves the problem, and outputting a formalized representation that can be input to an automated theorem verifier. We review some benchmarks that have been developed to evaluate these systems and some experimental studies. We argue that it is not clear whether these kinds of limitations will be important in developing AI technology for pure mathematical research, but that they will be important in applications of mathematics, and may well be important in developing programs capable of reading and understanding mathematical content written by humans.
翻译:本文讨论了当前人工智能(AI)技术解决将基本知识与常识推理相结合的字眼问题的能力和局限性。现有的人工智能系统无法可靠地解决这些问题。我们审查了使用AI自然语言技术开发的三种方法:直接输出答案,输出一个能解决问题的计算机程序,以及输出一个可以输入自动理论验证器的正式代表。我们审查了为评价这些系统和一些实验研究而制定的一些基准。我们争论说,这些限制是否对于开发AI技术进行纯数学研究很重要,但对于数学应用十分重要,对于开发能够阅读和理解人类数学内容的方案可能也很重要。