A Deep Reinforcement Learning based Approach to Learning Transferable Proof Guidance Strategies

  • 2020-02-13 18:14:22
  • Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Edwin Pell, Kavitha Srinivas, Veronika Thost, Michael Witbrock, Achille Fokoue
  • 0

Abstract

Traditional first-order logic (FOL) reasoning systems usually rely on manualheuristics for proof guidance. We propose TRAIL: a system that learns toperform proof guidance using reinforcement learning. A key design principle ofour system is that it is general enough to allow transfer to problems indifferent domains that do not share the same vocabulary of the training set. Todo so, we developed a novel representation of the internal state of a prover interms of clauses and inference actions. We also propose a novel neural-basedattention mechanism to learn interactions between clauses. We demonstrate thatthis approach enables the system to generalize from training to test dataacross domains with different vocabularies, suggesting that the neuralarchitecture in TRAIL is well suited for representing and processing of logicalformalisms. We also show that TRAIL's learned strategies provide a comparableperformance to an established heuristics-based theorem prover.

 

Quick Read (beta)

A Deep Reinforcement Learning based Approach to
Learning Transferable Proof Guidance Strategies

Maxwell Crouse    Ibrahim Abdelaziz    Bassem Makni    Spencer Whitehead    Cristina Cornelio    Pavan Kapanipathi    Edwin Pell    Kavitha Srinivas    Veronika Thost    Michael Witbrock    Achille Fokoue
Abstract

Traditional first-order logic (FOL) reasoning systems usually rely on manual heuristics for proof guidance. We propose TRAIL: a system that learns to perform proof guidance using reinforcement learning. A key design principle of our system is that it is general enough to allow transfer to problems in different domains that do not share the same vocabulary of the training set. To do so, we developed a novel representation of the internal state of a prover in terms of clauses and inference actions. We also propose a novel neural-based attention mechanism to learn interactions between clauses. We demonstrate that this approach enables the system to generalize from training to test data across domains with different vocabularies, suggesting that the neural architecture in TRAIL is well suited for representing and processing of logical formalisms. We also show that TRAIL’s learned strategies provide a comparable performance to an established heuristics-based theorem prover.

Machine Learning, ICML
\setstackEOL


1 Introduction

Automated theorem provers (ATPs) have established themselves as useful tools for solving problems that are expressible in a variety of knowledge representation formalisms (e.g. first-order logic). Such problems are commonplace in areas core to computer science (e.g., compilers (curzon1991verified; leroy2009formal), operating systems (klein2009operating), and even distributed systems (hawblitzel2015ironfleet; garland1998ioa)), where ATPs are used to prove that a system satisfies some formal design specification.

Unfortunately, while the formalisms that underlie such problems have been (more or less) fixed, the strategies needed to solve them have been anything but. With each new domain added to the purview of automated theorem proving, there has been a need for the development of new heuristics and strategies that restrict or order how an ATP searches for proofs. The process of guiding a theorem prover during proof search is referred to as proof guidance. Though proof guidance heuristics have been shown to have a drastic impact on theorem proving performance (schulz2016performance), the specifics of when and why to use a particular strategy are still often hard to define (schulzwe).

Many state-of-the-art ATPs use machine learning to automatically determine heuristics for assisting with proof guidance. Generally, the features considered by such learned heuristics would be manually designed (KUV-IJCAI15-features; JU-CICM17-enigma), though more recently they have been learned through deep learning (LoosISK-LPAR17-atp-nn; ChvaJaSU-CoRR19-enigma-ng; paliwal2019graph). However, while deep learning has the obvious advantage of being able to lessen the amount of expert knowledge needed to handcraft new heuristics, its practical application to theorem proving has been limited to domains for which there has been plenty of training data (e.g., in larger theories like Mizar (mizar40for40) or the recent Holist (BaLoRSWi-CoRR19-holist)).

There has also been work exploring the use of reinforcement learning (RL), where the system automatically learns the right proof guidance strategy from proof attempts. Though RL has been successfully deployed in logics less expressive than first-order logic (FOL) (KuYaSa-CoRR18-intuit-pl; LeRaSe-CoRR18-heuristics-atp-rl; CheTi-CoRR18-rew-rl); for more expressive reasoning it has mostly been directed towards synthetic domains (zombori2019towards) or large domains with plentiful training data (KalUMO-NeurIPS18-atp-rl; BaLoRSWi-CoRR19-learning).

