UDACA/Split-Isa-AF-MMA
收藏Hugging Face2024-03-17 更新2024-06-11 收录
下载链接：
https://hf-mirror.com/datasets/UDACA/Split-Isa-AF-MMA
下载链接
链接失效反馈官方服务：
资源简介：
该数据集是DQ Round Trip Problem Selection电子表格中每个条目的集合，其中正式和非正式的列被合并，并与来自[*Multilingual Mathematical Autoformalization*](https://arxiv.org/abs/2311.03755)数据集的Isabelle训练和验证集中的正式和非正式声明进行连接。此外，还添加了一个文本列，其格式与原始数据相同。数据集的主要数据字段是`Statement`，它包含Isabelle语言中的非正式或正式声明。
该数据集是DQ Round Trip Problem Selection电子表格中每个条目的集合，其中正式和非正式的列被合并，并与来自[*Multilingual Mathematical Autoformalization*](https://arxiv.org/abs/2311.03755)数据集的Isabelle训练和验证集中的正式和非正式声明进行连接。此外，还添加了一个文本列，其格式与原始数据相同。数据集的主要数据字段是`Statement`，它包含Isabelle语言中的非正式或正式声明。
提供机构：
UDACA
原始信息汇总
数据集概述
数据来源
本数据集整合了DQ Round Trip Problem Selection电子表格（链接：https://docs.google.com/spreadsheets/d/1dEWWzjuEXwf9s4II0CixH4sqopc1flIMFx19UjHiyNU/edit?usp=sharing&resourcekey=0-_G7oxmbh7szV5jx-HxhepQ）中的所有条目，并与Multilingual Mathematical Autoformalization数据集中的Isabelle火车和val集合的正式和非正式声明进行了合并和串联。
数据字段
Statement: 包含非正式声明或Isabelle语言的正式声明。
