Multilingual Mathematical Autoformalization

要約

自動形式化は、自然言語素材を機械検証可能な形式に変換するタスクです。
自動形式化研究の進歩は、同じ本質を表現する非公式と公式のペアで構成される大規模なデータセットの欠如によって妨げられています。
既存の方法では、小さなコーパスを手動でキュレーションするか、大規模な言語モデルでの少数ショット学習を使用することで、この課題を回避する傾向があります。
しかし、これらの方法にはデータが不足しており、形式的な言語を習得するのが難しいという問題があります。
この研究では、言語モデルを使用して逆方向、つまり正式な数学的言語から翻訳することにより、非公式と公式のペアの大規模で柔軟な多言語およびマルチドメインのデータセットである $\texttt{MMA}$ を作成します。
ステートメントを対応する非公式なステートメントに変換します。
実験によると、$\texttt{MMA}$ で微調整された言語モデルは、$\texttt{miniF2F}$ および $\texttt{ProofNet}$ ベンチマークで最小限の修正で許容可能なステートメントの $16-18\%$ を生成し、
基本モデルでは $0\%$。
多言語形式データを微調整すると、単言語タスクに展開した場合でも、より有能な自動形式化モデルが得られることを実証します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google