UDACA/Isa-AF-MMA

该数据集结合了DQ Round Trip Problem Selection电子表格的所有条目，并移除了除正式和非正式列之外的所有列，同时添加了一个文本列。此外，数据集还结合了来自《Multilingual Mathematical Autoformalization》数据集的Isabelle训练和验证集，并以相同的格式添加了文本列。数据字段包括正式声明、非正式声明和文本列，其中文本列包含样本的结构化信息。数据集的语言为英语。该数据集结合了DQ Round Trip Problem Selection电子表格的所有条目，并移除了除正式和非正式列之外的所有列，同时添加了一个文本列。此外，数据集还结合了来自《Multilingual Mathematical Autoformalization》数据集的Isabelle训练和验证集，并以相同的格式添加了文本列。数据字段包括正式声明、非正式声明和文本列，其中文本列包含样本的结构化信息。数据集的语言为英语。

原始信息汇总

数据集概述

本数据集整合了DQ Round Trip Problem Selection电子表格（链接：https://docs.google.com/spreadsheets/d/1dEWWzjuEXwf9s4II0CixH4sqopc1flIMFx19UjHiyNU/edit?usp=sharing&resourcekey=0-_G7oxmbh7szV5jx-HxhepQ）的所有条目，移除了除正式和非正式列之外的所有列，并添加了一个文本列。此外，还合并了Multilingual Mathematical Autoformalization数据集中的Isabelle训练和验证集，同样添加了一个格式相同的文本列。

数据字段

• Formal statement: 在Isabelle中的正式声明
• Informal statement: 与正式声明等价的非正式语言描述
• text: 文本条目包含以下结构：The Formal Statement is: ______ The Informal Statement is: _______

语言

• 英语（en）