Title: LEARNING TO PROVE THEOREMS BY LEARNING TO GENERATE THEOREMS

Abstract: We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited humanwritten theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach significantly improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.

1. INTRODUCTION:

Automated theorem proving is a key task in Artificial Intelligence. The goal is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated theorem proving is useful in a wide range of applications, including the verification and synthesis of software and hardware systems (Gu et al., 2016; Darvas et al., 2005; Kern & Greenstreet, 1999) .

Automated theorem proving boils down to a search problem: finding the sequence of symbol manipulations that generate a valid proof. A prover typically works backward: starting from the theorem statement, it searches for a path that connects the theorem to known facts in the knowledge base. The fundamental challenge lies in the explosion of search space, in particular with long proofs and large knowledge bases. The success of theorem proving thus relies on effective heuristics that guide the search by deciding the next step the prover should take.

Deep learning has emerged as a promising approach to learning search heuristics in a automated theorem prover (Irving et al., 2016; Yang & Deng, 2019; Whalen, 2016; Loos et al., 2017; Bansal et al., 2019a) . The search process fundamentally reduces to a sequence of actions on manipulating a set of symbols. Thus a deep network can be trained to select the best action at each step.

A key challenge is how to train such networks. Prior work has used human-written theorems and proofs to perform imitation learning and has shown promising results (Loos et al., 2017; Yang & Deng, 2019; Whalen, 2016; Paliwal et al., 2019) . The training data consists of theorems and proofs manually written by human experts in a formal language, and the prover is trained to imitate the proof steps demonstrated by humans.

However, relying on human-written data has a major drawback, that is, such data has limited availability and scalability. Writing theorems and proofs in a formal language requires highly specialized knowledge and skill, including mathematics, computer programming, and proficiency in the particular formal language. For a computer science graduate student, it can take months to master a new formal language such as Mizar, Metamath or HOLight (Wiedijk, 2003) , after which it can take days to formalize a single page of a math textbook. This makes it impractical to crowdsource human-written proofs at large scale.

An alternative to imitation learning is reinforcement learning, which requires only formalized theorem statements but not their proofs. During training, the prover estimates the value of each action through exploration. This reinforcement learning approach substantially reduces the amount of manual formalization needed, but at the expense of sample efficiency. The prover needs positive rewards to assess past attempts, but positive rewards are only available when the prover finds a com-plete proof, which is rare because it involves a combination of multiple correct steps. This leads to extremely sparse positive rewards, and in turn very low sample efficiency.

In this paper, we propose to learn search heuristics using synthetic data. The basic idea is to construct a generator that automatically synthesizes new theorems and their proofs, which are then used to augment human-written data. To generate a new theorem and its proof, the generator applies an inference rule on a set of existing theorems and combines their proofs to form the proof of the new theorem. Similar to the prover, the generator performs a sequence of symbol manipulations, albeit in the inverse direction, going forward from existing theorems to a new theorem instead of from a target theorem to existing ones.

A key question is how to construct a generator such that the generated data is useful. The space of new theorems and proofs is infinite, but a prover can only process a finite amount of data during training. Thus, to maximize the utility of the generate data, we make the generator learnable by parametrizing it with deep networks.

We hypothesize that the generated data will be more useful if they are similar to human-written data. Thus we use human-written data to train a generator. We consider two scenarios. If the humanwritten data consists of both theorem statements and their proofs, we train the generator to follow the proof steps in the forward direction, so that a well-trained generator would derive theorems humans tend to derive. If the human-written data consists of only theorem statements but not their proofs, we use reinforcement learning to train the generator such that the generated theorems are similar to the human-written theorems. We measure similarity using the language model trained on the human-written theorem.

We instantiate our approach in Metamath (Megill, 2019) , a popular language for formal mathematics, and with Holophrasm (Whalen, 2016), a Metamath neural prover. We propose a neural theorem generator we call "MetaGen", which synthesizes new theorems and their proofs expressed in the formalism of Metamath. To the best of our knowledge, MetaGen is the first neural generator of synthetic training data for theorem proving. Experiments on real-world Metamath tasks demonstrate that synthetic data from MetaGen helps the prover prove more human-written theorems, achieving state of the art results. Experiments also show that our approach can synthesize useful data, even when there are only human-written theorems but zero proofs during training.

