MPTP large-theory benchmark
收藏arXiv2025-09-30 收录
下载链接：
http://grid01.ciirc.cvut.cz/~mptp/1147/MPTP2/problems_small_consist.tar.gz
下载链接
链接失效反馈官方服务：
资源简介：
该数据集是一个大规模的Mizar40问题基准，用于评估所提出的方法。该数据集涵盖了57880个问题，旨在检验梯度提升和神经引导方法在定理证明任务中的性能表现。
This dataset is a large-scale Mizar40 problem benchmark for evaluating the proposed methods. It contains 57,880 problems, aiming to test the performance of gradient boosting and neuro-guided methods on theorem proving tasks.
提供机构：
MPTP
