The authors constructed a large aligned corpus by informalizing Mizar statements into LaTeX-like mathematical text and trained sequence-to-sequence translation models to reconstruct the formal language.
Qingxiang Wang, Cezary Kaliszyk and Josef Urban trained neural machine-translation models on aligned informalized-LaTeX and formal Mizar statements. The paper reported 65.73% exact generation for the best model configuration on its inference data, with the union of evaluated models covering 79.17%.
The authors constructed a large aligned corpus by informalizing Mizar statements into LaTeX-like mathematical text and trained sequence-to-sequence translation models to reconstruct the formal language. The study evaluated multiple neural translation configurations and used case studies to examine which mathematical structures could be recovered correctly.
Autoformalization is a key interface problem between human mathematical writing and machine-checkable formal mathematics. This work showed, before the modern LLM era, that learned translation could make the informal-to-formal direction a concrete empirical research problem rather than only a long-term aspiration.
Significance rationale: These experiments were an early neural autoformalization milestone: instead of assuming a formal theorem statement as input, a neural machine-translation model was trained to map natural-looking mathematical text into Mizar statements. The work became an explicit predecessor in later autoformalization research, including the 2022 large-language-model route.
—
The arXiv and CICM research records establish the neural informal-to-formal translation experiments and the reported Mizar results. E2 records a public research record and does not imply independent reproduction or semantic validation of every generated statement.
No corrections recorded.
