×

A promising path towards autoformalization and general artificial intelligence. (English) Zbl 1455.68260

Benzmüller, Christoph (ed.) et al., Intelligent computer mathematics. 13th international conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12236, 3-20 (2020).
Summary: An autoformalization system is an AI that learns to read natural language content and to turn it into an abstract, machine verifiable formalization, ideally by bootstrapping from unlabeled training data with minimum human interaction. This is a difficult task in general, one that would require strong automated reasoning and automated natural language processing capabilities. In this paper, it is argued that autoformalization is a promising path for systems to learn sophisticated, general purpose reasoning in all domains of mathematics and computer science. This could have far reaching implications not just for mathematical research, but also for software synthesis. Here I provide the outline for a realistic path towards those goals and give a survey of recent results that support the feasibility of this direction.
For the entire collection see [Zbl 1452.68005].

MSC:

68V20 Formalization of mathematics in connection with theorem provers
68T05 Learning and adaptive systems in artificial intelligence
68T50 Natural language processing
PDFBibTeX XMLCite
Full Text: DOI