2. RELATED WORK:

Automated theorem proving Our work is related to prior work on learning to prove theorems (Whalen, 2016; Gauthier et al., 2018; Bansal et al., 2019a; Yang & Deng, 2019; Loos et al., 2017; Balunovic et al., 2018; Kaliszyk et al., 2018; Bansal et al., 2019b) . Our work directly builds off of Holophrasm (Whalen, 2016), a neural-augmented theorem prover for Metamath. It contains three deep networks to generate actions and initial values to guide proof search following the UCT algorithm (Kocsis & Szepesvári, 2006) .

TacticToe (Gauthier et al., 2018) , DeepHOL (Bansal et al., 2019a) and ASTactic (Yang & Deng, 2019) are learning-based theorem provers for higher-order logic based on various interactive theorem provers, including HOL4 (Slind & Norrish, 2008) , HOL Light (HOLLight) and Coq (Bertot & Castéran, 2004) . Paliwal et al. (2019) improves DeepHOL by representing formulas as graphs. Loos et al. (2017) propose to learn clause selection by deep learning inside the first-order logic prover E (Schulz, 2002) . FastSMT (Balunovic et al., 2018) learns to compose search heuristics as programs with branches for the SMT solver (De Moura & Bjørner, 2008) .

All of these methods are othogonal to our approach because all of their provers are learned from human-written training data, whereas our contribution is on training a neural generator of synthetic training data for theorem proving. Kaliszyk et al. (2018) ; Bansal et al. (2019a; b) use reinforcement learning to train provers with only human-written theorems but not their proofs. During training, a prover only collects rewards only upon finding full proofs. In contrast, we always train our prover using imitation learning. Under the same setting with only human-written theorems but not proofs, we use reinforcement learning to train our generator, whose reward is the similarity between a generated theorem and a humanwritten theorem, as measured by a language model of human-written theorems. Our reinforcement learning task is much easier because the reward is continuous and there are many ways to generate theorems similar to human-written ones.

Automatic goal generation by self-play Our work is similar to the line of work in reinforcement learning (Florensa et al., 2018; Sukhbaatar et al., 2017; 2018; Durugkar & Stone, 2018) that deploys one agent to generate tasks for another agent to accomplish. Sukhbaatar et al. (2017) ; Florensa et al. (2018) propose to train these two agents by adversary self-play, where the generation agent learns to produce difficult goals for another agent. With self-play, the generator learns to increase the difficulty of goals and build a learning curriculum automatically.

We pursue similar ideas in the new context of theorem proving by learning to generate synthetic theorems to train the prover. Also of note is that we have no adversarial self-play. The goal of the generator is to discover novel theorems similar to human-written ones, not to beat the prover.

Recently, Huang (2019) introduced a two-player game which encourages players to learn to predict the consistency of formulas in first-order logic by self-play. These two players behave symmetrically and complete with each other in the game. In contrast, our generator and prover execute different tasks, and are co-operative. In addition, their game remains a theoretical proposal without any empirical validation, whereas we have performed experiments on large-scale data.

3. BACKGROUND ON METAMATH:

Metamath is a language for developing formal mathematics. It is one of the simplest formal systems. It has only one inference rule, called substitution, but is universally applicable in formalizing a large portion of mathematics1 and different types of logic (Megill, 2019) .

A knowledge base in Metamath consists of a set of theorems including axioms, which are admitted to be true, and others that are derived from proofs. Each theorem has one or more expressions, including one assertion and zero or more hypotheses. The hypotheses provide the preconditions, such as x = y2 and y is an even number, to prove the assertion, such as x is divisible by 4.

Following Whalen (2016), an expression is represented as a tree of tokens, whose nodes are either constants or variables. A constant node has a fixed number of children (including zero) and a variable has no children. Therefore, we represent each expression as a unique sequence of tokens by traversing its parse tree in pre-order.

A proof is a sequence of steps using substitution. A proof step has two parts, a theorem that is declared earlier than the current theorem in the knowledge base, and a substitution that maps a variable in this theorem to a new expression. For example, we have a theorem t, hypotheses:

A = B (1) assertion: CF A = CF B (2) {A, B, C, F } is the set of variables in t.