In this paper, we deviate from prior work that operates only in data-rich or synthetic domains. We instead take aim at using deep reinforcement learning to guide theorem proving in data-sparse domains, which have been yet unable to leverage the benefits of deep learning driven advances in theorem proving. To do this, we introduce TRAIL, an RL based proof guidance system which is designed to learn transferable strategies that can be leveraged across different problem domains within a logical formalism. At the heart of TRAIL is (a) a novel representation of clauses, which abstracts away the specifics of the vocabulary of a problem, (b) a novel representation of the entire state of a theorem prover, which allows the system to consider the problem as a whole. This approach forces the system to focus less on individual patterns and symbols in a clause, and more on interactions between clause representations, which helps the system generalize across problem domains. To our knowledge, we are the first to design a deep reinforcement based proof guidance system with the explicit goal of building abstractions that suit transfer across problem domains.

We also evaluate multiple training regimens for transfer to determine which mechanism provides the best generalization: (a) we randomly explore from a tabula rasa state as done in AlphaZero (alphazero) to build a proof guidance system that maximizes exploration, (b) we explore the effectiveness of bootstrapping the system based on proofs from existing reasoners in a specific problem domain, where the system can effectively learn from highly optimized reasoners, and (c) we combine the effects of imitation with exploration. We examine how well the three regimens provide transfer across problem domains.

In summary, the core contributions of our work are as follows: (a) We propose a novel deep reinforcement based proof guidance system for FOL, which is general enough to allow transfer to problems in different domains. (b) We demonstrate the efficacy of this system, by showing that it is just as effective as a system which is trained on a problem set where all commonality in vocabulary between problems is removed. (c) We show significant generalization across different problem domains, from Mizar to TPTP and vice versa (after ensuring no overlap between the two data sets in terms of problems and vocabularies11 1 No overlap between TPTP and Mizar is achieved by (1) removing common problems, and (2) by consistent renaming, within each problem, all predicates, functions, and constants), when compared to training and testing on the same domain. (d) We ensure that the performance of our neural based system is competitive with saturation-based FOL reasoners, suggesting that the generalized learning shown by TRAIL approaches that of manually optimized reasoners.

2 Background: Reasoning in FOL

We assume the reader has knowledge of basic first-order logic and automated theorem proving terminology and thus will only briefly describe the terms commonly seen throughout this paper. For readers interested in learning more about logical formalisms and techniques see (thelogicbook; enderton2001mathematical).

In this work, we focus on first-order logic (FOL) with equality. In the standard FOL problem-solving setting, an ATP is given a conjecture (i.e., a formula to be proved true or false), axioms (i.e., formulas known to be true), and inference rules (i.e., rules that, based on given formulas, allow for the derivation of new true formulas). From these inputs, the ATP performs a proof search, which can be characterized as the successive application of inference rules to axioms and derived formulas until a sequence of derived formulas is found that represents a proof of the given conjecture.

The types of formulas considered here are clauses, i.e. disjunctions of literals (where a literal is a (un)negated formula that otherwise has no inner logical connectives). We further specify all variables to be implicitly universally quantified.

The theorem prover compared against in this work, Beagle (Beagle2015), is saturation-based. A saturation-based theorem prover maintains two sets of clauses, referred to as the processed and unprocessed sets of clauses. These two sets correspond to the clauses that have and have not been yet selected for inference. The actions that saturation-based theorem provers take are referred to as inferences. Inferences involve an inference rule (e.g. resolution, factoring) and a non-empty set of clauses, considered to be the premises of the rule. At each step in proof search, the ATP selects an inference with premises in the unprocessed set (some premises may be part of the processed set) and executes it. This generates a new set of clauses, each of which is added to the unprocessed set. The clauses in the premises that are members of the unprocessed set are then added to the processed set. This iteration continues until a clause is generated (in most cases, the empty clause) that signals a proof has been found.

3 TRAIL

