Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

Abstract

In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-written mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language. We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages. To train these models we also prepared four informal-to-formal datasets. We compare and analyze our results according to whether the model is supervised or unsupervised. In order to augment the data available for auto-formalization and improve the results, we develop a custom type-elaboration mechanism and integrate it in the supervised translation.

arXiv commentThe 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

References in corpus (12)

• Distributed Representations of Words and Phrases and their Compositionality
• Neural Machine Translation by Jointly Learning to Align and Translate
• Sequence to Sequence Learning with Neural Networks
• Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling
• Convolutional Sequence to Sequence Learning
• Cross-lingual Language Model Pretraining
• Enriching Word Vectors with Subword Information
• Unsupervised Statistical Machine Translation
• Phrase-Based & Neural Unsupervised Machine Translation
• Gradient Descent Finds Global Minima of Deep Neural Networks
• Representation Benefits of Deep Feedforward Networks
• Unsupervised Neural Machine Translation

Cited by in corpus (7)

• Mathematical Reasoning via Self-supervised Skip-tree Training
• NaturalProofs: Mathematical Theorem Proving in Natural Language
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• A Study of Continuous Vector Representationsfor Theorem Proving
• Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Markets
• Improving the Diproche CNL through Autoformalization via Large Language Models
• Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students