Source-linked AI summary
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
TL;DR
The paper asks how to automate part of mathematical formalization, framing it as translation from informal LaTeX into formal Mizar statements. It evaluates neural translation models and datasets, including supervised type elaboration; on the synthetic data, supervised NMT outperforms the unsupervised models across metrics.
Problem
Formalizations are still produced manually by a small expert community, motivating ways to automate parts of the process by translating informal mathematical LaTeX into formal statements.
Source: §1 · p. 1Method
The authors evaluate supervised NMT, unsupervised translation, and XLM on four datasets, and integrate soft type elaboration into supervised translation.
Source: §1 · p. 2, §7 · p. 12Results
On the synthetic dataset, NMT consistently outperformed UNMT and XLM across metrics, while on non-aligned ProofWiki data XLM generally outperformed UNMT except on perplexity.
Source: §4 · p. 8Takeaways & Limitations
The authors describe autoformalization as a promising direction and identify joint embedding of proof-assistant libraries as a way to explore increasing formal data.
Source: §7 · pp. 12–13The authors identify the limited availability of relevant datasets as a major issue for autoformalization research.
Source: §7 · p. 13
Abstract
from arXiv · showhide
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.
1 Introduction
The paper frames autoformalization as translating informal mathematical LaTeX into formal Mizar statements, using neural machine translation as an exploratory route toward automating part of formalization. It introduces three established translation models, four datasets, and a supervised type-elaboration experiment.
1 Introduction
- Autoformalization targets the gap between growing mathematics and manually produced formalizations by translating informal mathematical sentences into formal statements that could support later proof-assistant formalization.The authors propose treating this as a language-translation problem rather than tackling the full human reasoning process at once.Source: §1 · p. 1
- The experiments compare Luong et al.’s supervised NMT with Lample et al.’s unsupervised model and XLM, which adds cross-lingual pretraining.The paper extends NMT with type elaboration and treats XLM as an improved UNMT model.Source: §1 · p. 2
- The translation task maps LaTeX mathematical sentences to Mizar statements, using aligned data for supervised learning and non-aligned corpora for unsupervised learning.The authors prepared four datasets, including three LaTeX–Mizar corpora and a Mizar–TPTP dataset.Source: §1 · p. 2
- The paper evaluates preliminary translation experiments with BLEU, perplexity, edit-distance distributions, and visual comparisons, then discusses their limitations.A separate experiment integrates a type-elaboration mechanism with supervised NMT.Source: §1 · p. 2
2 Informal-To-Formal Datasets
The authors prepare four datasets for experiments translating between mathematical LaTeX and Mizar, selecting Mizar for its library and suitability for their exploration. The datasets include a large synthetic aligned corpus, manually aligned ProofWiki data, and a Mizar–TPTP corpus for testing type elaboration.
2 Informal-To-Formal Datasets
- The Mizar Mathematical Library’s size motivated the choice of Mizar, but the authors present it as expedient for testing NMT, not as superior to other proof assistants.They report more than 55,000 theorem statements and more than 3 million lines of code in the MML.Source: §2 · pp. 2–3
- Mizar’s Tarski–Grothendieck foundation was considered suitable for describing large categorical notions, while the authors also valued readability and ASCII-based text.They explicitly describe these non-size-based selection reasons as simple and speculative.Source: §2 · p. 3
2.1 The Synthetic LaTeX — Mizar Dataset
- Directly building aligned LaTeX–Mizar data from mathematical literature was considered too costly because parsing and preparing aligned corpora require substantial effort.The authors therefore used a tool that generates artificial LaTeX from Mizar statements as an initial workaround.Source: §2.1 · p. 3
- The synthetic dataset contains one million aligned LaTeX–Mizar sentence pairs generated with a tool that traces output sentences back to Mizar statements.The tool applies article-specific translation patterns and handles issues such as parentheses, conjunctive formulas, and typesetting.Source: §2.1 · pp. 3–4
- Because its sentences are deterministically generated, the synthetic corpus is grammatical but artificial, with a smaller vocabulary that weakens generalization.The authors describe algorithmically generated informal data as a temporary workaround for the data-collection problem.Source: §2.1 · p. 4
2.2 The ProofWiki — Mizar Datasets
- The authors also require a smaller aligned corpus for validating and testing unsupervised models, with both languages drawn from the same topic realm as their monolingual corpora.Their ProofWiki datasets provide aligned theorem statements alongside unaligned monolingual corpora.Source: §2.2 · p. 4
- The ProofWiki–Mizar datasets use monolingual LaTeX and Mizar corpora plus 470 manually aligned theorem statements, all in point-set topology and lattice theory.A second version restricts the monolingual corpora to those topics; the datasets are intended to support experiments with unsupervised models.Source: §2.2 · p. 4
2.3 The Mizar — TPTP Dataset
- Because Mizar’s closed-source engine and environment requirements make automated compilation difficult, the authors use supervised NMT to translate Mizar statements into TPTP formulas for type elaboration.The aligned Mizar–TPTP corpus is generated with the MPTP toolchain.Source: §2.3 · p. 4
3 Neural Machine Translation Models
The section introduces recurrent and Transformer-based neural machine translation, then describes supervised NMT and unsupervised UNMT and XLM approaches. Their training differs in architecture, data alignment, and how they learn representations.
3.1 Brief Overview
- The overview connects recurrent NMT advances to Transformer-based UNMT and XLM, with XLM extending UNMT using BERT-style pretraining.The account highlights gating, LSTM, bidirectional encoding, and attention in RNN-based translation before describing the later models.Source: §3.1 · p. 6
3.2 RNN-Based NMT
- NMT uses an encoder-decoder with attention; greedy decoding is used for model comparisons, while beam search is reserved for data augmentation.At inference, the encoder passes a hidden vector to the decoder, which generates the target one word at a time.Source: §3.2 · p. 7
3.3 UNMT
- UNMT keeps bilingual word representations fixed, initializes a shared encoder and two decoders through denoising, then alternates back-translation training in both language directions.The experiments use a Transformer architecture for more efficient GPU training.Source: §3.3 · p. 7
3.4 XLM
- XLM differs from UNMT by pretraining its word embeddings and using masked language modeling before back translation fine-tunes the encoders and decoders.In its masking procedure, each word has a 15% selection chance; selected words are masked 80% of the time, replaced randomly 10%, or unchanged 10%.Source: §3.4 · p. 8
4 Experiments and Results
The experiments evaluate translation with BLEU, perplexity, and edit distance. NMT performs best on the aligned synthetic dataset, while comparisons on non-aligned data favor XLM over UNMT in most metrics, with an exception for perplexity.
Evaluation metrics
- BLEU, perplexity, and Levenshtein edit distance assess translation quality, with higher BLEU but lower perplexity and edit distance indicating better scores.Edit distance counts insertions, deletions, and substitutions relative to the reference sentence.Source: §4 · p. 8
Evaluation limitation
- The three evaluation metrics measure syntactic closeness rather than semantic equivalence, so a syntactically small difference can change a formal statement’s meaning.The paper gives a missing “not” as an example of a meaning-changing difference.Source: §4 · p. 8
Results
- On the synthetic dataset, NMT outperforms UNMT and XLM across all metrics, and XLM outperforms UNMT.The comparison uses a 2000-sample evaluation; Table 7 presents the model metrics.Source: §4 · p. 8, Table 7 · p. 8
- On non-aligned datasets, XLM generally performs better than UNMT except on perplexity; both models score better on the topology subset than on the full ProofWiki–Mizar dataset.The paper attributes the topology/full-dataset comparison to the aligned corpus focusing on topology and lattice theory.Source: §4 · p. 8
5 Data Augmentation Using Type Elaboration
The section introduces a feedback loop that uses Mizar-style type elaboration to expand supervised translation data, with soft-type inference supplying missing type information. Across the first three iterations, exact matches nearly doubled, while later iterations showed diminishing improvement and signs of overfitting.
5.4 Data Augmentation Pipeline
- The feedback loop uses beam-search translations that can be deterministically transformed back into source sentences to add training pairs and retrain the model.The toolchain converts prefix-format inputs through TPTP-THF for elaboration, then back-translates elaborated formulas into Mizar statements.Source: §5 · p. 8, §5.4 · p. 11, Figure 2 · p. 11
5 Data Augmentation Using Type Elaboration
- Type elaboration is integrated into a supervised NMT feedback loop as a data-augmentation mechanism for improving translation syntax.The section frames the loop as a way to teach the model correct syntactic formats through recovered sentence pairs.Source: §5 · pp. 8–9
5.1 Mizar Soft Type System
- Mizar soft types are predicates, and deterministic type inference avoids needless search-space expansion when a term can acquire a type through multiple derivations.For example, a sum of n copies of 1 can be inferred real either through real addition or through natural-number addition followed by the type hierarchy.Source: §5.1 · p. 9
5.2 Mizar Soft Type Inference
- Soft-type inference recursively computes a ground term’s types from its arguments and function-type formulas, then widens types using type-hierarchy formulas.The described mechanism is a simplification: the Elaborator also handles redefinitions and requires some equational reasoning, whose details are omitted.Source: §5.2 · p. 10
5.3 Elaborator — Patterns and Elaboration
- The Elaborator turns pseudo-terms and pseudo-formulas into formulas by traversing bottom-up, using inferred soft types to satisfy pattern constraints and fill missing arguments.In the example, typing assumptions for a function and its argument determine the two extra arguments required by function application.Source: §5.3 · pp. 10–11
5.5 Experiments
- Iterations 1–3 increased exact matches by 100% with only a 16.41% increase in training data; improvement later ceased to be significant and the model began to overfit.The edit-distance distribution shifted toward exact matches in the first three iterations, then flattened.Source: Figure 4 · p. 12, §5.5 · p. 12
6 Related Works
Related work traces the vision of automating mathematical formalization from early proposals to systems for translating mathematical text. The authors connect their effort to the QED vision and express hope that neural machine learning can advance it.
6 Related Works
- Wang’s 1954 work hinted at automating mathematical formalization, and the QED Manifesto later set out a vision of a computer-based database of formalized mathematical knowledge.Source: §6 · p. 12
- Zinn (2004) used domain discourse theory to parse a number theory textbook, while Naproche invented controlled natural language resembling ordinary natural-language text that is compilable.Source: §6 · p. 12
- The authors identify their goal with the QED Manifesto’s vision [2] and hope neural network-based machine learning will help realize it.Source: §6 · p. 12
7 Conclusion
The paper reports initial experiments in translating LaTeX mathematics into proof-assistant statements and integrates soft type elaboration into supervised data augmentation. The authors identify relevant data availability as a continuing constraint and note that their datasets use sequences rather than richer formula features.
7 Conclusion
- The paper proposes autoformalization experiments with unsupervised translation and integrates soft type elaboration for data augmentation in supervised learning.Source: §7 · p. 12
- The datasets use sequences only; syntax trees and required environment declarations have not been tested as additional input features.Source: §7 · p. 12
- Relevant datasets remain a major constraint: abundant mathematics literature is not yet readily combined with the ITP expertise and data needed for autoformalization.The authors call for more high-quality data and more comprehensive experiments.Source: §7 · pp. 12–13