Let φ be a substitution to map each variable in t to a new expression,

EQUATION

By replacing variables in the t with their corresponding expressions from φ, we have a new assertion and a set of new hypotheses, new hypotheses:

EQUATION

and this proof step (t, φ) demonstrates that the new assertion 2 + 2 = 2 + (1 + 1) is entailed by the new hypothesis 2 = (1 + 1). Note that we need to substitute all occurrences of the same variable with the same expression in both the assertion and hypotheses 2 .

Formally, let e ∈ E be an expression (a tree of tokens) with l unique variables f e = (f 1 , f 2 , ..., f l ) ∈ F l , and let φ ∈ F → E be a substitution. Let e(φ) denote the new expression obtained by replacing f i in e with φ(f i ), for i = 1, 2..., l. And given k expressions e = (e 1 , e 2 , ..., e k ) ∈ E k , let e(φ) = (e 1 (φ), e 2 (φ), ..., e k (φ)) represent applying the substitution to all k expressions.

Given a theorem t, let a t be its assertion and h t = (h t,1 , h t,2 , ..., h t,m ) ∈ E m be its hypotheses. Let φ t be a substitution for variables in t. A proof step s = (t, φ t ) ∈ E m+1 × (F → E) demonstrates an entailment of assertion a t (φ t ) by hypotheses h t (φ t ).

In this formal system, proving a theorem τ means finding a tree such that (1) the root node is the assertion of τ , (2) each leaf node is either empty or one of the hypotheses of τ , and (3) each internal node is an expression associated with a proof step that demonstrates an entailment of the node by its children.

To prove a target theorem τ , it is the most straightforward to reason backward. We start by selecting a proof step that will demonstrate an entailment of the assertion of the target theorem, that is, 

a t (φ) = a τ .

4. APPROACH:



4.1. PROBLEM STATEMENT AND APPROACH OVERVIEW:

In our task setup, we assume two sets of pre-existing human-written theorems. There is a set of "background theorems", B = {b 1 , b 2 , ..., b n }, which can be freely used as known facts in both training and testing. Each proof step consists of a background theorem b ∈ B and its substitution.

There is also a set of "target theorems", T = {t 1 , t 2 , .., t n }, which are theorems to prove. The target theorems are split into a training set, a validation set, and a test set. The target theorems in the test are not seen during training. A prover learns to prove the target theorems in the training set. The final goal of the prover to perform well on the target theorems in the test set.

For target theorems in the training set and the validation set, a subset of them have human-written proofs. Let S = (s 1 , s 2 , ..., s k ) be proofs for k target theorems (t s,1 , t s,2 , ..., t s,k ) ⊆ T and s i = (s 1 i , s 2 i , ...s li i ) be a sequence of proof steps for i = 1, 2, ..., k. We also consider the case with only theorems but zero proofs.

Our approach consists of two modules, a prover to find proofs for given target theorem and a generator to sample synthetic theorems along their proofs. We call these synthetic theorems as "generated theorems". These two modules performs similarly but in opposed directions. They both generate proof steps iteratively to find a proof for the target theorem or generate new theorems.

The prover executes backward reasoning. Given a target theorem, it builds the proof search tree where a node represents a goal. It starts from the assertion as the root and extends the proof search tree by decomposing current goals using new proof steps. It succeed if a complete proof is found.

The generator runs in forward reasoning. It maintains a graph of theorems where nodes in the graph are all theorems it has encountered during training, and each edge represents entailment in a single proof step between a precondition and the assertion. It samples new proof steps using existing theorems as preconditions and add the generated theorems to the graph. Generated theorems are then used to train the prover.

For both the prover and the generator, the policies to pick a proof step are parameterized by deep networks with similar architectures but different inputs.

We first train the generator using target theorems and optionally their proofs. Then sample synthetic proofs and train the prover from both human proofs and synthetic proofs. Initialize()

