Machine Learning Guidance for Connection Tableaux

In this section, we show how the prover transforms problems into formulas and processes them to yield a matrix. We focus on first-order logic problems represented as a set of axioms \(\{A_1, \dots , A_n\}\) together with a conjecture C, where all axioms and the conjecture are closed formulas. The goal is to show that the axioms imply the conjecture. For convenience, in the actual implementation we use the TPTP format [76] as input. Each parsed input problem is transformed according to the following procedure. Only the steps 2 and 6 differ in comparison with the original Prolog implementations of leanCoP and nanoCoP [57, 61].

The matrix is built from the resulting formula. For the clausal connection prover, this involves a transformation of the formula into clausal normal form. The standard transformation applies distributivity rules of the shape \(A \wedge (B \vee C) \equiv (A \vee B) \wedge (A \vee C)\) to the formula until it is in conjunctive normal form. In the worst case, this transformation makes the formula grow exponentially. To avoid this, the definitional transformation introduces new symbols [58, 63, 80]. Similarly to Skolemisation, the introduced symbols should be consistent across different problems, which is achieved by using a normalised string representation of the clause literals as new symbol names. For the nonclausal connection prover, no clausification is required, as the formula can be directly transformed into the nonclausal matrix. For both clausal and nonclausal matrices, the polarity of literals is encoded by the sign of the integer representing the predicate symbol.

The Skolemisation of a formula \(\varDelta \) replaces existentially quantified variables occurring in \(\varDelta \) by newly introduced function symbols called Skolem functions, yielding a formula equisatisfiable to \(\varDelta \) without existential quantifiers. Skolemisation may introduce distinct Skolem functions when a single Skolem function would have sufficed. For example, a subformula \(\exists x. P(x)\) of two formulas \(\varDelta _1\) and \(\varDelta _2\) may be Skolemised to \(P(s_1)\) in \(\varDelta _1\) and to \(P(s_2)\) in \(\varDelta _2\), such that \(s_1 \ne s_2\). This makes it difficult to spot in hindsight that \(s_1\) and \(s_2\) were produced from equivalent subformulas. For machine learning, however, when we learn something about a formula containing a Skolem function, such as \(P(s_1)\), we wish to transfer this knowledge to a different formula where the same formula was Skolemised to \(P(s_2)\). To solve this problem, we present a new Skolemisation method that introduces Skolem functions “consistently”. In general, a consistent Skolemisation method can instantiate different existentially quantified variables with the same Skolem functions under certain conditions. For example, a consistent Skolemisation method could ensure for the example above that \(s_1 = s_2\).

Consistent Skolemisation methods have been studied in the context of the \(\delta \)-rule in tableaux methods [6]. The Skolem terms introduced by such methods may lead to rather large formulas unless techniques such as structure sharing are used [24]. However, in our setting, such techniques would complicate the parallel execution of several prover instances and require the adaption of both the prover and the machine learning methods. We propose a new consistent Skolemisation method which produces reasonably small Skolem functions without relying on structure sharing.

We assume that the formulas in this section are in negation normal form. A position p is a sequence \(p_1 \dots p_n\), where every \(p_i\) is either 0 or 1. The empty sequence \(\varepsilon \) denotes the root position, and pq is the concatenation of two positions p and q. The subformula of F at the position p, denoted as \(F|_p\), is defined as follows: \(F|_\varepsilon = F\), and if \(F = \exists x. G\) or \(F = \forall x. G\), then \(F|_{0p} = G|_p\), and if \(F = G_1 \wedge G_2\) or \(F = G_1 \vee G_2\), then \(F|_{0p} = G_1|_p\) and \(F|_{1p} = G_2|_p\).

