Multilingual Mathematical Autoformalization

📄 arXiv: 2311.03755v2 📥 PDF

作者: Albert Q. Jiang, Wenda Li, Mateja Jamnik

分类: cs.CL, cs.LG

发布日期: 2023-11-07 (更新: 2023-11-09)

💡 一句话要点

提出MMA数据集以解决自动形式化中的数据稀缺问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动形式化 数据集构建 多语言处理 机器学习 数学推理

📋 核心要点

  1. 现有自动形式化方法因缺乏足够的非正式-正式对数据集而受到限制，导致数据稀缺和形式语言获取困难。
  2. 本文提出MMA数据集，通过反向翻译生成非正式-正式对，解决了数据稀缺问题，并提升了模型的自动形式化能力。
  3. 实验结果显示，基于MMA微调的模型在miniF2F和ProofNet基准测试中，接受的语句比例从0%提升至16-18%。

📝 摘要（中文）

自动形式化是将自然语言材料翻译为机器可验证形式的任务。现有研究因缺乏足够的非正式-正式对数据集而受限，现有方法通常通过手动整理小型语料库或使用大语言模型的少量学习来规避这一挑战。然而，这些方法面临数据稀缺和形式语言获取困难的问题。本文创建了MMA，一个大型、灵活的多语言多领域非正式-正式对数据集，通过使用语言模型反向翻译，即从正式数学语句到相应的非正式语句。实验表明，基于MMA微调的语言模型在miniF2F和ProofNet基准测试中，接受的语句比例提高了16-18%，而基础模型为0%。我们证明了在多语言正式数据上微调可以使自动形式化模型在单语任务中表现更佳。

🔬 方法详解

问题定义：本文旨在解决自动形式化中缺乏大规模非正式-正式对数据集的问题。现有方法依赖于小型语料库或少量学习，导致数据稀缺和形式语言获取困难。

核心思路：论文的核心思路是创建MMA数据集，通过语言模型反向翻译正式数学语句为非正式语句，从而生成丰富的非正式-正式对数据。这样的设计旨在克服现有方法的数据限制，提供更广泛的训练数据。

技术框架：整体架构包括数据集的构建和模型的微调两个主要阶段。首先，通过语言模型生成非正式语句，然后使用这些数据对模型进行微调，以提高其在自动形式化任务中的表现。

关键创新：最重要的技术创新在于MMA数据集的创建，它通过反向翻译生成大量非正式-正式对，显著提升了模型的训练数据量。这一方法与传统的手动整理或少量学习方法本质上不同，提供了更为高效的数据生成途径。

关键设计：在模型微调过程中，采用了特定的损失函数以优化生成语句的准确性，并对网络结构进行了调整，以适应多语言和多领域的需求。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，基于MMA微调的语言模型在miniF2F和ProofNet基准测试中的接受语句比例从0%提升至16-18%，证明了多语言正式数据的微调对模型能力的显著提升。

🎯 应用场景

该研究的潜在应用领域包括教育、自动化证明、数学软件开发等。通过提高自动形式化的能力，MMA数据集能够帮助开发更智能的教育工具和数学推理系统，推动相关领域的研究与应用。未来，该方法可能会影响更多语言和领域的自动形式化研究。

📄 摘要（原文）

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.