We first describe our overall approach to defining the proof guidance problem in terms of reinforcement learning. We then describe two novel aspects of TRAIL that help with generalized learning of proof guidance: (a) a vectorization process which represents all clauses and actions within a proof state in a way that abstracts away the specifics of the vocabulary of a problem and (b) an attention-based policy network that learns the interactions between clauses and actions to select the next action. Last, we describe the three different learning regimens we used to see if generalization varies as a function of training procedure.

3.1 RL-based Proof Guidance

Figure 1: Formulation of automated theorem proving as a RL problem.

We formalize the guidance process as an RL problem where the reasoner provides the environment in which the learning agent operates. Figure 1 shows how an ATP problem is solved in our framework. Given a conjecture and a set of axioms, TRAIL iteratively performs reasoning steps until a proof is found (within a provided time limit). The reasoner tracks the state of the proof, st, which encapsulates both the clauses that have been derived or used in the derivation so far and the actions that can be taken by the reasoner at the current step. At each step, this state is passed to the learning agent: an attention-based model (luong2015attention) that predicts a distribution over the actions and uses it to sample a corresponding action, at,i. This action is then given to the reasoner, which executes it and updates the proof state.

Formally, a state, st=(𝒞t,𝒜t), consists of:

  • 𝒞t={ct,j}j=1N, the set of processed clauses, (i.e., all clauses selected by the agent up to step t); where 𝒞0=.

  • 𝒜t={at,i}i=1M, the set of all available actions that the reasoner could execute at step t. An action, at,i=(ξt,i,c^t,i), is a pair comprising an inference rule, ξt,i, and a clause, c^t,i. c^t,i is an axiom, the negated conjecture, or a derived clause that has yet to be selected by the agent. Informally, 𝒜t represents the unprocessed clauses at step t and the inference rules applicable to them. 𝒜0 is the cross product of the set of all inference rules (denoted by ) and the set containing all axioms and the negated conjecture.

At step t, given a state st (provided by the reasoner), the learning agent computes a probability distribution over the set of available actions 𝒜t, denoted by Pθ(at,i|st) (where θ is the set of parameters for the learning agent), and samples an action at,i𝒜t. The sampled action at,i=(ξt,i,c^t,i) is then executed by the reasoner by applying ξt,i to c^t,i (which may involve other clauses from the processed set 𝒞t). This yields a set of new derived clauses, 𝒞¯t, and a new state, st+1=(𝒞t+1,𝒜t+1), where 𝒞t+1=𝒞t{c^t,i} and 𝒜t+1=(𝒜t-{at,i})(×𝒞¯t).

Upon completion of a proof attempt, TRAIL must compute a loss and issue a reward that encourages the agent to optimize for decisions leading to a successful proof in the smallest number of steps. Specifically, for an unsuccessful proof attempt (i.e., the underlying reasoner fails to derive a contradiction within the time limit), each step t in the attempt is assigned a reward rt=0. For a successful proof attempt, in the final step, the underlying reasoner produces a parsimonious refutation proof 𝒫 containing only the actions that generated derived facts directly or indirectly involved in the final contradiction. At step t of a successful proof attempt where the action at,i is selected, the reward rt is 0 if at,i is not part of this minimal refutation proof 𝒫; otherwise rt is inversely proportional to the total number of steps in the proof attempt.

The final loss consists of the standard policy gradient loss (sutton1998reinforcement) and an entropy regularization term to avoid collapse onto a sub-optimal deterministic policy and to promote exploration.

(θ)= -𝔼[rti=1Mαt(at,i)log(Pθ(at,i|st))]
-λ𝔼[i=1M-Pθ(at,i|st)log(Pθ(at,i|st))]

where αt indicates the action selected at step t (i.e., αt(at,i)=1 if action at,i is selected at t; otherwise αt(at,i)=0), and λ is the entropy regularization hyper-parameter.

We use a normalized reward to improve stability of training as the intrinsic difficulty of problems can vary widely in our problem dataset. We explored (i) normalization by the inverse of the number of steps performed by a mature traditional reasoner (in this work, Beagle), (ii) normalization by the best reward obtained in repeated attempts to solve the same problem, and (iii) no normalization; the normalization strategy was a hyper-parameter. This loss has the effect of giving actions that contributed to the most direct proofs for a given problem higher rewards, while dampening actions that contributed to lengthier proofs for the same problem.