while V.length ≤ N do / * A new proof step. * / Sample b ∼ D 1 // ( * * ) φ, q ←-∅, ∅ for h ∈ h b do / * Sample a precondition node for h * / try Sample q, φ q ∼ D 2 except Failed Restart from ( * * ) end Add q to q Merge φ q to φ end for f ∈ b's assertion variables do / * Generate a substitution for f * / try Sample e f ∼ D 3 except Failed Restart from ( * * ) end φ(f ) ←-e f end AddNode(b, φ, q) end return end Function Initialize(): V, E ←-∅, ∅ for t ∈ T do for h ∈ h t do / * Add a hypothesis * / Add (h, {h}) to V end end for s ∈ S do for (b, φ) ∈ s do / * Add a step (b, φ) * / q ←-precondition nodes for (b, φ) AddNode(b, φ, q) end end return end Function AddNode(b, φ, q): a, h ← a b (φ), ∅ for q ∈ q do / * Merge hypotheses * / Merge h q to h end v ← (a, h) if v / ∈ V then / * A new node. * / Add v to V for q ∈ q do Add (q, v) to E end end return end 4.2 GENERATOR 4.2.1 GENERATION PROCEDURE

The generator maintains a graph of theorems G = (V, E), where V = H Q is the set of nodes and E is the set of edges.

H is the set of hypotheses, which is collected from target theorems T as H = t∈T h t . H is fixed and we never generate new hypotheses. For convenience, we write a hypothesis h as (h, {h}) in the same form as a theorem, such that we have a h = h, h h = {h}. Q = {(a 1 , h 1 ), (a 2 , h 2 ), (a 3 , h 3 ), ...} is the set of theorems that have been encountered by the generator. Here we record each node in the form of theorems instead of assertions, because hypotheses play an important role to the meaning and the proof of a theorem. We hope to keep track of different proofs for the same assertion from different hypotheses.

G is a directed graph. An edge (u, v) ∈ E represents that v is entailed in a proof step that uses a u the assertion of u as one of the preconditions. A hypothesis node has no incoming edges. For a node, if multiple proofs exist, we preserve the edges from the last proof step of its shortest proof.

To generate a new theorem, a proof step is sampled such that every precondition for this step is identical to the assertion of a node in the graph. We call this node the precondition node.

Formally, given a proof step s = (b, φ) and precondition nodes q ⊆ V , s demonstrates that a b (φ) is entailed by the preconditions h b (φ). For h ∈ h b (φ), we have a node q h ∈ q such that a q h = h. Then we merge hypotheses from precondition nodes to get h = h∈h b (φ) h q h and compose a theorem (a b (φ), h), which means a b (φ) can be proved from the new hypotheses h merged from precondition nodes. It is added to Q if it is different from other nodes in the graph. This procedure is summarized as AddNode in Algorithm 1.

Initially, we add hypotheses from target theorems T into H.

If we have at least one training proof, assume t s ∈ T is the target theorem for a proof s = (s 1 , s 2 , ..., s l ) ∈ S. For a proof step s i = (b, φ) ∈ s, where i = 1, 2, ..., l, each precondition h ∈ h b (φ) for s i is either a hypothesis of t s or an intermediate assertion that is entailed in a previous step s j ∈ s, where j < i. This means a node q satisfying a q = h has been added to the graph G previously. So we can find precondition nodes for s i and add this step to the graph.

The above process is also summarized as Initialize in Algorithm 1.

After initializing the graph G from training data, we sample proof steps upon nodes in G as precondition nodes to produce new generated theorems. We repeat this procedure until we obtain all the generated theorems in our expectation to training the prover.

To sample a proof step, we need to make three decisions sequentially.

• Sample a background theorem b ∼ D 1 (B).

• Given an empty substitution φ and precondition nodes q, for each hypothesis h b,i ∈ h b , sample a node q i ∼ D 2 (b, φ, q) and its corresponding substitution φ i , such that h b,i (φ i ) = a qi and φ i is consistent with the existing substitution φ. Update φ and q using φ i and q i . • Optionally, if the theorem b has assertion variables, for each assertion variable f , sample an expression e ∼ D 3 (f, b, φ, q) and update φ.

The distribution D 1 (B) is either uniform over T or multinomial over the frequencies of background theorems used in training proofs.

D 2 is a distribution over all nodes in G that can result in a substitution φ i consistent with φ and h b,i . D 2 is multinomial over softmax probabilities outputted from a deep network, called the relevance network following Whalen (2016).

