Elamur Research⌕
☰
home / papers / 2019 / Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

Paper · 2019 · Qingxiang Wang, Chad Brown, Cezary Kaliszyk et al.

Summary

The paper treats autoformalization, the conversion of human-written mathematics into machine-checkable statements, as a machine translation problem. LaTeX sentences are the source language and Mizar statements are the target. Mizar was chosen mainly because its Mizar Mathematical Library (MML) is the largest formal corpus available, with over 55 thousand theorems and more than 3 million lines. Further reasons are its Tarski-Grothendieck set-theoretic foundation, its ASCII format and its readability. The authors built four informal-to-formal datasets and tested three existing neural translation systems: the supervised NMT of Luong et al., the unsupervised UNMT of Lample et al., and the cross-lingual pretrained XLM. They judged output quality using BLEU, perplexity, edit-distance distributions and manual inspection. Pretraining in XLM gave better results than the original UNMT. To enlarge supervised training data, they also added a custom type-elaboration step to NMT and tested it on a Mizar–TPTP dataset. The work is an exploratory baseline. It shows that neural translation is a feasible starting point and that the scarcity of aligned informal–formal data is the field's central bottleneck.

Key points

  • The four datasets are Synthetic LaTeX — Mizar, ProofWiki — Mizar topology, ProofWiki — Mizar full, and Mizar — TPTP. The first three grow in size and in how closely they resemble natural language.
  • The three models differ in setup:
    • NMT runs on TensorFlow, using a two-layer LSTM encoder-decoder by default.
    • UNMT runs on PyTorch, with RNN or transformer variants and fixed word2vec embeddings.
    • XLM uses BERT-style pretraining, and the authors treat it as an improved UNMT.
  • Type elaboration on pattern formulas serves as data augmentation for supervised NMT. It was tested via Mizar — TPTP because Mizar is not based on type theory, which makes automation harder.
  • Future work includes jointly embedding several proof-assistant libraries to enlarge the formal data.
  • The paper appeared at CPP '20. Exact scores were in the omitted middle part of the provided text and should be checked in the full paper.

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🎓University of WarsawWarsaw · Poland14 works · 774 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 2Research subjects and languages the work is about.Machine translation · 1,109 worksReasoning · 1,948 works

Cite

Cite as Qingxiang Wang, Chad Brown, Cezary Kaliszyk and Josef Urban. 2019. Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. arXiv:1912.02636.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3372885.3373827 · arXiv 1912.02636

@misc{wang2019exploration,
  title = {{Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar}},
  author = {Qingxiang Wang, Chad Brown, Cezary Kaliszyk and Josef Urban},
  year = {2019},
  doi = {10.1145/3372885.3373827},
  eprint = {1912.02636},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3372885.3373827}
}

References

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

  1. Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenber… find
  2. Anonymous. 1994. The QED Manifesto. In Proceedings of the 12th International Conference on Automated Deduction (CADE-12). Springer-Verlag, London, UK, UK, 238–251. http://dl.acm.org/citation.cfm?id= 648231.752823 ↗
  3. Mikel Artetxe, Gorka Labaka, Eneko Agirre, and Kyunghyun Cho. 2017. Unsupervised Neural Machine Translation. CoRR abs/1710.11041 (2017). https://doi.org/10.18653/v1/D18-1399 arXiv:1710.11041 ↗
  4. Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. 2015. Neural Machine Translation by Jointly Learning to Align and Translate. In 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, Yoshua Bengio and Yann LeCun (Eds.…
  5. Grzegorz Bancerek. 2006. Automatic Translation in Formalized Mathematics. Mechanized Mathematics and Its Applications 5, 2 (2006), 19–31. find
  6. Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Ko-rnilowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 2018. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. J. Autom. Reasoning 61, 1-4 (2018), 9–32. https://doi.org/10.1007/s10817-017-9440-6 — [doi:10.1007/s10817-017-9440-6](https://doi.org/10.1007/s10817-017-9440-6) ↗
  7. Grzegorz Bancerek and Patricia Carlson. 1994. Mizar and the Machine Translation of Mathematics Documents. Available online at http://www.mizar.org/ project/ banc_carl93.ps (1994). ↗
  8. Grzegorz Bancerek, Adam Naumowicz, and Josef Urban. 2018. System Description: XSL-Based Translator of Mizar to LaTeX. In Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (Lecture Notes in [22] Thomas Hales, Mark Adams, G… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/