Figure 2: Overview of the vectorizer operating on the clause q(f(g(x,y),z),g(x,y)).

3.2 Vectorization Process

Clause Vectorization: Figure 2 shows an example of the vectorizer operating on a clause with a single positive literal. Our method for vectorization is informed by how inference rules operate over clauses. Consider the resolution inference rule. Two clauses resolve if one contains a positive literal whose constituent atom is unifiable with the constituent atom of a negative literal in the other clause. Hence, vector representations of clauses should capture the relationship between literals and their negations as well as reflect structural similarities between literals that are indicative of unifiability.

Our approach captures these features by deconstructing input clauses into sets of patterns. We define a pattern to be a linear chain that begins from a predicate symbol and includes one argument (and its argument position) at each depth until it ends at a constant or variable. The set of all patterns for a given clause is then simply the set of all linear paths between each predicate and the constants and variables they bottom out with. Since the names of variables are arbitrary, they are replaced with a wild-card symbol, “”, indicating that the element may match with anything. Argument position is also indicated with the use of wild-card symbols. Going back to the clause in Figure 2, we obtain the patterns q(f(g(,),),) and q(,g(,))).

We obtain a d-dimensional representation of a clause, 𝐜t,j, by hashing the linearization of each pattern p using MD5 hashes (rivest1992md5) to compute a hash value v, and setting the element at index vmodd to the number of occurrences of the pattern p in the clause ct,j. Furthermore, we explicitly encode the difference between patterns and their negations by doubling the representation size and hashing them separately, so that the first d elements encode the positive patterns and the second d elements encode the negated patterns. Feature hashing greatly condenses the representation size and has been shown useful in the ATP domain (JU-CoRR19-enigma-hammering; ChvaJaSU-CoRR19-enigma-ng)

Even with MD5 hashing, when operating in domains with smaller vocabularies and shorter formulas it is possible (though unlikely) that vocabulary specific features could still be learned. To mitigate this, our approach systematically renames patterns prior to hashing. Specifically, a unique identifier is appended (generated from the proof attempt number) to each predicate, function, and constant (e.g. in the second proof attempt our patterns would be q2(f2(g2(,),),) and q2(,g2(,))). This does not affect the underlying semantics of a problem, as each predicate, function, and constant has been renamed consistently.

The pattern-based vectorization procedure is intended to produce sparse feature vectors that give reasonable estimates of purely structural similarity. Through both the hashing and renaming, TRAIL has minimal dependence on symbol specific features. While this is certainly appealing from a transferability perspective, we note that it could also be useful when constrained to a single domain. For instance, in Mizar nearly 40% of symbols are introduced during the translation of theories into conjunctive normal form (these are skolem constants, skolem functions, or definitional predicates) (olvsak2019property), which means that any system being applied to Mizar must be able to handle problem specific symbols that may appear only a handful of times.

Action Vectorization: Since actions are pairs of clauses and inference rules, our approach represents the clause in each action pair using the process described above and represents the inference rule as a one-hot encoding of size ||. We write (𝐳t,i,𝐜^t,i) to denote the encoding for action at,i.

3.3 Attention-based Policy Network

Figure 3: Policy network architecture.

The architecture of the policy network in TRAIL is shown in Figure 3. The inputs to the policy network are the sets of processed clause representations, {𝐜t,1,,𝐜t,N}, and action representations, {(𝐳t,1,𝐜^t,1),,(𝐳t,M,𝐜^t,M)}. First, we transform the sparse clause representations (from the set of processed clauses or actions) into dense representations by passing them through k fully-connected layers. This yields sets {𝐡t,1,,𝐡t,N} and {𝐡^t,1,,𝐡^t,M} of dense representations for the processed and action clauses. Then, for each action pair, we concatenate the clause representation 𝐡^t,i with the corresponding inference representation 𝐳t,i to form the new action representation 𝐚t,i=[𝐡^t,i,𝐳t,i]. The resulting sets of new clause and action representations are joined into matrices 𝐂 and 𝐀, respectively.