Graph G could have millions of nodes. This makes it intractable to compute D 2 over all nodes in G. In practice, we limit the number of nodes for D 2 to compute. Given a hypothesis h, to sample a precondition node, we retrieve all nodes that could fit h by substitution. If we get too many candidates, we sample 2000 nodes randomly and calculate D 2 over these 2000 candidates using the relevance network.

D 3 is a distribution over potential expressions. We parameterize D 3 by a sequence generation network, which produces the pre-order traversal sequences for the expression trees. We call this network as substitution network instead of generation network used in Whalen ( 2016) to prevent it from getting confused with the generator.

If we cannot find a feasible precondition node for a hypothesis of b or generate a legal expression to an assertion variable, we fail in this iteration and restart by sampling a theorem.

The complete generation procedure is summarized as Generate in algorithm 1. The architecture of the relevance and substitution networks of the generator is presented in Appendix A.1.1.

4.2.2. TRAINING OF THE GENERATOR:

We propose two training strategies to learn the generator, with or without training proofs.

With access to training proofs, we train the generator using Imitation Learning. After initializing the graph G from training proofs, the generator is trained to imitate each proof step s = (b, φ). For each h ∈ h b , we use a node q where a q = h(φ) as supervision for the relevance network to learn to pick precondition nodes. For each b's assertion variable f , we use the φ(f ) as supervision for the substitution network to learn to generate substitution for f .

We call the generator trained in this strategy as MetaGen-IL.

If we have no access to training proofs, we train the generator using Reinforcement Learning. We first learn a language model from target theorems using a GRU. We expect this language model assigns low cross-entropy to generated theorems that are similar to target theorems. Then we use this language model as a reward function to train the generator with the Reinforce algorithm. We run the generator to sample new generated theorems on-the-fly. New theorems are evaluated by the cross-entropy of the language model and the generator is updated toward lower cross-entropy.

We call the generator trained in this strategy as MetaGen-RL.

4.3. PROVER:

We adopt Holophrasm as our theorem prover. Given a target theorem, Holophrasm tries to find the proof by backward reasoning. It starts from the assertion and builds the proof search tree that consists of goals and proof steps. Each goal has multiple proof steps as its children. Each proof step (b, φ), which demonstrates that a b (φ) is entailed by h b (φ), has a b (φ) as its parent and a set of subgoals h b (φ) as its children. A proof step is solved if it has no children or all of its children are solved. A goal is solved if at least one of its proof steps is solved. The proof is found when the assertion in the root is solved.

Holophrasm maintains valuation for goals and proof steps. It explores the proof search tree using UCT (Kocsis & Szepesvári, 2006) . The search direction is controlled by the valuation, which is dependent on a node's initial value and visit count following the UCB criterion.

The initial value of a goal is from a payoff network. To generate a proof step for the current goal, a relevance network picks a theorem and optionally a substitution network produces substitutions for hypothesis variables. The initial value of this step is also calculated using the prediction scores from relevance and substitution networks.

All deep networks (relevance, substitution, payoff) of the prover are trained by imitation learning.

We mix the human proofs for training theorems and synthetic proofs generated by MetaGen and optimize deep networks to make the same decision as a training proof step. Noted that, we don't limit the number of candidates for relevance networks in the prover as we do in the generator.

The architecture and more training details of deep networks for the prover is presented in Appendix A.1.2.

5. EXPERIMENTS:



5.1. EXPERIMENTAL SETUP:

To evaluate our proposed methods, we train the prover on the mixture of human proofs (if available) and synthetic proofs sampled by our proposed generator MetaGen, in three different settings: (1) with 10% training proofs, (2) with all training proofs, and (3) with no training proofs.

Dataset We use the Metamath set.mm knowledge base as our dataset. set.mm formalizes the Tarski-Grothendieck set theory. It contains 29337 theorems and they are all used as background theorems B in algorithm 1. We remove axioms from B and use the rest of theorems as target theorems T that are divided into three sets, including 21788 training theorems, 2712 validation theorems and 2720 test theorems.

The generator is trained on training theorems and their human proofs optionally. For experiments with no training proofs, we learn a language model from training theorems and use it as the reward function to train MetaGen-RL. For other two experiments with 10% or all human proofs of training theorems, we train MetaGen-IL on the given proofs as described in section 4.2.2.

