神经推测数据集

神经推测数据集是由捷克信息学、机器人学和控制论研究所创建，用于通过神经网络方法生成数学猜想。该数据集包含四种不同的数据格式，总计处理了28271个Mizar定理，数据量从53MB到658MB不等。创建过程涉及使用MPTP系统和E prover进行定理证明，并采用Transformer架构特别是GPT-2实现进行推测实验。该数据集主要应用于自动推理和理论探索，旨在解决自动化生成数学猜想的问题。

The Neural Conjecture Dataset was created by the Institute of Informatics, Robotics and Cybernetics of the Czech Republic for generating mathematical conjectures via neural network approaches. This dataset includes four distinct data formats, with a total of 28,271 Mizar theorems processed, and its size ranges from 53 MB to 658 MB. The development process involved theorem proving using the MPTP system and E Prover, as well as conjecture generation experiments implemented with the Transformer architecture, specifically the GPT-2 model. This dataset is primarily utilized in automated reasoning and theoretical exploration, with the goal of addressing the challenge of automated mathematical conjecture generation.