{'fraction_non_alphanumeric': 0.030002006823198875, 'fraction_numerical': 0.026289383905277946, 'mean_word_length': 4.685681688533942, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
First Neural Conjecturing Datasets and Experiments

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.


Introduction and Related Work
Automated creation of suitable conjectures is one of the hard problems in automated reasoning over large mathematical corpora. This includes tasks such as (i) conjecturing suitable intermediate lemmas (cuts) when proving a harder conjecture, and (ii) unrestricted creation of interesting conjectures based on the previous theory (i.e., theory exploration). Starting with Lenat's AM [10], several systems such as the more specialized Graffitti by Fajtlowicz [4], and Colton's HR [3] have been developed, typically using heuristics for theory exploration or limited brute-force enumeration, controlled e.g. by the type system [7].
Our motivation is the work of Karpathy 1 with recurrent neural networks (RNNs). One of his experiments used the Stacks project, generating LaTeXstyle pseudo-mathematics that looked quite credible to non-experts. We have repeated these experiments over the Mizar library using Karpathy's RNNs in 2016, but the results did not seem convincing. The neural methods have however improved since, coming up with stronger methods and systems such as attention, transformer and GPT-2 [12]. The experiments described here started by testing GPT-2 on the Mizar library, gradually producing several more datasets.
Related work includes research on the informal-to-formal grammar-based and neural translation [9,8,17,16]. There it was found that PCFGs and RNNs with attention work well on some informal-to-formal datasets, can learn analogies from the data, and can be used to produce multiple formal outputs of which some are new provable conjectures. In [16] we use this together with type checking to set up a data-augmentation loop between the neural learner and the type-checker. Such learning-reasoning loops are also planned for the datasets presented here. Similar experiments are done in [6] and by Chvalovský 2 . Gauthier has been working on term synthesis using Monte-Carlo Tree Search and reinforcement learning with semantic feedback [1,5].

Datasets
The datasets for neural conjecturing are available from our web page 3 . We have so far experimented with the following data: 1. All Mizar articles (MML version 1147), stripped of comments and concatenated together 4 . This is 78M of uncompressed text. 2. Text version of the HTML export [14] of the MML articles 5 . This unpacks to 156MB. It additionally contains disambiguation features such as full types of variables, full names of theorems and the thesis is printed after every natural deduction step. This seems useful for neural conjecturing because the context is repeated more often. 3. Tokenized TPTP proofs 6 of 28271 Mizar theorems translated by the MPTP system [15]. The proofs are produced by the E prover [13] equipped with recent ENIGMA guidance [2]. This unpacks to 658MB. 4. A subselection of the used Mizar premises from the 28271 proofs printed in prefix notation 7 . These files always start with the conjecture, and the premises are printed in the order in which E used them in its proof. This unpacks to 53MB.

Experiments
The basic experiment for each dataset consists of training the smallest (117M parameters) version of GPT-2 on a NVIDIA GeForce GTX 1080 GPU with 12GB RAM, producing random unconditioned samples during the training. The produced samples and the most recent trained models are available from our web page 8 . The published models can be used for conditional and unconditional generation of Mizar-like texts, proofs and premise completion. The samples contain megabytes of examples of what can be generated and how the generated texts improve during the training. The training on the third dataset was stopped early. The large number of redundant tokens such as brackets and commas led us to produce the fourth dataset that uses the punctuation-free prefix notation and much shorter summary of the E proof (just the premises in their order). The training for datasets 1, 2 and 4 has been running for several weeks, with the performance still slowly improving. See Figure 1 in Appendix A for a sample training and loss on dataset 2. There are many interesting conjectures generated during the unconditioned sampling. The trained models can be directly used by Mizar users for autocompletion of their texts. Some examples compared to real theorems are shown below. More semantic evaluation on the textual datasets (1 and 2) could be done in various ways. We imagine that a proper Mizar environment will have to be guessed, some assumptions may be automatically added, etc.

Conditioned completion
We have also done two initial experiments with proof and formula completion. The data and results for them are available from our web page 9 . In the first experiment, we use a model trained on Dataset 4 (premises), and ask the model to auto-complete 369 theorems from the CARD series of Mizar. For each conjecture we produce 10 premise selections using beam search, and we use different temperatures and beam search parameters. An interesting phenomenon is that with low temperatures, practically all conjectured premises are known Mizar theorems. I.e., the task reduces to standard premise selection. With higher temperatures, GPT-2 starts producing premises (lemmas) that are not among the existing Mizar theorems, but are still well-typed. Even higher temperatures lead to non-well-typed or even unparsable lemmas. The next section provides a more involved ATP evaluation done on a larger dataset. The second experiment was done over Dataset 2 and a set of 462 partial formulas from the CARD articles. The model trained on Dataset 2 is then (again using beam search) asked to auto-complete these formulas. Mizar users can also play with such autocompletion via a web server 10 using this model. For example,

Initial ATP Evaluation
The first larger ATP (semantic) evaluation uses the fourth dataset following the setting introduced for such evaluations in [6]. After training GPT-2 on the 28271 ENIGMA proofs, we produce (using beam search) 12 GPT-2 premise predictions for a set of 31792 theorems of which 6639 are not among the training ones. This yields 381432 predictions, 12 deduplicated to 193320 unique predictions. The predictions are converted back to TPTP from the polish notation, creating ATP problems. We distinguish between the premises that already exist as Mizar theorems and definitions, and the new formulas (conjectures) introduced by GPT-2. 108564 13 of the created problems contain no new conjectures, i.e., GPT-2 works there as a standard premise selector similar to [11].
Most (86899) of these ATP problems 14 can be quickly shown to be countersatisfiable by E prover. 15 This shows the first difference between syntactic loss as used by the ML/NLP community and semantic usefulness. GPT-2's loss is geared towards mimicking the length of the original texts with a small number of syntactic mistakes. In premise selection, the underlying task is to generate premises that have sufficient logical power. Overshooting is better than making a mistake and observing the usual length of the text. 11866 of the problems can be proved in 6 s, resulting in proofs of 8105 theorems. This is not yet an interesting number, because GPT-2 does not observe the chronological order of premises. E.g., 4350 of the proofs use only a single premise -typically GPT-2 suggested the proved theorem itself as a premise. Still, some predictions are chronologically correct and lead to correct new proofs. E.g. for theorem XXREAL 1:48, 16 which is not in the training set, the fifth GPT-2 sample proposed 7 premises 17 of which 5 were used in a quickly found new E proof 18 (see Appendix A for details).
Next we evaluate 19 the 44524 problems 20 that do use at least one newly proposed premise. We have not strictly enforced the chronology, but remove the theorem itself from axioms if proposed. 34675 of the problems are then found countersatisfiable by E in 1 s and for 1515 a proof is found. The conjectures may be interesting, even though hard to prove automatically: E.g. for GROUPP -1:T10 21 a valid, though not quite trivial strengthening from finite to general groups is proposed, see Appendix A for details.
In total, GPT-2 proposed in this experiment 52515 new syntactically correct formulas 22 that deduplicate to 33100. Some are clearly false, yet quite natural to ask: e.g. for dozens of theorems like SINCOS10:17 23 -"sec is increasing on [0, π/2)" -GPT-2 makes the conjecture that every differentiable function is increasing. 24 In this particular case we can likely disprove the conjecture since there are counterexamples in the MML. Similarly, in FUNCTOR1:9 25 , to prove that the composition of full functors is full, GPT-2 proposes to reduce fullness to faithfulness, likely because a previous theorem 26 says that faithfulness is preserved under composition. See Appendix A for details.
Finally we use standard premise selection (although we could recurse and use GPT-2) and E with the ENIGMA guidance to try to prove the 52515 new formulas. 27 This yields 9000-10000 proofs, 28 depending on how we run premise selection and E. While some proofs are long, it seems that we are not yet capable of proving the more interesting conjectures and we still need more ATP strengths. E.g., the longest ATP proof shows that -infty is non empty, where -infty is defined as [0,REAL]. A slightly more useful conjecture which is also hard to prove 29 is the strengthening of the symmetry of the are_homeomorphic predicate 30 from non-empty to arbitrary spaces.