iset.mm
收藏arXiv2025-09-30 收录
下载链接：
https://github.com/princeton-vl/MetaGen
下载链接
链接失效反馈官方服务：
资源简介：
该数据集对直觉逻辑进行了形式化，并包含了463个公理和8916个定理，这些定理相应地对应于8916个证明任务。在生成合成数据方面，该数据集还包括了100万个独特的合成定理。在规模上，数据集分为8916个证明任务，其中7123个用于训练，890个用于验证，903个用于测试。该数据集的任务是自动定理证明。
This dataset formalizes intuitionistic logic, containing 463 axioms and 8916 theorems, each of which corresponds to a unique proof task. For synthetic data generation, the dataset also includes 1,000,000 unique synthetic theorems. The dataset consists of 8916 proof tasks in total, which are split into three subsets: 7123 for training, 890 for validation, and 903 for testing. The core task of this dataset is automated theorem proving.
提供机构：
Metamath