Throughout the reasoning process, the policy network must produce a distribution over the actions relative to the clauses that have been selected up to the current step, where both the actions and clauses are sets of variable length. This setting is analogous to ones seen in attention-based approaches to problems like machine translation (luong2015attention; vaswani2017attention) and video captioning (yu2016video; whitehead2018kavd), in which the model must score each encoder state with respect to a decoder state or other encoder states. To score each action relative to each clause, we compute a multiplicative attention (luong2015attention)

𝐇 =𝐀𝐖a𝐂,

where 𝐖a(2d+||)×2d is a learned parameter and the resulting matrix, 𝐇M×N, is a heat map of interaction scores between processed clauses and available actions. We then perform max pooling over the columns (i.e., clauses) of 𝐇 to find a single score for each action and apply a softmax normalization to the pooled scores to obtain the distribution over the actions, Pθ(at,i|st).

3.4 Training Regimens

We use one of the following three strategies to attempt to solve all the problems in the training set in order to determine if training regimens also determine how effective generalization is.

Random Exploration: We randomly explore the search space as done in AlphaZero (alphazero) to establish performance when the system is started from a tabula rasa state (i.e., a randomly initialized policy network Pθ). At training, at an early step t (i.e., t<τ0, where τ0, the temperature threshold, is a hyper-parameter that indicates the depth in the reasoning process at which training exploration stops), we sample the action at,i in the set of available actions 𝒜t, according to the following probability distribution P^θ derived from the policy network Pθ:

P^θ(at,i|st)=Pθ(at,i|st)1/τat,j𝒜tPθ(at,j|st)1/τ

where τ, the temperature, is a hyper-parameter that controls the exploration-exploitation trade-off and decays over the iterations (a higher temperature promotes more exploration). On the other hand, when the number of steps already performed is above the temperature threshold (i.e., tτ0), an action, at,i, with the highest probability from the policy network, is selected, i.e., at,i=argmaxat,j𝒜tPθ(at,j|st).

At the end of training iteration k, the newly collected examples and those collected in the previous w iterations (w is the example buffer hyperparameter) are used to train, in a supervised manner, the policy network using the reward structure and loss function defined in Section 3.1. The updated policy network is retained for the next iteration if it is superior to the previous one in terms of number of problems solved on the validation problem set; otherwise, it is discarded. At validation and testing, exploration is disabled (i.e., the temperature threshold is set to 0).

This approach has the disadvantage that the system spends a significant amount of time in unproductive parts of the search space, but it may help transfer because of the random exploration of search space.

Expert Bootstrapping Learning: We explore the effectiveness of bootstrapping the RL process. This approach is similar to random exploration with the exception that, at the first iteration, the initial randomly initialized policy network model is trained, in a supervised manner, using examples from problems from the training set solved by an existing reasoner (in this work we use Beagle (Beagle2015)). Thus, the first iteration ends with a model trained by an expert, then training proceeds exactly as in the first random exploration approach. We contrast this approach versus the random exploration strategy for generalization.

Exploratory Imitation Learning: Similar to expert bootstrapping, we bootstrap the training with examples from an existing reasoner (our expert). But, in later iterations, we reduce our reliance on this reasoner for example collection. Specifically, at iteration k at training, for a step t in the reasoning process, with a probability ρk-1, we delegate the selection of the action from the list of available actions 𝒜t to the expert, and, with a probability 1-ρk-1, we follow the same action selection strategy as in the random exploration approach. Here 0<ρ<1 is a hyper-parameter controlling the decay of our reliance on the expert reasoner. At validation and testing, there is no reliance on the expert. This approach is the middle ground between random exploration and expert based learning, and is hence a useful datapoint in understanding the effectiveness of either on generalization.

4 Experiments and Results

Table 1: Hyper-parameter values
k layers units per layer dropout λ (reg.) 2d (sparse vector size) τ (temp.) τ0 (temp. threshold) ρ (expert decay) reward normalization
2 161 0.57 0.004 645 1.13 11 0.75 (iii) No normalization

In this section, we are trying to answer the following questions: (a) How well does the proof guidance system in TRAIL generalize across problem domains? To evaluate this question, we trained on two different datasets, and then measured generalization across them. (b) What factors contribute to generalization? To evaluate this question, we examined if differences in training regimens in RL affect generalization. (c) Is TRAIL effective at generalized proof guidance? For this, we tested whether TRAIL’s performance was competitive with an existing reasoner.

