Multilingual Mathematical Autoformalization

TL;DR

This paper introduces MMA, a large multilingual dataset for autoformalization, enabling language models to translate formal mathematical statements into informal language, significantly improving their performance on benchmarks.

Contribution

The creation of MMA, a novel multilingual, multi-domain dataset for autoformalization, and demonstrating its effectiveness in enhancing language model performance.

Findings

Fine-tuned models achieve 16-18% acceptable statements on benchmarks.

Base models had 0% acceptable statements without fine-tuning.

Multilingual training improves monolingual autoformalization capabilities.

Abstract

Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create $\texttt{MMA}$, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on $\texttt{MMA}$ produce $16-18\%$ of statements acceptable with minimal corrections on the $\texttt{miniF2F}$ and $\texttt{ProofNet}$ benchmarks, up from $0\%$ with the base model. We demonstrate that fine-tuning on multilingual formal data results in more capable autoformalization models even when deployed on monolingual tasks.