The sequence of free variables of F is denoted by \({{\,\mathrm{\mathcal {FV}ar}\,}}(F)\). The order of the sequence \({{\,\mathrm{\mathcal {FV}ar}\,}}(F)\) must not depend on the names of the variables; i.e. for any bijective substitution \(\sigma \), if \(\sigma F = G\), then \(\sigma {{\,\mathrm{\mathcal {FV}ar}\,}}(F) = {{\,\mathrm{\mathcal {FV}ar}\,}}(G)\). The sequence of existentially/universally quantified variables of a formula F along p is \({{\,\mathrm{\mathcal {V}ar}\,}}_Q(F, p) = \bigcup _{i < |p|} \left\{ x \mid \varDelta |_{p_1 \dots p_i} = Q x. G\right\} \), where the sequence is ordered by ascending i and \(Q \in \left\{ \forall , \exists \right\} \). For example, if \(\varDelta = \forall x. \exists y z. P(x, y, z)\) and \(p = 00\), then \(\varDelta |_p = \exists z. P(x, y, z)\), \({{\,\mathrm{\mathcal {V}ar}\,}}_{\forall }(\varDelta , p) = \left[ x\right] \), and \({{\,\mathrm{\mathcal {V}ar}\,}}_{\exists }(\varDelta , p) = \left[ y\right] \).

To describe multiple Skolemisation methods, we introduce a Skolemisation operator \(S_f(\sigma , \varDelta , p)\). This operator is parametrised by a Skolemisation function \(f(x, \sigma , \varDelta , p) =\sigma '\), which yields for a formula \(\sigma (\varDelta |_p) =\exists x. F\) an equisatisfiable formula \(\sigma ' (\varDelta |_{p0})\).² The operator \(S_f(\sigma , \varDelta , p)\) returns the f-Skolemisation of \(\sigma (\varDelta |_p)\). It follows that the f-Skolemisation of \(\varDelta \) is \(S_f(\emptyset , \varDelta , \varepsilon )\). The purpose of a Skolemisation function is to eliminate a single existential quantifier, whereas the Skolemisation operator uses the Skolemisation function to eliminate all existential quantifiers of a formula.The Skolemisation function for inner Skolemisation is \(IS(x, \sigma , \varDelta , p) = \sigma \cup \left\{ x \mapsto s(\mathbf{y})\right\} \) with s denoting a fresh Skolem function symbol and \(\mathbf{y} ={{\,\mathrm{\mathcal {FV}ar}\,}}(\sigma (\varDelta |_p))\). This performs inner Skolemisation from left to right, to avoid nesting of Skolem functions [54]. While producing small formulas, this is not a consistent Skolemisation method, as all different existentially quantified variables are mapped to different Skolem functions.

An alternative Skolemisation method uses epsilon notation [29]. The critical axiom of the epsilon calculus is \(P(t) \rightarrow P(\epsilon x. P(x))\) from which one can derive \(\exists x. P(x) \leftrightarrow P(\epsilon x. P(x))\). The Skolemisation function for epsilon-Skolemisation is then \(\epsilon S(x, \sigma , \varDelta , p) = \sigma \cup \left\{ x \mapsto \epsilon x. \sigma (\varDelta |_{p0})\right\} \). Epsilon-Skolemisation maps the subformulas \(\exists x. P(x)\) from the introductory example to the same term, namely \(P(\epsilon x. P(x))\), therefore it is a consistent Skolemisation method. However, epsilon-Skolemisation requires an extension of first-order logic. Furthermore, like previous consistent Skolemisation methods, it can yield exponentially large formulas unless structural sharing is used.

The key to obtaining a consistent Skolemisation method for our setting is to combine inner Skolemisation with epsilon-Skolemisation. We can express any Skolem term \(s(\mathbf{y})\) introduced by inner Skolemisation by some epsilon term \(\epsilon x. F\) introduced by epsilon-Skolemisation. We will show a consistent Skolemisation method that uses this correspondence, by introducing the same Skolem terms whenever their underlying epsilon terms are alpha-equivalent.

We now show how to consistently Skolemise a subformula \(\exists x. F\) of \(\varDelta \) at position p. We will refer to variables that are existentially quantified in \(\varDelta \) as existential variables and to variables that are universally quantified in \(\varDelta \) as universal variables. Our consistent Skolemisation proceeds in three steps: First, we obtain the smallest subformula \(F_{\min }\) of \(\varDelta \) that contains \(\varDelta |_p\) and contains no free existential variables. The minimality of \(F_{\min }\) serves to maximise the number of equivalent existential variables being mapped to the same Skolem function, which is important for learning. Next, we obtain the position q of \(\varDelta |_p\) in \(F_{\min }\). The idea is that encoding the combination of \(F_{\min }\) and q in the name of the Skolem function suffices to characterise \(\varDelta |_p\), allowing to reconstruct the epsilon term \(\epsilon x. F\). Finally, we obtain the arguments of the Skolem function. Putting everything together, the Skolemisation function for our consistent Skolemisation is \(CS(x, \sigma , \varDelta , p) = \sigma \cup \left\{ x \mapsto s^{F_\alpha }_{q}(\mathbf{y})\right\} \), where \(s^F_p\) denotes a first-order function symbol that carries in its name the formula F as well as the position p.