Baselines For all experiments, we compare with Holophrasm trained on human proofs only by imitation learning the same as Whalen (2016). With no human proofs, we propose also an ad-hoc baseline by replacing relevance and substitution networks with TF-IDF similarities and a naive language model. For more details on baseline methods, please refer to Appendix A.2.

Evaluation The prover is evaluated by the number theorems proved on the test set. Following the settings used in Whalen ( 2016), the prover is run on each test target theorem for 5 minutes or through 10000 passes, in three runs with different beam search width as 1,5,20 for substitution networks.

Since payoff networks are trained on exclusive data sampled by relevance and substitution networks, they can not be compared among different methods. In general, we found payoff networks work similarly, with accuracy ranging from 78 to 82.

Please also refer to Appendix A.3 for our full implementation details and hyper-parameter settings.

We present the performance of the relevance and substitution networks and the final provers in the next section.

5.2. RESULTS:



Relevance network:

We evaluate relevance networks by the average probability and top-K accuracy to pick positive theorems among all feasible candidates. From table 1, we got similar performance for all networks trained using human proofs, even among those trained on 10% or all proofs.

In all settings, the performance of substitution networks are improved by a large margin by using synthetic data. This demonstrates the synthetic proofs generated by MetaGen are effective in training substitution networks.

With 10% proofs, MetaGen-IL-Rand beats the baseline trained on 10% proofs only. This result demonstrates the robustness of the MetaGen algorithm even without learned parameters. MetaGen-IL outperforms MetaGen-IL-Rand and this verifies that the learning of the generator is effective.

Prover Since we cannot promote relevance networks using synthetic proofs, we only apply relevance networks trained on real proofs only, to study if improvement from substitution networks could be reflected on provers.

As shown in table 3 , provers augmented with synthetic proofs generated by MetaGen proved more target theorems than all baseline methods with the same amount of human proofs.

Our re-implementation of Holophrasm baseline using all proofs proves 539 test theorems, which is much higher than reported by Whalen ( 2016). We assume it is due to our GPU implementation, which brings the speed advantages since all provers run in the same time limit.

Given no training proofs, the original Holophrasm performs worst since it carries two randomly initialized networks. After training on synthetic proofs generated by MetaGen-RL, Holophrasm proves 140 more test theorems. It also find 12.5% more proofs than TF-IDF and language model baseline. This shows the effectiveness of MetaGen-Rl.

By incorporating MetaGen-IL with all training proofs, we prove 574 theorems on the set.mm knowledge base, which is the new state-of-the-art result on this benchmark.

Generated theorems:

We show some examples of the generated theorems in table 4. Generated theorems range over different topics, such as basic arithmetic, complex analysis, basic function operation, number theory and algebraic structures.

Some theorems provide important and interesting results, such as the third one, a equation involving the trigonometric function and the complex formula. Some are boring for human, such as the first one and the fourth one, but they also provide meaningful training data for the prover. The first one takes five steps to prove and the fourth one takes four steps. Although their proofs consist of common used theorems, such as commutative law of addition and real field is closed to arithmetic, they provide novel scenarios to exercise these theorems. Without humans' intuition and abstraction, such "trivial" exercises are helpful for deep networks to strengthen their memorization and generalize to broader range of theorems. 

A APPENDIX:

A.1 NETWORK ARCHITECTURE Our deep networks follow the same architecture as Holophrasm (Whalen, 2016) . We represent each expression as a sequence of tokens. Both the relevance and substitution networks take such expression sequences as inputs. A embedding layer is learned for tokens in the vocabulary and GRUs (Cho et al., 2014) are used to encode and decode input sequences.

A.1.1 GENERATOR:

The relevance network picks a precondition node among some theorem nodes according to the background theorem b and previously selected precondition nodes. It uses a theorem encoder to embed the background theorem b as concatenation of the assertion and hypotheses of b and hypotheses of selected precondition nodes. It uses another precondition encoder to embed each theorem node as concatenation of its assertion and hypotheses. These two embeddings are fed to a bilinear layer for the score of this node. The softmax probabilities are outputted over all candidates.

The substitution network is a sequence-to-sequence model. It generates the substitution for a variable f in background theorem b, given a set of precondition nodes. It replaces f as special token to mark itself as the target, then uses a encoder-decoder GRU to generate the output sequence from concatenation for the assertion of b and hypotheses of precondition nodes.

