Abstract
We report on our experiments to train deep neural networks that automatically translate informalized LaTeX-written Mizar texts into the formal Mizar language. To the best of our knowledge, this is the first time when neural networks have been adopted in the formalization of mathematics. 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 our best performing model configurations are able to generate correct Mizar statements on 65.73\% of the inference data, with the union of all models covering 79.17\%. These results indicate that formalization through artificial neural network is a promising approach for automated formalization of mathematics. We present several case studies to illustrate our results.
Abstract (translated)
我们汇报了我们的实验，以培训深度神经网络，该网络可以自动将非正式的LaTeX书面Mizar文本翻译成正式的Mizar语言。就我们所知，这是神经网络在数学形式化中首次被采用。使用Luong等人的神经机器翻译模型（NMT），我们测试了我们对齐的非正式语料库对各种超参数并评估其结果。我们的实验表明，我们最好的模型配置能够在推理数据的65.73％上生成正确的Mizar语句，所有模型的并集涵盖了79.17％。这些结果表明，通过人工神经网络形式化是数学自动形式化的一种有前途的方法。我们提出了几个案例研究来说明我们的结果。
URL
https://arxiv.org/abs/1805.06502