The combination of \(F_\alpha \) and q in the newly introduced Skolem function name allows the reconstruction of the epsilon term which epsilon-Skolemisation would have introduced for x. We can expand \(s^{F_\alpha }_q(\mathbf{x})\) with \(F_\alpha = \lambda \mathbf{v}_m. F_{\min }\) to its corresponding Skolem epsilon term by performing epsilon-Skolemisation of \(F_{\min }\), obtaining the epsilon term t that was introduced for the variable that is existentially quantified at position q in \(F_{\min }\), and instantiating the free variables of t by beta-reducing \((\lambda \mathbf{v}_m. \lambda \mathbf{v}_q. t) \mathbf{x}\), where \(\mathbf{v}_q = {{\,\mathrm{\mathcal {V}ar}\,}}_{\forall }(F_{\min }, q) \cap {{\,\mathrm{\mathcal {FV}ar}\,}}(F_{\min }|_q)\).

Encoding \(F_\alpha \) and q in the name of a first-order function symbol avoids dedicated procedures during proof search to decide the equivalence of Skolem functions and does not require adaptations of the machine learning methods to account for Skolem functions. The resulting Skolem function names are linear in the size of \(\varDelta \).

To find a connection with a literal L, it suffices to find a contrapositive of M with an antecedent \(L'\) such that L and \(L'\) can be unified. The consequent of the contrapositive can then be used to generate extension clauses.

The original versions of leanCoP and nanoCoP rely on Prolog’s internal literal indexing to keep a contrapositive database. We considered storing contrapositives in first-order term indexing structures [65]. However, the overall effect on the performance of storing contrapositives in a discrimination tree [25] on the considered datasets is minor, as unification with array substitutions (see below) is relatively fast. In our implementations, we store all contrapositives in a hash table indexed by the polarity and the predicate symbol of the antecedents. To find connections with a literal L, we perform two steps: First, we retrieve from the hash table all contrapositives whose antecedents have the same polarity and predicate symbol as L, and replace their free variables with fresh ones. Second, we return those contrapositives obtained in the first step whose antecedents can be unified with L.

Unification is one of the most time-consuming parts of proof search. Therefore it is crucial to represent data, including substitutions, in a way that allows efficient unification. The simplest approach to represent substitutions is to use association lists from variables to terms. This is done e.g. in the HOL Light implementation of MESON. However, as variable lookup is linear in the number of bound variables, this approach does not scale well. An improvement over this is to use tree-based maps, used for example by Metis. Both solutions however incur a significant overhead in tableaux proof search, where a single large substitution is needed. In functional languages with efficient support for arrays (e.g. the ML language family, used in many proof systems), it is more efficient to store the substitution in a single global mutable array. As variables can be represented by positive integers, the nth array element contains the term bound to the variable n. By keeping a stack of variables bound in each prover state, it is also possible to backtrack efficiently: variables removed from the top of the stack are removed from the global array. This way, backtracking can be done as if the substitution was contained in a purely functional data structure, however allowing for more efficient unification.

Proof search in connection tableaux calculi is analytic, i.e. the proof tree is constructed bottom-up. As the proof search is not confluent, i.e. making a wrong choice can lead to a dead-end, backtracking is necessary for completeness. The proof tree is constructed with a depth-first strategy, which results in an incomplete proof search. To remedy this, iterative deepening is used, where the maximal path length is increased in every iteration.

The connection provers leanCoP and nanoCoP use a number of optimisation techniques, such as regularity, lemmas, and restricted backtracking [58]. When backtracking is restricted, as soon as the proof search finds some proof tree to close a branch, no other potential proof trees for that branch are considered anymore. While restricted backtracking loses completeness, it significantly increases the number of problems solved for various first-order problem classes.

