casey-martin/multilingual-mathematical-autoformalization

该数据集包含并行的数学陈述，输入为非正式的自然语言证明，输出为Lean或Isabelle中的形式化证明。数据集可用于训练模型将数学陈述形式化为可验证的证明，这是一种机器翻译的形式。数据集通过创建大规模、多语言、多领域的非正式-正式对，解决了自动形式化研究中的数据稀缺和形式语言获取困难的问题。实验表明，在MMA数据集上微调的语言模型在miniF2F和ProofNet基准测试中，能够产生16-18%的陈述，这些陈述在最小修正下是可接受的，而基础模型的这一比例为0%。此外，微调多语言形式数据的结果表明，即使在单语言任务中部署，也能产生更强大的自动形式化模型。

原始信息汇总

多语言数学自动形式化数据集

数据集配置

• 默认配置
  • 训练集: data/*_train.jsonl
  • 验证集: data/*_val.jsonl
  • 测试集: data/*_test.jsonl
• 精简配置
  • 训练集: data/lean_train.jsonl
  • 验证集: data/lean_val.jsonl
  • 测试集: data/lean_test.jsonl
• Isabelle配置
  • 训练集: data/isabelle_train.jsonl
  • 验证集: data/isabelle_val.jsonl
  • 测试集: data/isabelle_test.jsonl

许可

• Apache 2.0

任务类别

• 翻译
• 文本生成

语言

• 英语

标签

• 数学
• 自动形式化
• Lean
• Isabelle

数据集大小

• 100K<n<1M

数据集描述

该数据集包含并行的数学陈述：

1. 输入：自然语言中的非正式证明
2. 输出：对应的Lean或Isabelle形式化

该数据集可用于训练模型如何将数学陈述形式化为可验证的证明，这是一种机器翻译形式。

示例

输入:

• 自然语言陈述: 如果 "r" 是一个有限集，"i" 是 "r" 的一个元素，那么函数 "a" 应用于 "i" 的结果是 "a" 在 "r" 上的多重集范围的一个元素。将自然语言陈述翻译为Isabelle:

输出:

• lemma mset_ran_mem[simp, intro]: "finite r <Longrightarrow> i<in>r <Longrightarrow> a i <in># mset_ran a r"