论文标题
第一个神经猜想的数据集和实验
First Neural Conjecturing Datasets and Experiments
论文作者
论文摘要
我们描述了几个数据集和第一个实验，并通过神经方法创建猜想。该数据集基于以几种形式处理的Mizar数学库，以及MPTP系统从中提取的问题，并使用Enigma指南证明了E贵族。猜想实验使用了变压器体系结构，尤其是其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.