Prolog allows for a very elegant and succinct implementation of proof search. First attempts to directly integrate machine learning into Prolog leanCoP have suffered from low speed [83]. Later, [38, 41] showed that implementations of leanCoP in a functional programming language allow for fast machine learning. However, implementing proof search with restricted backtracking in a functional language is not straightforward.

In this section, we discuss several implementations of a clausal prover loop that can be adapted to use restricted backtracking: The simplified version of leanCoP shown in Sect. 3.4.1 is the smallest, but also the slowest implementation. For the sake of performance comparison, we take care that all subsequent implementations perform the proof search in precisely the same order as the original Prolog implementation. We then introduce purely functional implementations in Sect. 3.4.2 using lazy lists and streams. This version slightly increases code size compared to the Prolog version, but greatly improves performance, as shown in the evaluation in Sect. 3.5. We also discuss an approach based on continuations, still purely functional, but more complicated than the stream version. In exchange, this version has slightly better performance than the stream one, likely due to not having to allocate memory for (stream) constructors. The fastest, but also most complicated implementation considered in this paper uses an explicit stack and exceptions for backtracking. However, as it proves in our evaluation just as many problems as the continuation-based version, we will only briefly discuss it.

We evaluate the functional connection provers on several first-order problem datasets, with statistics given in Table 1:

We use a 48-core server with AMD Opteron 6174 2.2 GHz CPUs, 320 GB RAM, and 0.5 MB L2 cache per CPU. Each problem is always assigned one CPU. We run all provers with a timeout of 10 s per problem.

We evaluate several prover configurations in Table 2. As state of the art, we use the ATPs Vampire 4.0 [45] and E 2.0 [72], which performed best in the first-order category of CASC-J8 [78]. Vampire and E are written in C++ and C, respectively, implement the superposition calculus, and perform premise selection with SInE [31]. Furthermore, Vampire integrates several SAT solvers [13], and E automatically determines proof search settings for a given problem. We ran E with --auto-schedule and Vampire with --mode casc. In addition, we evaluated the ATP Metis [33]: It implements the ordered paramodulation calculus (having inference rules for equality just like the superposition calculus), but is considerably smaller than Vampire and E and is implemented in a functional language, making it more comparable to our work.

We implemented functional-style versions of leanCoP 2.1 and nanoCoP 1.0 in the functional programming language OCaml.⁷ Our implementations use the techniques introduced such as hash-based indexing and array-based substitutions (Sect. 3.3), efficient control flow (Sect. 3.4), and consistent Skolemisation (Sect. 3.2), as well as all optimisation techniques of the Prolog implementations, such as regularity, lemmas, and restricted backtracking. We refer to our functional OCaml implementations as fleanCoP and fnanoCoP, whereas we refer to the original Prolog versions as pleanCoP and pnanoCoP. The Prolog versions were run with ECLiPSe 5.10. A prover configuration containing “\(+\)x” or “−x” means that feature x was enabled or disabled, respectively. “cut” denotes restricted backtracking and “conj” stands for conjecture-directed search. leanCoP was evaluated without definitional clausification, see Sect. 3.1. The OCaml implementations use streams to control backtracking (see Sect. 3.4.2) and arrays as substitutions. As strategy scheduling is not a focus of this work, we evaluate our provers with disabled strategy scheduling.

The results are shown in Table 2: The OCaml versions outperform the Prolog versions in almost all cases (the exception being fnanoCoP−cut on the FS-msn dataset). The most impressive result is achieved by fleanCoP\(+\)cut\(+\)conj on the chainy dataset: The OCaml version proves 58.8% more problems than its Prolog counterpart, thus even passing E. Furthermore, on four out of six datasets, our strongest configuration proves more problems than Metis.

nanoCoP solves more problems than leanCoP on the datasets Miz40 and FS-msn, in both cases without cut. However, for both datasets, nanoCoP proves fewer problems than any of the reference provers Vampire, E, and Metis. In conclusion, in scenarios where both Metis and leanCoP are available, the current version of nanoCoP cannot play its theoretical strength⁸ in any of the datasets evaluated.

We evaluate different proof search implementation styles in Tables 3 and 4. Here, inferences denote the number of successful unifications performed by some prover on all problems within 10 s timeout. This metric is not available for the Prolog versions, as these do not print the number of inferences performed when prematurely terminated.

