# Multilingual Mathematical Autoformalization

Preprint · Albert Q. Jiang, Wenda Li, Mateja Jamnik

- Archive id: arxiv:2311.03755
- Published: 2023-11-07
- arXiv: https://arxiv.org/abs/2311.03755
- Citations: 1
- Source URL: https://arxiv.org/abs/2311.03755
- PDF: https://arxiv.org/pdf/2311.03755
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.