4.1 Datasets

We evaluated TRAIL using problems drawn from both the Mizar22 2 https://github.com/JUrban/deepmath/ (mizar) dataset and the Thousands of Problems for Theorem Provers (TPTP)33 3 http://tptp.cs.miami.edu/ dataset. Mizar is a well known mathematical library of formalized and mechanically-verified mathematical problems. TPTP is the definitive benchmarking library for theorem provers, designed to test ATP performance across a wide range of problem domains (e.g., biology, geography, number theory, etc.). The different problem domains within the TPTP will serve as our data-sparse setting in our transfer experiment, as each distinct problem domain within the TPTP has on average only 400 problems . Problems from Mizar were drawn from the subset used by (Alemi-NIPS16-deepmath), i.e. the subset of problems known to be solvable by existing ATPs (this subset was used to allow for a direct comparison against our baseline reasoner). From the TPTP dataset, a random subset of 2,000 problems were selected from various problem domains. For transfer and generalization experiments, we ensure no overlap between the two datasets in terms of problems and vocabularies by (a) removing common problems from the test sets, and (b) by consistent renaming, within each problem, all predicates, functions, and constants.

4.2 Hyper-Parameter Tuning and Experimental Setup

We used gradient-boosted tree search from scikit-optimize44 4 https://scikit-optimize.github.io/ to find effective hyper-parameters using 10% of the Mizar dataset. This returned the hyper-parameter values in Table 1. We then selected a different 10% of the dataset (completely disjoint from the one used for hyper-parameter tuning), performed a 3-fold cross evaluation on it, and, for each iteration, we report the average across the combined set of problems in all folds. The maximum time limit for solving a problem was 100 seconds. Experiments were conducted over a cluster of 19 CPU (56 x 2.0 GHz cores & 247 GB RAM) and 10 GPU machines (2 x P100 GPU, 16 x 2.0 GHz CPU cores, & 120 GB RAM) over 4 to 5 days (for hyper-parameter tuning, we added 5 CPU and 2 GPU machines).

We use three metrics to measure performance. The first is cumulative completion performance. Following (BaLoRSWi-CoRR19-learning), this is the cumulative number of distinct problems solved by TRAIL across all iterations divided by the total number of problems. The second metric is best iteration completion performance. This was reported in (KalUMO-NeurIPS18-atp-rl) and is the number of problems solved at the best performing iteration divided by the total number of problems. The third metric is average proof length, which measures the average number of steps taken to find a proof.

Table 2: Number of problems solved across TPTP domains with at least 25 problems used in test set. Random model is not trained.
Domain # Prob. # TRAIL # Beagle # Random
CSR 27 16 16 11
SET 73 25 32 4
GEO 68 21 27 1
SWC 46 14 14 0
KLE 35 4 5 0
LCL 33 8 8 1

4.3 Generalization Across Problem Domains

Table 2 shows TRAIL’s performance when it is trained on Mizar and tested on distinct problem domains from the TPTP. The subject matter between domains can vary greatly. For instance, CSR tests common sense reasoning, while GEO involves reasoning about geometry, and SWC covers software verification. This results in different needs between domains, e.g., the CSR domain requires heavy use of the resolution inference rule while the GEO domain involves more equational reasoning and thus requires the superposition inference rules. As can be seen in Table 2, each distinct domain TRAIL was evaluated on contains only a few problems. By training on Mizar (a completely different dataset designed for different purposes), TRAIL was able to nearly match Beagle in many categories. Furthermore, the performance of the untrained, random model shows that TRAIL was clearly learning transferable proof search strategies.

Table 3: Cumulative completion performance as percentage of problems solved by training regimen and transfer to different datasets. Random model is not trained.
Training Regimens Testing
Mizar TPTP
Beagle 64.1% 37.9%
Random model 22.2% 8.3%
\setstackgapS4.05ex\Centerstack[l]Training
on Mizar
Tabula Rasa 64.3% 31.1%
Expert Bootstrapping 64.8% 33.1%
Exploratory Imitation 64.4% 30.5%
\setstackgapS4.05ex\Centerstack[l]Training
on TPTP
Tabula Rasa 58.5% 31.0%
Expert Bootstrapping 61.0% 29.6%
Exploratory Imitation 63.1% 31.6%

