IMM project
收藏arXiv2025-09-30 收录
下载链接：
https://github.com/weakmemory/imm
下载链接
链接失效反馈官方服务：
资源简介：
该数据集来自IMM项目，包含了大量由人类编写的定理和证明，专为支持Coq版本8.19而设计。在实验中使用的数据集是300个定理的子集，这些定理的证明过程限制在最多20个策略以内。根据证明过程的长度，该数据集被分为三组，实验旨在评估使用不同方法和模型能够证明多少个定理。该数据集是从一个更大的项目中选取的子集，其规模适中。研究任务是对使用各种模型的Coqpilot在证明定理方面的性能进行评估。
This dataset is derived from the IMM project, which contains a large corpus of human-written theorems and their formal proofs, and is specifically designed to support Coq version 8.19. The subset utilized in the experiments comprises 300 theorems, with each proof script restricted to at most 20 tactics. This dataset is split into three groups based on the length of their proof scripts. The experiment aims to assess how many theorems can be successfully proven using different methods and models. This is a moderately sized subset selected from a larger project. The core research task is to evaluate the theorem-proving performance of Coqpilot across various models.
提供机构：
IMM project team