To measure the impact of the substitution structure, we evaluated the best-performing implementation, i.e. the stack-based one, using a list-based substitution instead of an array-based substitution, see Table 3. This decreased the number of inferences by 50%, showing that the performance of the substitution structure is crucial for fast proof search.

The words of the connection tableaux calculus \(\langle C, M, { Path} \rangle \) correspond to a set of tableau branches sharing the active \({ Path}\). Therefore, to characterise a branch, we use as its features the set of symbols occurring in the active path. This does not include symbols in the substitution.⁹ We weigh the symbols by the number of times they appeared in all problems, giving higher weight to rarer symbols via inverse document frequency [36], as well as by the distance between the current depth and the depth the symbols were put onto the path, giving higher weight to symbols more recently processed.

Given a set of contrapositives that are applicable in a tableau branch, we wish to obtain an ordering of the contrapositives such that trying the contrapositives in the given order minimises the time spent to find a proof. In this subsection, we show how to order the set of applicable contrapositives by a formula \({{\,\mathrm{\textsc {nb}}\,}}\) that is based on Naive Bayesian probability, as used for premise selection [40].

Adopting machine learning jargon, we will refer to contrapositives as labels, and we say that a label l co-occurred with a set of features \(\mathbf{f}\) if the contrapositive l was used in a proof branch characterised by features \(\mathbf{f}\) and l contributed to the final proof, and we say that l occurred if it co-occurred with some set of features. For this, we introduce a function F(l), which returns the multiset of sets of features that co-occurred with l, i.e. \(F(l) = \{\mathbf{f} \mid (l, \mathbf{f}) \in S\}\). The total number of times that l occurred is |F(l)|.

Let \(P(l_i, \mathbf{f})\) denote the probability that a label \(l_i\) from a set \(\mathbf{l}\) of potential labels is useful in a state characterised by features \(\mathbf{f}\). Using Bayes’ theorem together with the (naive) assumption that features are statistically independent, we deriveTo increase numerical stability, we calculate the logarithm of the probabilityIn the final formula \({{\,\mathrm{\textsc {nb}}\,}}(l_i, \mathbf{f})\) to rank labels, we modify \(\ln P(l_i \mid \mathbf{f})\) as follows:The resulting formula isThe unconditional label probability \(P(l_i)\) is calculated as follows:In practice, as the denominator of the fraction is the same for all \(l_i\), we drop it, similarly to \(P(\mathbf{f})\) above.

To obtain the conditional feature probability \(P(f_j \mid l_i)\), we distinguish whether a feature \(f_j\) already appeared in conjunction with a label \(l_i\). If so, then its probability is the ratio of the number of times \(f_j\) appeared when \(l_i\) was used to the number of times that \(l_i\) was used. Otherwise, the probability is estimated to be a minimal constant probability \(\mu \):Here, \({\mathbf{1 }}_A(x)\) denotes the indicator function that returns 1 if \(x \in A\) and 0 otherwise.

The Machine Learning Connection Prover (MaLeCoP) was the first leanCoP-based system to explore the feasibility of machine-learnt internal guidance [83]. MaLeCoP relies on an external machine learning framework (using by default the SNoW system [19]), providing machine learning algorithms such as Naive Bayes and shallow neural networks based on perceptrons or winnow cells. During proof search, MaLeCoP sends features of its current branch to the framework, which orders the proof steps applicable in the current branch by their expected utility. The usage of a general framework eases experiments with different methods, but the prediction speed of MaLeCoP’s underlying advisor system together with the communication overhead is several orders of magnitude lower than the raw inference speed of leanCoP. This was to some extent countered by fast query caching mechanisms and a number of strategies trading the machine-learnt advice for raw speed, yet the real-time performance of the system remains relatively low.

This motivated the creation of the Fairly Efficient Machine Learning Connection Prover (FEMaLeCoP), which improved speed by integrating a fast and optimised Naive Bayes classifier as shown in Sect. 4.2 into the prover [38]. Naive Bayes was chosen because learning data can be easily filtered for the current problem, making the calculation of Naive Bayesian probabilities for a given branch efficient for each applicable contrapositive. FEMaLeCoP efficiently calculates the Bayesian probabilities of a given set of contrapositives by saving statistics directly in the contrapositive database, see Sect. 3.3. Performance is further improved by updating branch features from the previous branch, instead of fully recalculating them in every new branch.