4.4 Generalization Across Datasets

In this experiment, we show TRAIL’s performance when we train it on Mizar and test its performance on TPTP and vice versa. As described earlier, these two datasets have very different vocabularies. In examining the factors that help this sort of generalization across datasets, we examine the effect of each type of training regimen.

Training on Different Regimens: Table 3 shows the performance of the different training regimens and how much each regimen facilitates generalization. As a baseline, we also include the performance of a model with randomly initialized weights, without any training. This randomly initialized model could solve 22.2% of Mizar problems and 8.3% of TPTP problems. We can see first that TRAIL when tested and trained on the same domain performed much better compared to the randomly initialized models (a statistical test of z=34.4,p<.05 for Mizar, z=8.67,p<.05 for TPTP), suggesting that learning did occur. Notice that TRAIL solved on average 64.5% of the Mizar test problems when trained on the Mizar dataset across regimens, and less on Mizar when trained on TPTP at 60.9% (a statistical test of z=3.03,p<.05 suggested statistical significance).

For TPTP, on average, training on TPTP (30.7% of TPTP test problems solved) was statistically just as good as training on Mizar and testing on TPTP (31.6% of TPTP test problems solved). In general, training regimens had no effect on success rates for either Mizar or TPTP. In all other cases such as transfer from Mizar to Mizar, or vice versa or training on TPTP, these differences were not statistically significant, so we do not describe these results further. We therefore conclude that TRAIL provides very good generalization across different datasets, regardless of type of regimen.

4.5 Effectiveness of Trail

Baselines: Beagle (Beagle2015) is an established reasoner that provides competitive performance on ATP datasets. The current implementation of TRAIL uses Beagle as its underlying reasoner. This is purely an implementation choice, made mostly because Beagle is open source and could have its proof guidance removed and replaced with TRAIL. The purpose of Beagle in TRAIL is only to execute the actions selected by the TRAIL learning agent; i.e., Beagle’s proof guidance was completely disabled when it was embedded as a component in TRAIL. TRAIL is not reasoner-dependent, and any reasoner that can apply FOL inference rules can serve the same role as Beagle in TRAIL. We support this claim with an experiment in the following section that shows similar performance gains when Beagle is substituted with a different (in-house) reasoner.

The purpose of the baseline experiments are to ensure that proof guidance controlled by TRAIL functions at a competitive level with a manually-optimized reasoner.

Comparison Against a Heuristics-based Reasoner: Table 3 also shows the cumulative completion performance as percentage of problems solved by TRAIL compared to Beagle (Beagle2015). Beagle’s optimized strategy (heuristics-based) managed to solve 64.1% of the Mizar problems and 37.9% of TPTP problems. On the other hand, TRAIL with expert bootstrapping managed to solve more problems than Beagle on Mizar with 64.8% (statistically insignificant with z=0.57 and p=.57) and it solved 33.1% (statistically insignificant with z=1.46 and p=0.14) of the TPTP problems.

Comparison Against a RL-based Reasoner: We also compare TRAIL’s performance against  (KalUMO-NeurIPS18-atp-rl) using the best iteration completion performance as percentage of problems solved on Mizar dataset at testing (same metric used by (KalUMO-NeurIPS18-atp-rl)). While TRAIL managed to solve 61.6% of the problems, (KalUMO-NeurIPS18-atp-rl) solved only 50%. Although a direct comparison with TRAIL cannot be made due to different time limits and hardware,  (KalUMO-NeurIPS18-atp-rl) reported 90% problems solved by Vampire in the same setting for which they got 50%, suggesting that the baseline performance of TRAIL is very promising.

Proof Length: Figure 4 shows the average number of steps required to find a proof improves over iterations. For each problem, this score is the number of proof steps used by Beagle divided by the number of steps used by TRAIL to find the proof. This score is computed on problems solved by both systems. A score greater than one means TRAIL finds more efficient and shorter proofs compared to Beagle. All training regimens started from the same initial model weights; hence they have the same performance at iteration 1. After the first model update, the performance of all models improved significantly. These scores improve over the iterations, almost matching Beagle for tabula rasa and slightly above Beagle for exploratory imitation at the last iteration.

