因斯布鲁克大学 发布 HOLSTEP 数据集, 应用在 逻辑定理证明、机器学习 领域

因斯布鲁克大学 本次发布的数据集 HOLSTEP, HOLSTEP数据集由因斯布鲁克大学开发，专注于高阶逻辑定理证明，包含2,013,046个训练样本和196,030个测试样本，源自11,400个证明。数据集涵盖基础数学、分析、三角学及图等数据结构的推理。创建过程涉及从HOL Light定理证明器中提取证明步骤，并进行离线处理以提取依赖关系和标记训练测试样本。该数据集旨在通过机器学习技术改进定理证明策略，特别是在交互式定理证明系统中提高自动化证明搜索的效率。

查看HOLSTEP

关于 因斯布鲁克大学 , 因斯布鲁克大学是奥地利的一所公立大学，成立于1669年，位于因斯布鲁克市。该大学在自然科学、社会科学和人文科学等多个领域都有卓越的研究和教学成果。

关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。