First Experiments with Neural Translation of Informal to Formal Mathematics

05/10/2018

∙

by   Qingxiang Wang, et al.

∙

0

∙

share

We report on our first experiments to train deep neural networks that automatically translate informalized -written Mizar texts into the formal Mizar language. Using Luong et al.'s neural machine translation model (NMT), we tested our aligned informal-formal corpora against various hyperparameters and evaluated their results. Our experiments show that NMT is able to generate correct Mizar statements on more than 60 percent of the inference data, indicating that formalization through artificial neural network is a promising approach for automated formalization of mathematics. We present several case studies to illustrate our results.