Figure 4: Validation: Average number of steps required to find a proof relative to Beagle on Mizar (with standard error bars).

Reasoner Agnosticism: TRAIL is a reasoner-agnostic system; i.e., one can use any reasoner after disabling the reasoner’s own proof guidance strategy, as long as this reasoner can execute the actions proposed by TRAIL successfully. To demonstrate that this is indeed the case, we also integrated a baseline reasoner (Basic) in TRAIL. Basic is an in-house reasoner that implements some of the more common state-of-the-art optimization techniques such as subsumption checking, demodulation, and term indexing. The fully optimized version of Basic could solve 13.6% of Mizar problems. TRAIL integrated with Basic could solve only 3% of these problems prior to any training, however it improved to 15.6% after 30 iterations; a 2% improvement over Basic’s fully optimized version. Our goal here was only to demonstrate the generality of the TRAIL system architecture, and to show that the results of prior sections were not due to the choice of a particular reasoner like Beagle.

5 Related Work

Several approaches focus on the (sub)problem of premise selection (i.e., finding the axioms relevant to proving the considered problem) (AlamaHKTU-jar14-premises-corpus-kernel; Blanchette-jar16-premises-isabelle-hol; Alemi-NIPS16-deepmath; WangTWD-NIPS17-deepgraph). As is often the case with automated theorem proving, most early approaches were based on manual heuristics (hoder2011sine; roederer2009divvy) and traditional machine learning (AlamaHKTU-jar14-premises-corpus-kernel); though a few recent works are neural (Alemi-NIPS16-deepmath; WangTWD-NIPS17-deepgraph). As humans still outperform fully automated systems, there has also been research on using learning to support interactive theorem proving (Blanchette-jar16-premises-isabelle-hol; Bancerek-JAR2018-mml).

Some early research has applied (deep) RL for guiding inference (TaylorMSW-FLAIRS07-cyc-rl), planning, and machine learning techniques for inference in relational domains (surveyRLRD). Several papers consider propositional logic or other decidable FOL fragments and thus focus on much simpler algorithms than we do. Close to TRAIL is the approach described in (KalUMO-NeurIPS18-atp-rl). It applies RL combined with Monte-Carlo tree search (MCTS) for automated theorem proving in FOL, but has some key limitations: 1) The input axioms are represented by features that depend on the vocabulary (i.e., user-defined predicates etc.). As a result, the approach would not transfer well to new problems with a different vocabulary. 2) The approach is specific to tableau-based reasoners and therefore may present difficulties for theories containing many equality axioms, which are better handled in the superposition calculus (bachmair1994refutational). 3) It relies upon simple linear learners and gradient boosting as policy and value predictors. Our work also aligns well with the recent proposal of an API for deep RL-based interactive theorem proving in HOL Light, using imitation learning from human proofs (BaLoRSWi-CoRR19-holist). That paper also describes an ATP as a proof-of-concept. However, their ATP is intended as a baseline and lacks more advanced features like our exploratory learning.

Non-RL based approaches using deep-learning to guide proof search include (ChvaJaSU-CoRR19-enigma-ng; LoosISK-LPAR17-atp-nn; paliwal2019graph). Each of the listed works would use a neural network during proof guidance to rank the list of available clauses with respect to only the conjecture. Their underlying theorem prover would then expand proof search from the highest ranked clause. This ranking scheme was recognized as a limitation in (piotrowski2019guiding), where the authors described how such a methodology would fail to capture any dependencies between non-conjecture clauses. Their proposed solution was an RNN-based encoding scheme for embedding entire proof branches in a tableau-based reasoner. The choice of a tableau reasoner was due to the relative compactness of tableau proof branches, which helped to keep the RNN from incorrectly discarding information. It was unclear how to extend their method to saturation-based theorem provers, where a theorem prover state may include thousands of irrelevant clauses.

6 Conclusions

We presented TRAIL: a flexible, deep reinforcement learning based proof guidance system that transfers well across FOL problem domains. The transfer was robust across training regimens and changes in problem vocabularies. A next step is to see if training transfers across logical formalisms.

References