arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2005.14664cs.AIcs.LGcs.LOcs.NEcs.SC
收藏

第一个神经猜想数据集和实验

First Neural Conjecturing Datasets and Experiments

Czech Institute of Informatics, Robotics and Cybernetics(捷克信息学、机器人学与控制论研究所)

Josef Urban, Jan Jakubův

摘要:

我们描述了几个数据集和第一个实验,通过神经方法创建图形。这些数据集基于Mizar数学库,以多种形式进行处理,并通过MPTP系统从中提取问题,并通过E prover使用ENIGMA指南进行证明。编程实验使用了Transformer架构,特别是它的GPT-2实现。

英文摘要:

We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms and the problems extracted from it by the MPTP system and proved by the E prover using the ENIGMA guidance. The conjecturing experiments use the Transformer architecture and in particular its GPT-2 implementation.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