A.1.2 PROVER:

The relevance network picks a theorem on a goal given a proof task. It has a theorem encoder to embed each potential theorem as the concatenation of its assertion and hypotheses. It also has a goal encoder to embed the concatenation of goal and the hypotheses of the task. A bilinear layer and the softmax function follows these two encoders to output the probability over potential theorems.

The substitution network is a sequence-to-sequence model. After replacing a target variable as a special token, it takes inputs as the concatenation of hypotheses of the task and hypotheses of a picked theorem, passes it through a encoder-decoder to generate a sequence tokens as the substitution.

The payoff network predicts if a goal can be proved in the given proof task. So it takes the concatenation of the goal and hypotheses of the task as inputs and use a GRU encoder and two linear layers to get the score for the current goal.

The relevance and substitution networks are learned from training proofs. Given a proof step s = (b, φ), the relevance network learns to predict b from other theorems and the substitution network learns to generate φ(f ) for a hypothesis variable f in b.

The payoff network works as a binary classifier of intermediate goals. Positive instances are extracted as goals from training proofs. Negative instances are generated using the learned relevance and substitution networks. For each goal in training proofs, we generate proof steps and its subgoals. The subgoals not covered by the proof are treated as negative instances.

:

Its largest knowledge base, set.mm ranks 3rd in the "Formalizing 100 Theorems" challenge (Wiedijk).

Variables in Metamath are called metavariables, which are different from variables bound by quantifiers in the first-order and higher-order logic.

Figures and Tables:

It is worth noting that if we pick a particular theorem t, if a valid φ exists, φ(f ) is uniquely determined for any variable f that occurs in the assertion (recall that each expression is a tree of tokens). But φ(f ) is not uniquely determined if f only occurs in the hypotheses (f is called a hypothesis variable, or a assertion variable if it only occurs in the assertion), because it can be replaced with anything. Once this initial proof step (t, φ) is fully specified, the assertion a τ is entailed by a set of new hypotheses h τ (φ), and the goal of proving theorem τ has now been decomposed to the subgoals of finding entailment of the new hypotheses h τ (φ) by the original hypotheses h τ .

Table content: <table/>

The performance of relevance networks on validation data evaluated by the average probability and top-K accuracy to pick positive theorems.

Table content: <table><tr><td>Human</td><td>Synthetic</td><td/><td/><td/><td/></tr><tr><td colspan="2">proofs proof steps</td><td>Generator</td><td>Model</td><td>Prob</td><td colspan="2">Top-1 Top-5 Top-20</td></tr><tr><td>0</td><td>0</td><td>-</td><td>tf-idf</td><td colspan="2">0.0081 27.82 36.15</td><td>47.68</td></tr><tr><td>0</td><td>0</td><td>-</td><td colspan="3">relevance 0.0065 0.279 1.924</td><td>12.50</td></tr><tr><td>0</td><td>200K</td><td colspan="4">MetaGen-RL relevance 0.2160 22.23 42.23</td><td>60.54</td></tr><tr><td>2179</td><td>0</td><td>-</td><td colspan="3">relevance 0.6007 62.14 76.30</td><td>89.30</td></tr><tr><td>2179</td><td>1M</td><td colspan="4">MetaGen-IL relevance 0.5889 62.14 76.29</td><td>87.61</td></tr><tr><td>21788</td><td>0</td><td>-</td><td colspan="3">relevance 0.5978 61.54 74.55</td><td>87.28</td></tr><tr><td>21788</td><td>10M</td><td colspan="4">MetaGen-IL relevance 0.5920 63.02 76.71</td><td>87.93</td></tr></table>

The performance of substitution networks on validation data evaluated by the average probability and accuracy to generate the ground truth token at each position with teacher forcing.

