First Neural Conjecturing Datasets and Experiments
First Neural Conjecturing Datasets and Experiments
复制标题
第一个神经推测数据集和实验
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Jan Jakubuv
中科院分区：
文献类型：
--
作者：
J. Urban;Jan Jakubuv
我们描述了几个数据集和通过神经方法创建猜想的第一个实验。数据集基于以多种形式处理的 Mizar 数学库以及 MPTP 系统从中提取的问题，并由 E 证明器使用 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.