The evaluation of Naive Bayes guidance (as well as the comparative evaluation of other methods in the next section) will involve collecting training data by running leanCoP on a training dataset followed by running guided FEMaLeCoP both on training data and on a testing set. Additionally, to maximize the amount of available training data, we will split the dataset in such a way that problems that unmodified leanCoP can solve will be in the training set and unsolved problems will be in the testing set. We run both leanCoP and FEMaLeCoP on the bushy MPTP2078 dataset with a timeout of 60 s, use nondefinitional clausification, conjecture-directed search and restricted backtracking. Both leanCoP and FEMaLeCoP considered in this evaluation are implemented in OCaml using continuation passing style and array-based substitutions, see Sects. 3.4.3 and 3.3.

The original leanCoP orders the input formula so that more promising (e.g. smaller) clauses are tried earlier, see Sect. 3.1. To evaluate the ability of FEMaLeCoP to learn useful clause orders itself, we evaluate versions of leanCoP and FEMaLeCoP that either order the clauses like the original leanCoP or reverse the original order of clauses in the matrix. The latter reduces the number of proven problems compared to the default clause order.

Our evaluation proceeds as follows: We first run leanCoP on all problems. This divides our problems into a training set, namely the problems that leanCoP solves, and a testing set, namely the problems that leanCoP does not solve. From the proofs for the problems in the training set, we extract the information which contrapositive contributed in which tableau branch. We combine this information for all proofs in a format that allows efficient retrieval of learning data for given contrapositives. With the training data generated from the leanCoP proofs, we run FEMaLeCoP on both training and testing set.

The results of the evaluation with reversed and default clause order are shown in Tables 5 and 6, respectively. The \(\sum \) column shows for every prover how many problems it solved in total (i.e. the sum of training and testing problems solved by the prover). The \(\bigcup \) column shows how many problems were solved by either the underlying prover gathering data or the machine learning guided prover (i.e. the sum of training problems solved by the unguided prover and testing problems solved by the guided prover).

We detail the results of leanCoP and FEMaLeCoP without definitional clausification and with the reversed clause order. In this setting, leanCoP proves 574 problems. Running FEMaleCoP on this training set proves 550 problems, which is a loss of 4.2% compared to leanCoP. However, on the testing set, FEMaLeCoP proves 90 problems that were unsolved by leanCoP. Combining the problems from the training and testing set, FEMaLeCoP proves 640 problems, which is 11.5% more problems than solved by leanCoP, despite the fact that the inference rate of FEMaLeCoP is about 40% below leanCoP. The union of leanCoP and FEMaLeCoP proves 664 problems, adding 90 problems (15.7%) to the problems solved by leanCoP.

In comparison, when using versions of leanCoP and FEMaLeCoP that use the default clause order or definitional clausification (\(+\)def), the gain of proven problems for FEMaLeCoP is lower.

In the next section, we will show another machine learning method and compare its performance with the performance of Naive Bayesian guidance.

Monte Carlo Tree Search (MCTS) is a method to search potentially infinite trees by sampling random tree paths (called simulations) [17]. The outcome of simulations is used to estimate the quality of tree nodes, and MCTS steers search towards nodes with higher quality estimates.

We consider connection proof search as traversal of a tree that we define as follows.

The search for a proof of the word \(\langle C, M, Path \rangle \) then succeeds if we find a node \(n \in N\) with \(n_0 \rightarrow ^* n\) such that n is a closed derivation, where \((N, n_0, \rightarrow )\) is the connection proof search tree for \(\langle C, M, Path \rangle \).

Let \(\rho \in N \rightarrow {\mathbb {R}}\) be a reward function that estimates the distance of an unclosed derivation in the proof search tree from a closed derivation. Then we can use Monte Carlo Tree Search to traverse the proof search tree, giving preference to regions that yield higher rewards. For this, we first define Monte Carlo trees:

A single iteration of Monte Carlo Tree Search takes a Monte Carlo tree T and returns a new tree \(T'\) as follows¹⁰: In the next sections, we propose heuristics for the child selection policy, child probability, reward, and expansion policy.

UCT (Upper Confidence Bounds for Trees) is a frequently used child selection policy for Monte Carlo Tree Search [44]. It uses \({{\,\mathrm{\text {visits}}\,}}_T(n)\), which is the number of T-descendants of n, and \(\overline{\rho } _T(n)\), which is the average T-descendant reward of n.Given a node n, UCT ranks every T-child \(n'\) of n withHere, \(C_p\) is called the exploration constant, where small values of \(C_p\) prefer nodes with higher average descendant reward and large values of \(C_p\) prefer nodes with fewer visits. In the UCT formula, division by zero is expected to yield \(\infty \), so if a node n has unvisited children, one of them will be selected by UCT.

The UCT child selection policy \(cs_T(n)\) recursively traverses the Monte Carlo tree T starting from the root \(n_0\). \(cs_T(n)\) chooses the T-child of n with maximal UCT value and recurses unless n has no T-child, in which case n is returned:

The child probability \(P(n' \mid n)\) determines the likelihood of choosing a child node \(n'\) of n in a simulation. We show three different methods to calculate the child probability.

Several heuristics in this section require a normalisation function, for which we use a strictly increasing function \({{\,\mathrm{\text {norm}}\,}}\in [0, \infty ) \rightarrow [0, 1)\) that fulfils \(\lim _{x \rightarrow \infty } {{\,\mathrm{\text {norm}}\,}}(x) = 1\) and \({{\,\mathrm{\text {norm}}\,}}(0) = 0\). For example, \({{\,\mathrm{\text {norm}}\,}}(x) = 1 - (x + 1)^{-1}\).To measure the efficiency of a reward heuristic, we introduce discrimination: Assume that an MCTS iteration of the Monte Carlo tree T starts a simulation from the node \(n_p\) and finds a proof. Then the discrimination of T is the ratio of the average reward on the Monte Carlo tree branch from the root node \(n_0\) to \(n_p\) and the average reward of all Monte Carlo tree nodes. Formally, let the average reward of a set of nodes N beThen, the discrimination of T is

The expansion policy determines which node \(n_e\) of a simulation \(n_1 \rightarrow \dots \rightarrow n_s\) is added to the Monte Carlo tree. We implement two different expansion policies:The minimal expansion policy is similar to restricted backtracking in the sense that it restricts proof search to be resumed only from certain states, thus resulting in an incomplete search.

We implemented Monte Carlo proof search (MCPS) on top of the functional implementation of leanCoP using lazy lists, see Sect. 3.4.2.¹¹ In our implementation, leanCoP provides the search tree and MCTS chooses which regions of the tree to search. Unlike for the traditional leanCoP, the depth of the search tree is not limited. To guarantee nonetheless that simulations terminate, simulations are stopped after a fixed number of simulation steps \(s_{\max }\).

While it is possible to run MCPS from the root node until a proof is found, we found it to perform better when it serves as advisor for leanCoP. We show this in Listing 4, assuming for a simpler presentation that the default expansion policy from Sect. 5.5 is used: In line 4, initTree \(L\ { Path}\ \sigma \) creates an initial Monte Carlo tree for a connection proof search tree for the word \(\langle \{L\}, M, { Path} \rangle \) under the substitution \(\sigma \). Starting from this initial Monte Carlo tree T, mcps T constructs a (potentially infinite) lazy list of Monte Carlo iterations, with T as its head, where an iteration consists of a Monte Carlo tree and possibly a proof discovered during the simulation performed in the iteration. Of this list, we consider T and the following maxIterations elements: When maxIterations is set to 0, only T is considered and thus proof search behaves like leanCoP. When maxIterations is set to \(\infty \), the whole proof search is performed in the MCPS part. As MCPS is performed lazily, MCPS may be performed for less than maxIterations iterations when it discovers some proof contributing to the final closed derivation. Here, the lazy list characterisation introduced in Sect. 3.4.2 turns out to permit a very concise implementation as well as an easy integration of techniques such as restricted backtracking. As soon as all proofs discovered during MCPS were considered (line 5), the tree T of the final Monte Carlo iteration last mc is obtained and the children of the root of T are sorted by decreasing average T-descendant reward \(\overline{\rho } _T\) (line 6). Finally, the last applied proof step of each child is processed like in the lazy list implementation (lines 7–11).

The array substitution technique from Sect. 3.3 requires that the proof search backtracks only to states whose substitution is a subset of the current state’s substitution. However, because this requirement is not fulfilled for MCPS, we use association lists for substitutions.

To obtain suitable parameters for our heuristics, we evaluate them on the bushy MPTP2078 problems, with definitional clausification and a timeout of 10 s for each problem. Before evaluation, we collect training data for machine learning heuristics by running leanCoP with a strategy schedule on all bushy problems with a timeout of 60 s. This solves 600 problems.

The base configuration of monteCoP uses the open branches probability (see Sect. 5.3), the branch ratio reward (see Sect. 5.4), and the minimal expansion policy 1 (see Sect. 5.5), where the maximal simulation depth \(s_{\max } = 50\), the exploration constant \(C_p = 1\), and the maximal number of MCTS iterations maxIterations \(= \infty \). For any heuristic h not used in the base configuration, we replace the default heuristic with h and evaluate the resulting configuration. The results are shown in Table 7: The heuristics that most improve the base configuration are the machine-learnt closability reward and the minimal expansion policy 2.

We explore a range of values for several numeric parameters, for which we show results in Fig. 5: The maximal number of MCTS iterations maxIterations performs best between 20 and 40, see Fig. 5a: Below 20, MCTS cannot provide any meaningful quality estimates, and above 40, the quality estimates do not significantly improve any more, while costing computational resources. The exploration constant \(C_p \approx 0.75\) gives best results, where the machine-learnt closability reward achieves a local optimum, see Fig. 5b: At such an optimum, exploration and exploitation combine each other best, therefore the existence of such an optimum is a sanity check for reward heuristics (which the branch ratio reward does not pass). The maximal simulation depth \(s_{\max } \approx 20\) seems to perform best, see Fig. 5c. Above this value, the number of solved problems decreases, since the number of actually performed simulation steps decreases, as shown in Fig. 5d. This might be explained by the fact that at higher simulation depths, the computational effort to calculate the set of possible steps increases, for example because the substitution contains more and larger elements.

We adapt the base configuration to use the best heuristics from Table 7 and the best values for parameters discussed in Fig. 5, yielding \(s_{\max } =20\), \(C_p = 0.75\), and maxIterations \(= 27\). We use this improved configuration as basis for the following evaluation.

We now compare the performance of FEMaLeCoP with default clause order and the improved configuration of monteCoP obtained in Sect. 5.7. In the following, leanCoP/m and leanCoP/F refer to the leanCoP versions used to generate training data for monteCoP and FEMaLeCoP, respectively. We use the same evaluation methodology as in in Sect. 4.4: First, we run leanCoP/m and leanCoP/F on all problems for 60 s each, collecting training data. Next, to maximize the amount of available training data, we split the dataset for both leanCoP/m and leanCoP/F in such a way that problems that the respective prover can solve will be in its training set and unsolved problems will be in its testing set. Then, we run FEMaLeCoP and monteCoP on the testing sets corresponding to their respective underlying leanCoP versions, again for 60 s each.

With a timeout of 60 s, monteCoP solves 601 problems, compared to 563 solved by the best single leanCoP/m strategy, see Table 8. In comparison, FEMaLeCoP solves 592 problems, compared to 577 solved by the best single leanCoP/F strategy, see Table 6.

Figure 6 shows for any moment in time the total number of both training and testing problems solved up to that point. To this end, the testing data graph offsets the curves for monteCoP and FEMaLeCoP by the number of problems solved during training by leanCoP/m and leanCoP/F, respectively. Furthermore, we show on the training graph the number of training problems solved by monteCoP and FEMaLeCoP using training data from leanCoP/m and leanCoP/F.

On Fig. 6, we can see that despite monteCoP’s poor performance on the training set and despite the lower amount of problems solved by leanCoP/m compared to leanCoP/F, monteCoP is quickly taking the lead on the testing set compared to FEMaLeCoP. In total, the combination of leanCoP/F and FEMaLeCoP proves 627 problems, whereas leanCoP/m and monteCoP prove 653 problems. That means that in the evaluated scenario, the combination of leanCoP/m and monteCoP is more effective than leanCoP/F and FEMaLeCoP.