Table content: <table><tr><td>Human</td><td>Synthetic</td><td/><td/><td/><td/></tr><tr><td colspan="2">proofs proof steps</td><td>Generator</td><td>Model</td><td>Prob</td><td>Accuracy</td></tr><tr><td>0</td><td>0</td><td>-</td><td colspan="2">lauguage model 0.0032</td><td>9.06</td></tr><tr><td>0</td><td>0</td><td>-</td><td>substitution</td><td>0.0008</td><td>0.01</td></tr><tr><td>0</td><td>200K</td><td>MetaGen-RL</td><td>substitution</td><td>0.0050</td><td>25.03</td></tr><tr><td>2179</td><td>0</td><td>-</td><td>substitution</td><td>0.2738</td><td>58.91</td></tr><tr><td>2179</td><td>1M</td><td>MetaGen-IL-Rand</td><td>substitution</td><td>0.3203</td><td>61.78</td></tr><tr><td>2179</td><td>1M</td><td>MetaGen-IL</td><td>substitution</td><td>0.3710</td><td>66.56</td></tr><tr><td>21788</td><td>0</td><td>-</td><td>substitution</td><td>0.6142</td><td>81.57</td></tr><tr><td>21788</td><td>10M</td><td>MetaGen-IL</td><td>substitution</td><td>0.6847</td><td>83.90</td></tr><tr><td colspan="6">With 10% training proofs, we also compare with a random generator baseline MetaGen-IL-Rand.</td></tr></table>

Sainbayar Sukhbaatar, Emily Denton, Arthur Szlam, and Rob Fergus. Learning goal embeddings via self-play for hierarchical reinforcement learning. arXiv preprint arXiv:1811.09083, 2018. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016. Freek Wiedijk. Formalizing 100 theorems. http://www.cs.ru.nl/ ˜freek/100/. Freek Wiedijk. Formal proof sketches. In International Workshop on Types for Proofs and Programs, pp. 378-393. Springer, 2003. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, 2019.

Table content: <table/>

Peer review (iclr2020):
This paper focuses on the problem of developing deep learning systems that can prove theorems in a mathematical formalism -- in this case, MetaMath. This has been a rapidly growing topic in the past few years, as evidenced by the numerous cited works. What sets this work apart from others is its focus on the instrumental task of generating data to train a prover, rather than directly training the prover on human theorems (via reinforcement learning) or human proofs (via imitation learning). The paper proposer two approaches to generating theorems imitation learning (IL) and reinforcement learning (RL). The IL approach trains a neural policy to imitate the same steps taken in human proofs. The RL approach first trains a language model on human theorems (not proofs), and uses the likelihood under the model as a reward function for an RL agent which must take forward proof steps. Both approaches result in a policy that can be used to take proof steps, with the goal of producing new theorems which are similar to the human ones. Since the proof steps are known for the generated theorems, a prover agent (which operates in backwards mode, working from the goal back to the hypotheses) can be trained to imitate the steps taken in the synthetic proofs (along with the human ones, if any are present). At test time, the learned prover imitation policy is then used to guide an MCTS agent, as described in the Holophrasm paper. It is compared against the original Holophrasm algorithm, rerun on modern hardware. This is to my knowledge a novel approach in the neural theorem proving domain, and in my opinion one that offers a potentially significant advantage over the existing fixed-dataset appraoches. The main result of the paper is that an extra 35/2720 (1.2%) of the test theorems are proven, a 6% improvement over the Holophrasm baseline of 539. It is difficult to judge how relevant of an improvement this is, and there is no analysis of the difficulty of the MetaMath problem set. In addition, due to the 10-1-1 train-validation-test split, the neural agents are likely shown relatively similar problems during training as at test time, including potentially stronger versions of the same theorems. There is also no comparison against non-neural approaches, such as Z3, Vampire, or similar theorem provers. To accept this paper, I would like to see stronger evidence that the introduced method produces significant improvements in prover ability. For example, the same method could be applied to datasets such as HOList, Mizar, and CoqGym which have received more attention recently than MetaMath. Some additional questions and comments: 1. How big does the theorem graph G get? Since the relevance policy is over all nodes of the graph, this could lead to a very large neural network that would be difficult to fit into memory. Certainly not all 1M synthetic theorems could be generated in one graph. 2. The paper claims that all theorems from set.mm are used as background theorems in algorithm 1, including the test ones -- this potentially sounds like training on the test set, or even worse, having access to the test theorems as *proven background knowledge* at test time. 3. Please include some more details about the training of the Holophrasm baseline. Does it simply do RL on the human theorems, or does it also do IL on human proofs?