Elamur Research⌕
☰
home / papers / 2018 / First Experiments with Neural Translation of Informal to Formal Mathematics

First Experiments with Neural Translation of Informal to Formal Mathematics

Paper · 2018 · Qingxiang Wang, Cezary Kaliszyk and Josef Urban

Summary

Wang, Kaliszyk and Urban study autoformalization: automatically converting mathematics written in LaTeX into a machine-checkable formal language, here Mizar. No large corpus pairs informal and formal statements, so the authors built one synthetically through informalization. They used Grzegorz Bancerek's long-developed Mizar-to-LaTeX translation, which produces the journal Formalized Mathematics, and modified its XSL stylesheets so that proof-internal formulas are also rendered. This yielded roughly a million aligned, tokenized LaTeX–Mizar statement pairs. They then trained Luong et al.'s NMT implementation of the seq2seq model with RNN cells and attention, varying hyperparameters such as unit count, depth, optimizer, residual and bidirectional layers, and attention type. The best configuration exactly reproduced the target Mizar statement for about two thirds of the test set, and pooling many models raised exact coverage further. The authors describe this as the first use of neural networks for formalizing mathematics. The results suggest that neural translation can learn nontrivial informal-to-formal mappings, which makes it a promising route toward machine understanding of mathematical texts.

Key points

  • The corpus contains 947,231 aligned Mizar–LaTeX training pairs and 105,247 test pairs, all generated from the Mizar library via Bancerek's translation tools.
  • The best single model (1024 units) produced identical statements for 65.73% of test pairs (BLEU 61.6, about 11 hours of training). That rose to 74.58% when outputs within one token edit of the target were counted.
  • The union of all 39 trained models gave exact translations for 79.17% of test pairs. Greedy covers of 5 and 10 models reached 74.50% and 76.89%.
  • In the reverse direction (Mizar → LaTeX), a model with 512 units, bidirectional layers and scaled Luong attention matched the target exactly on 51.61% of test pairs.
  • Planned future work includes:
    • semantic checking via MPTP/TPTP and ATP systems, since many outputs counted as wrong may be valid synonymous Mizar formulations;
    • extension to full proofs, ProofWiki and eventually arbitrary LaTeX texts.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Machine translation · 1,109 works

Cite

Cite as Qingxiang Wang, Cezary Kaliszyk and Josef Urban. 2018. First Experiments with Neural Translation of Informal to Formal Mathematics. arXiv:1805.06502.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1805.06502 · arXiv 1805.06502

@misc{wang2018first,
  title = {{First Experiments with Neural Translation of Informal to Formal Mathematics}},
  author = {Qingxiang Wang, Cezary Kaliszyk and Josef Urban},
  year = {2018},
  doi = {10.48550/arxiv.1805.06502},
  eprint = {1805.06502},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1805.06502}
}

References

23 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. G. Bancerek. Automatic translation in formalized mathematics. Mechanized Mathematics and Its Applications, 5(2):19–31, 2006. find
  2. G. Bancerek, C. Bylinski, A. Grabowski, A. Kornilowicz, R. Matuszewski, A. Naumowicz, K. Pak, and J. Urban. Mizar: State-of-the-art and beyond. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, volume 9150 o… find
  3. G. Bancerek and P. Carlson. Mizar and the machine translation of mathematics documents. Available online at http://www.mizar. org/ project/ banc_ carl93. ps , 1994. ↗
  4. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  5. K. Cho, B. van Merriënboer, Ç. Gülçehre, D. Bahdanau, F. Bougares, H. Schwenk, and Y. Bengio. Learning phrase representations using rnn encoder–decoder for statistical machine translation. In Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 17…
  6. G. Cybenko. Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems, 2(4):303–314, Dec 1989. find
  7. I. Goodfellow, Y. Bengio, and A. Courville. Deep Learning. MIT Press, 2016. http://www.deeplearningbook.org. ↗
  8. T. Hales. Dense Sphere Packings: A Blueprint for Formal Proofs, volume 400 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2012. find
  9. T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, and R. Zumkeller. A formal proof of the Kepler conje… — A formal proof of the Kepler conjecture
  10. K. Hornik. Approximation capabilities of multilayer feedforward networks. Neural Netw., 4(2):251–257, Mar. 1991. find
  11. C. Kaliszyk, J. Urban, and J. Vyskočil. Automating formalization by statistical and semantic parsing of mathematics. In M. Ayala-Rincón and C. A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, volume 10499 of LNCS, pages 12–27. Springer, 2017. find
  12. C. Kaliszyk, J. Urban, and J. Vyskočil. Learning to parse on aligned corpora (rough diamond). In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pages 227–233. Springer, 2015. find
  13. C. Kaliszyk, J. Urban, J. Vyskočil, and H. Geuvers. Developing corpus-based translation methods between informal and formal mathematics: Project description. In S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, editors, Intelligent Computer Mathematics - International Conference, C… find
  14. A. Krizhevsky, I. Sutskever, and G. E. Hinton. ImageNet classification with deep convolutional neural networks. In F. Pereira, C. J. C. Burges, L. Bottou, and K. Q. Weinberger, editors, Advances in Neural Information Processing Systems 25, pages 1097–1105. Curran Associates, Inc., 2012.
  15. M. Luong, E. Brevdo, and R. Zhao. Neural machine translation (seq2seq) tutorial. https://github.com/ tensorflow/ nmt , 2017. ↗
  16. C. J. Maddison, A. Huang, I. Sutskever, and D. Silver. Move evaluation in Go using deep convolutional neural networks. CoRR, abs/1412.6564, 2014. — [arXiv:1412.6564](https://arxiv.org/abs/1412.6564) find
  17. G. Neubig. Neural machine translation and sequence-to-sequence models: A tutorial. CoRR, abs/1703.01619, 2017. find
  18. C. Olah. Understanding LSTM networks. http://http://colah.github.io/posts/2015-08-Understanding-LSTMs/. find
  19. K. Papineni, S. Roukos, T. Ward, and W. Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, pages 311–318. ACL, 2002.
  20. I. Sutskever, O. Vinyals, and Q. V. Le. Sequence to sequence learning with neural networks. In Proceedings of the 27th International Conference on Neural Information Processing Systems - Volume 2, NIPS’14, pages 3104–3112, Cambridge, MA, USA, 2014. MIT Press.
  21. A. Trybulec and P. Rudnicki. A collection of TeXed Mizar abstracts. Available online at http://www.mizar. org/ project/ TR-89-18. pdf , 1989. ↗
  22. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  23. J. Urban and J. Vyskočil. Theorem proving in large formal mathematics as an emerging AI field. In M. P. Bonacina and M. E. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William McCune, volume 7788 of LNAI, pages 240–257. Springer, 2013. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/