Implicit Learning of Common Sense for Reasoning

1 Introduction

The means of acquisition and use of common sense knowledge is a central question of Artificial Intelligence, starting with McCarthy's work [1959]. As a starting point, it is helpful to distinguish between common sense knowledge that is learned from typical experiences, and knowledge that is (at least in humans and many other animals) innate, specifically the core knowledge described by Spelke and Kinzler [2007]. We will only seek to address the learned knowledge here. Valiant [2006] has proposed that such knowledge can be formally captured by a logical syntax with a semantics derived frommachine learning, PAC-Semantics. In particular, Valiant observed that the number of rules that can be soundly learned from a given data set is exponentially large in the amount of data provided. This efficiency of the data requirements is encouraging given that existing KBs of common sense knowledge such as CYC [Lenat, 1995] and Open Mind [Stork, 1999] contain millions of rules at present and continue to grow. Here, we will seek to address a puzzle left untouched by Valiant's work, namely, how is it that a computationally limited agent can so efficiently acquire and marshal such vast stores of knowledge? We will argue that this is possible when the learning occurs only implicitly, i.e., without producing explicit representations of the learned knowledge. We will show specifically how this implicitly learned knowledge can be utilized quite efficiently in standard reasoning problems. The

∗Supported by ONR grant number N000141210358 and NSF grant number CCF-0939370. This work was done while the author was also affiliated with MIT.

(possibly exponential-size) KB itself will appear only in our analysis of a combined system for learning and reasoning.

Technically, our contribution is that we exhibit computationally efficient algorithms for reasoning under PACSemantics using both explicitly given rules and rules that are learned implicitly from partially obscured examples. As is typical for such works, we can illustrate the task performed by our algorithm with a story about an aviary. Suppose that we know that the birds of the aviary fly unless they are penguins, and that penguins eat fish. Now, suppose that we obtain a feeding log, from which we can glean that most (but perhaps not all) of the birds in the aviary seem not to eat fish. From this information, we can infer that most of the birds in the aviary can fly. Our algorithms, given the prior knowledge and partial information of the feeding log as input, will draw such a conclusion. In particular, they achieve this without being told up front that "not eating fish" is the key property that must be learned from the data; in an implicit sense, this premise is automatically picked out from among the myriad possible facts and rules that could be learned.

The conclusion that the birds of the aviary fly draws on both the empirical (partial) information and reasoning from our explicit, factual knowledge: on the one hand, our feeding log did not mention anything about whether or not the birds of the aviary could fly, and on the other hand, although our knowledge is sufficient to conclude that the birds that don't eat fish can fly, it isn't sufficient to conclude whether or not, broadly speaking, the birds in the aviary can fly. The key definition of "witnessed evaluation" of the (common sense) facts and rules is what makes this connection possible. It allows us to guarantee that we learn facts such as that the birds don't eat fish when they can almost always be verified under the partial information, and at the same time, it enables the learned facts and rules to be easily integrated into derivations in standard proof systems. The underlying definition is standard in proof complexity, but this is the first work (to our knowledge) to use it to guarantee learnability in a partial information context.

Our results show that essentially all natural tractable proof systems considered in the literature (e.g., width-bounded and treelike resolution) can also utilize knowledge that is implicitly learned from partial examples to produce PAC conclusions, without losing the tractability of the systems. The penalty for access to such implicit knowledge is essentially independent of the size of the implicit KB. We also note that the introduction of probability to cope with the imperfection of learned rules does not harm the tractability of inference, in contrast to some richer probability logics [Halpern, 1990].

It is perhaps more remarkable in from a learning theoretic perspective that our approach does not require the rules to be learned (or discovered) to be completely consistent with the examples drawn from the (arbitrary) distribution. In the usual learning context, this would be referred to as agnostic learning, as introduced by Kearns et al. [1994]. It is essential to common sense reasoning that we can detect and utilize such rules that may even possess some known counterexamples, such as "birds fly." But, agnostic learning is notoriously hard-Kearns et al. noted that even agnostic learning of clauses (over an arbitrary distribution, in the standard PAC-learning sense) would yield an efficient algorithm for PAC-learning DNF (also over arbitrary distributions), which remains the central open problem of computational learning theory. Again, by declining to produce a hypothesis, we manage to circumvent a key barrier (to the state of the art, at least).

1.1 Relationship to other work

Given that the task we consider is fundamental and has a variety of applications, other frameworks that can handle our task have naturally been proposed-for example, Markov Logic [Richardson and Domingos, 2006] is one well-known framework based on graphical models, and Bayesian Logic Programming [Kersting and De Raedt, 2008] is an approach that has grown out of the Inductive Logic Programming (ILP) community that can be used to achieve the tasks we consider here. The main distinction between all of these approaches and our approach is that these other approaches all aim to model the distribution of the data, which is generally a much more demanding task - both in terms of the amount of data and computation time required - than simply answering a query. Naturally, the upshot of these other works is that they are much richer and more versatile, and there are a variety of other tasks (e.g., density estimation, maximum likelihood computations) and/or settings (e.g., infinite firstorder domains) that these frameworks can handle that we do not. Our aim is instead to show how this more limited (but still useful) task can be done much more efficiently, much like how algorithms such as SVMs and boosting can succeed at predicting attributes for concept classes of limited scope without needing to model the distribution of the data.

In this respect, our work is similar to the Learning to Reason framework of Khardon and Roth [1997], who showed how an NP-hard reasoning task (deciding a logn-CNF query), when coupled with a learning task beyond the reach of the state of the art (learning DNF from random examples) could result in an efficient overall system. The distinction between our work and Khardon and Roth's is, broadly speaking, that we re-introduce the theorem-proving aspect that Khardon and Roth had explicitly sought to avoid. Briefly, these techniques permit us to incorporate declaratively specified background knowledge and moreover, permit us to cope with partial information in more general cases than Khardon and Roth [1999], who could only handle constant width clauses. As we noted earlier, we believe that reasoning is primarily of interest in partial information settings (cf. it is somewhat subtle to explain what the technical contribution of Khardon and Roth [1997] achieves that is not achieved by a simple estimator). Another difference between our work and that of Khardon and Roth, that also distinguishes our work from traditional ILP (e.g., [Muggleton and De Raedt, 1994]), is that as mentioned above, we are able to utilize rules that hold with less than perfect probability (akin to agnostic learning, but easier to achieve here).

2 Definitions and preliminaries

2.1 PAC-Semantics

Inductive generalization (as opposed to deduction) inherently entails the possibility of making mistakes. Thus, the kind of rules produced by learning algorithms cannot hope to be valid in the traditional (Tarskian) sense (for reasons we describe momentarily), but intuitively they do capture some useful quality. PAC-Semantics were introduced by Valiant [2000] to capture in general this quality possessed by the output of PAC-learning algorithms when formulated in a logic. Precisely, suppose that we observe examples independently drawn from a distribution over {0, 1}n ; now, suppose that our algorithm has found a rule f(x) for predicting some target attribute xt from the other attributes. The formula "xt = f(x)" may not be valid in the traditional sense, as PAC-learning does not guarantee that the rule holds for every possible binding, only that the rule f so produced agrees with xt with probability 1 - ϵ with respect to future examples drawn from the same distribution. That is, the formula is instead "valid" in the following sense:

Definition 1 ((1- ϵ)-valid) Given a distribution D over {0, 1}n , we say that a relation R is (1 - ϵ)-valid if Prx∈D[R(x) = 1] ≥ 1 - ϵ.

Of course, we may consider (1 - ϵ)-validity of relations R that are not obtained by learning algorithms and in particular, not of the form "xt = f(x)."

A number of well-known specific examples of common sense reasoning were demonstrated to be captured by learned rules by Valiant [1995] and Roth [1995], and Valiant [2006] proposed learned knowledge in general to be suitable for capturing certain kinds of common sense knowledge. The non-monotonic examples discussed by Valiant and Roth arise when we consider conditioning D on some relatively rare event, such as encountering a penguin. Tolerance to counterexamples from such rare but possible events is thus crucial for capturing common sense reasoning. We won't further consider how or when to condition on such events here. Instead, we take some such distribution as given and attempt to reason about typical examples from the distribution.

Valiant [2000] considered one rule of inference, chaining, for formulas of the form ℓt = f(x) where f is a linear threshold function: given a collection of literals such that the partial assignment obtained from satisfying those literals guarantees f evaluates to true, infer the literal ℓt. Valiant observed that for such learned formulas, the conjunction of literals derived from a sequence of applications of chaining is also (1 - ϵ′ )- valid for some polynomially larger ϵ′ . It turns out that this property of soundness under PAC-Semantics is not a special feature of chaining: generally, it follows from the union bound that any classically sound derivation is also sound under PAC-Semantics in a similar sense.

Proposition 2 (Classical reasoning in PAC-Semantics)

Let ψ1, . . . , ψk be formulas such that each ψi is (1-ϵi)-valid under a common distribution D for some ϵi ∈ [0, 1]. Suppose that {ψ1, . . . , ψk} |= ϕ (in the classical sense). Then ϕ is (1 - ϵ′ )-valid under D for ϵ′ = ∑i ϵi.

So, soundness under PAC-Semantics does not pose any constraints on the rules of inference that we might consider; the degree of validity of the conclusions merely aggregates any imperfections in the various individual premises involved. We also note that without further knowledge of D, the loss of validity from the use of a union bound is optimal.

Subsequently, we will assume that our Boolean functions will be given by formulas of propositional logic formed over Boolean variables {x1, . . . , xn} by negation and the following linear threshold connectives (which we will refer to as the threshold basis for propositional formulas):

Definition 3 (Threshold connective) A threshold connective for a list of k formulas φ1, . . . , φk is given by a list of k+1 rational numbers, c1, . . . , ck, b. The formula [∑ki=1 ciφi ≥ b] is interpreted as follows: given a Boolean interpretation for the k formulas, the connective is true if ∑i:φi=1 ci ≥ b.

Naturally, a threshold connective expresses a k-ary AND connective by taking the ci = 1, and b = k, and expresses a k-ary OR by taking c1, . . . , ck, b = 1. By using the threshold connective as our basis, we will also be able to easily demonstrate that our results apply to some numerical proof systems such as cutting planes [Cook et al., 1987], which reasons about systems of linear inequalities, and the polynomial calculus [Clegg et al., 1996] a proof system for reasoning about the common roots of systems of polynomial equations.

We note that Valiant actually defines PAC-Semantics for first-order logic by considering D to be a distribution over the values of atomic formulas. He focuses on formulas of bounded arity over a polynomial size domain; then evaluating such formulas from the (polynomial size) list of values of all atomic formulas is tractable, and in such a case everything we consider here about propositional logic essentially carries over in the usual way, by considering each atomic formula to be a propositional variable (and rewriting the quantifiers as disjunctions or conjunctions over all bindings). As we don't have any insights particular to first-order logic to offer, we will focus exclusively on the propositional case in this work.

Michael [2008] built systems based on PAC-Semantics for addressing NLP tasks, providing some concrete demonstrations of how to apply the theory. More specifically, Michael and Valiant [2008] demonstrated that chaining with rules obtained from PAC-learning algorithms improved the accuracy of algorithms for predicting missing words while Michael [2009] described an approach to textual entailment.

2.2 Partial observability

Our knowledge of a domain will be obtained from a collection of examples independently drawn from a distribution D capturing our domain, and our main question of interest will be deciding whether or not a formula is (1 - ϵ)-valid in D.

But notice, in the story about the aviary in the introduction, reasoning was only needed on account of the partial information provided by the feeding log: if it had stated whether or not the birds could fly as well, then we could have answered this query more simply by a direct examination of the data. Generally, answering queries in PAC-Semantics from complete examples is trivial: Hoeffding's inequality guarantees that with high probability, the proportion of times that the query formula evaluates to 'true' is a good estimate of the degree of validity of the formula. Recall:

Theorem 4 (Hoeffding's inequality) Let X1, . . . ,Xm be i.i.d. random variables taking values in [0, 1]. Let ¯X = 1m ∑mi=1 Xi. Then for every γ,

In such cases, reasoning per se is of no use. We were interested in using common sense facts about our domain that were learnable rules over D in reasoning, so our focus necessarily concerns situations involving both learning and partial information, building on a theory developed by Michael [2010].

Definition 5 (Partial examples) A partial example ρ is an element of {0, 1, ∗}n . We say that a partial example ρ is consistent with an example x ∈ {0, 1}n if whenever ρi ̸= ∗, ρi = xi.

Naturally, instead of examples directly fromD, our knowledge of D will be derived from a collection of partial examples drawn from a masking process over D:

Definition 6 (Masking process) A mask is a function m : {0, 1}n → {0, 1, ∗}n , with the property that for any x ∈ {0, 1}n , m(x) is consistent with x. A masking process M is a mask-valued random variable (i.e., a random function). We denote the distribution over partial examples obtained by applying a masking process M to a distribution D over assignments by M(D).

Note that the definition of masking processes allows the hiding of entries to depend on the underlying example from D.

Of course, when e.g., all attributes of our examples are hidden by the masking process, any nontrivial knowledge of our domain is surely beyond "common sense." We therefore start by only considering some facts that can be easily empirically verified, effectively by generalizing Valiant's [2000] partial information chaining rule. (Simple consequences of such empirically grounded facts will also be included later.)

Definition 7 (Witnessed formulas) We define a formula to be witnessed to evaluate to true or false in a partial example by induction on its construction; we say that the formula is witnessed iff it is witnessed to evaluate to either true or false.

• A variable is witnessed to be true or false iff it is respectively true or false in the partial example.
• ¬φ is witnessed to evaluate to true iff φ is witnessed to evaluate to false; naturally, ¬φ is witnessed to evaluate to false iff φ is witnessed to evaluate to true.
• A formula with a threshold connective [c1φ1 + · · · + ckφk ≥ b] is witnessed to evaluate to true iff

and it is witnessed to evaluate to false iff

(i.e., iff the truth or falsehood, respectively, of the inequality is determined by the witnessed formulas, regardless of what values are substituted for the nonwitnessed formulas.)

The formulas that are witnessed true with probability 1 - ϵ will be our easily verified rules: the recursive definition gives a linear-time algorithm for computing the witnessed evaluation. They will thus also be the common sense facts that we will guarantee to be learnable. We stress that such formulas may still be (witnessed, even) false with probability up to ϵ. This tolerance to a few counterexamples is essential for them to capture interesting examples of common sense facts.

A formal example of particular interest is a CNF formula. A CNF is witnessed to evaluate to true in a partial example precisely when every clause has some literal that is satisfied. It is witnessed to evaluate to false precisely when there is some clause in which every literal is falsified. If we think of the clauses as encoding implications (e.g., Horn rules), then they are witnessed true when either the head is true and unmasked, or else when one of the body literals is false and unmasked; the conjunction of these rules is witnessed true when all of the individual rules are simultaneously witnessed true. Witnessed satisfaction is also necessary for a useful CNF (for resolution) to be guaranteed to be satisfied: When a clause is not witnessed true in a partial example and does not contain a complementary pair, in the absence of background knowledge, there is always a consistent example that falsifies it. By contrast, it is of course NP-complete to determine whether a CNF can be satisfied when it is not witnessed false. The definition then only "gives up" cases where no single clause is set to false, but nevertheless no consistent assignment across all of the clauses exists. This concession is significant in some richer proof systems that we consider later, such as k-DNF resolution [Kraj´ıˇcek, 2001].

Refining the motivating discussion somewhat, a witnessed formula is one that can be evaluated in a very straightforward, local manner. When the formula is not witnessed, we will likewise be interested in the following "simplification" of the formula obtained from an incomplete local evaluation:

Definition 8 (Restricted formula) Given a partial example ρ and a formula φ, the restriction of φ under ρ, denoted φ|ρ, is a formula recursively defined as follows:

• If φ is witnessed in ρ, then φ|ρ is ⊤ ("true") if φ is witnessed true, and ⊥ ("false") otherwise.
• If φ is a variable not set by ρ, φ|ρ = φ.
• If φ = ¬ψ and φ is not witnessed in ρ, then φ|ρ = ¬(ψ|ρ).
• If φ = [∑ki=1 ciψi ≥ b] and φ is not witnessed in ρ, suppose that ψ1, . . . , ψℓ are witnessed in ρ (and ψℓ+1, . . . , ψk are not witnessed). Then φ|ρ is [∑ki=ℓ+1 ci(ψi|ρ) ≥ d] where d = b - ∑i:ψi|ρ=⊤ ci.

For a restriction ρ and set of formulas F, we let F|ρ denote the set {φ|ρ : φ ∈ F}.

Given unit cost arithmetic, restrictions are also easily computed from their definition in linear time. In a CNF that is not witnessed, the restriction simply deletes clauses that are witnessed satisfied in the partial example, and deletes the falsified literals from the remaining clauses.

2.3 Proof systems

The reasoning problems that we consider will be captured by "proof systems." Formally:

Definition 9 (Proof system) A proof system is given by a sequence of relations {Ri}∞i=0 over formulas such that Ri is of arity-(i + 1) and whenever Ri(ψj1 , . . . , ψji , ϕ) holds, {ψj1 , . . . , ψji } |= ϕ. Any formula ϕ satisfying R0 is said to be an axiom of the proof system. A proof of a formula φ from a set of hypotheses H in the proof system is given by a finite sequence of triples consisting of

1. A formula ψk
2. A relation Ri of the proof system or the set H
3. A subsequence of formulas ψj1 , . . . , ψji with jℓ < k for ℓ = 1, . . . , i (i.e., from the first components of earlier triples in the sequence) such that Ri(ψj1 , . . . , ψji , ψk) holds, unless ψk ∈ H.

for which φ is the first component of the final triple in the sequence.

Needless to say it is generally expected that Ri is somehow efficiently computable, so that the proofs can be checked. We don't explicitly impose such a constraint on the formal object for the sake of simplicity, but the reader should be aware that these expectations will be fulfilled in all cases of interest.

We will be interested in the effect of the restriction (partial evaluation) mapping applied to proofs-that is, the "projection" of a proof in the original logic down to a proof over the smaller set of variables by the application of the restriction to every step in the proof. Although it may be shown that this at least preserves the (classical) semantic soundness of the steps, this falls short of what we require: we need to know that the rules of inference are preserved under restrictions. Since the relations defining the proof system are arbitrary, though, this property must be explicitly verified. Formally, then:

Definition 10 (Restriction-closed proof system) We will say that a proof system over propositional formulas is restriction closed if for every proof of the proof system and every partial example ρ, for any (satisfactory) step of the proof Rk(ψ1, . . . , ψk, φ), there is some j ≤ k such that for the subsequence ψi1 , . . . , ψij Rj(ψi1 |ρ, . . . , ψij |ρ, φ|ρ) is satisfied, and the formula ⊤ ("true") is an axiom. 1

So, when a proof system is restriction-closed, given a derivation of a formula ϕ from ψ1, . . . , ψk, we can extract a derivation of ϕ|ρ from ψ1|ρ, . . . , ψk|ρ for any partial example ρ such that the steps of the proof consist of formulas mentioning only the variables masked in ρ. This means that we can extract a proof of a "special case" from a more general proof by applying the restriction operator to every formula in the proof. An illustration of this transformation appears in Figure 1 in the next section, where we describe how the problem in the introduction is solved by our algorithm. It turns out to be folklore in the proof complexity community that almost every propositional proof system is restrictionclosed-Beame et al. [2004] defined "natural" special cases of resolution to have this property, in particular.

1 This last condition is a technical condition that usually requires a trivial modification of any proof system to accommodate. We can usually do without this condition in actuality, but the details depend on the proof system.

We will be especially interested in special cases of the decision problem for a logic given by a collection of "simple" proofs-if the proofs are sufficiently restricted, it is possible to give efficient algorithms to search for such proofs, and then such a special case of the decision problem will be tractable, in contrast to the general case. Formally, now:

Definition 11 (Automatizability problem) Fix a proof system, and let S be a set of proofs in the proof system. The automatizability problem for S is then the following promise problem: given as input a formula ϕ and a set of hypotheses H such that either there is a proof of ϕ in S from H or else H ̸|= ϕ, decide which case holds.

A classic example of such an automatizability problem for which efficient algorithms exist is for formulas of propositional logic that have resolution derivations of constant width (first studied by Galil [1977]) using a simple dynamic programming algorithm. Essentially the same dynamic programming algorithm can be used to solve the automatizability problem for bounded-width k-DNF resolution, a slightly stronger proof system introduced by Kraj´ıˇcek [2001]. In a different strengthening, Clegg et al. [1996] showed that polynomial calculus has an efficient algorithm when the polynomials are all of degree bounded by some absolute constant d. Another example (of incomparable strength) is that treelike resolution proofs that can be derived while only remembering a constant number of clauses (i.e., of constant "clause space" [Esteban and Tor´an, 2001]) can also be found in polynomial time by a variant of Beame and Pitassi's algorithm [1996] (noted by Kullman [1999]). We also note that the special case of the cutting planes proof system [Cook et al., 1987] in which the coefficient vectors have bounded L1-norm and constant sparsity is also suitable [Juba, 2012, Section 4.3]. Our approach is sufficiently general to show that implicit learning can be added to all of these special cases.

We will thus be interested in syntactic restrictions of restriction-closed proof systems like those above. We wish to know that (in contrast to the rules of the proof system) these syntactic restrictions are likewise closed under restrictions in the following sense:

Definition 12 (Restriction-closed set of proofs) A set of proofs S is said to be restriction closed if whenever there is a proof of a formula ϕ from a set of hypotheses H in S, there is also a proof of ϕ|ρ from the set of hypotheses H|ρ in S for any partial example ρ.

It is not difficult to show that all of the syntactic special cases of the proof systems that feature efficient algorithms mentioned above are also restriction-closed sets of proofs (and as hinted at previously, this seems to be folklore). The full details for the systems we mentioned here are available in a technical report [Juba, 2012].

Algorithm 1: DecidePAC

parameter: Algorithm A solving the automatizability problem for the class of proofs S. input : Formula ϕ, ϵ, δ, γ ∈ (0, 1), list of partial examples ρ(1) , . . . , ρ(m) fromM(D), list of hypothesis formulas H output : Accept if there is a proof of ϕ in S fromH and formulas ψ1, ψ2, . . . that are simultaneously witnessed true with probability at least 1 - ϵ + γ on M(D); Reject if H ⇒ ϕ is not (1 - ϵ - γ)-valid under D. begin FAILED ← 0. foreach partial example ρ(i) in the list do if A(ϕ|ρ(i) , H|ρ(i) ) rejects then Increment FAILED. if FAILED > ⌊ϵ · m⌋ then return Reject return Accept

3 Inferences from incomplete data with implicit learning

In a given sample of data, there are potentially exponentially many possible different formulas that could be easily learned from the data. Specifically, this "common sense knowledge" consists of formulas which are easy to check for consistency with the underlying distribution by testing them on a sample of partial examples. More formally, these are formulas that are witnessed to evaluate to true on the distribution over partial examples with probability at least (1 - ϵ). We will see that it is possible to simulate access to all of these "common sense facts" during reasoning; whenever some collection of such "common sense facts" suffice to complete a proof of our query, our algorithm will accept the query. Notice that this may even include "facts" that may be witnessed false with probability up to ϵ. This is crucial if we are to draw an inference such as "birds fly" when our examples have a small but non-negligible chance of being penguins (and thus for nonmonotonic effects to appear given such rare events).

We now state and prove the main theorem. It shows that a variant of the automatizability problem, in which the algorithm is given partial examples and expected to accept queries based on proofs that invoke such "common sense knowledge," is essentially no harder than the original automatizability problem as long as the proof system is restriction-closed. The reduction is very simple and is given in Algorithm 1.

Theorem 13 (Implicit learning preserves tractability) Let S be a restriction-closed set of proofs for a restriction-closed proof system. Suppose that there is an algorithm for the automatizability problem for S running in time T(n, |ϕ|, |H|) on input ϕ and H over n variables. Let D be a distribution over examples, M be any masking process, and H be any set of formulas. Then there is an algorithm that, on input ϕ, H, δ and ϵ, uses O(1/γ 2 log 1/δ) examples, runs in time O(T(n, |ϕ|, |H|) 1 γ 2 log 1δ ), and such that given that either

• [H ⇒ϕ] is not (1- ϵ -γ)-valid with respect to D or
• there exists a proof of ϕ from{ψ1, . . . , ψk}∪H inS such that ψ1, . . . , ψk are simultaneously witnessed to evaluate to true with probability 1 - ϵ + γ over M(D) decides which case holds with probability 1 - δ.

Proof: Suppose we runAlgorithm1 onm= 1 2γ 2 ln 1δ examples drawn fromM(D). Then, (noting that we need at most logm bits of precision for ⌊ϵ · m⌋) the claimed running time bound and sample complexity is immediate.

As for correctness, first note that by the soundness of the proof system, whenever there is a proof of ϕ|ρ(i) fromH|ρ(i) , ϕ|ρ(i) must evaluate to true in any interpretation of the remaining variables consistent with H|ρ(i) . Thus, if H ⇒ ϕ is not (1 - ϵ - γ)-valid with respect to D, an interpretation sampled from D must satisfy H and falsify ϕ with probability at least ϵ + γ; for any partial example ρ derived from this interpretation (i.e., sampled fromM(D)), the original interpretation is still consistent, and therefore H|ρ ̸|= ϕ|ρ for this ρ. So in summary, we see that a ρ sampled fromM(D) produces a formula ϕ|ρ such that H|ρ ̸|= ϕ|ρ with probability at least ϵ + γ, and so the algorithm A rejects with probability at least ϵ +γ. It follows fromHoeffding's inequality now that for m as specified above, at least ϵm of the runs of A reject (and hence the algorithm rejects) with probability at least 1 - δ.

So, suppose instead that there is a proof in S of ϕ from H and some formulas ψ1, . . . , ψk that are all witnessed to evaluate to true with probability at least 1-ϵ+γ over M(D). Then, with probability 1 - ϵ + γ, ψ1|ρ, . . . , ψk|ρ = ⊤. Then, since S is a restriction closed set, if we replace each assertion of some ψj with an invocation of R0 for the axiom ⊤, then by applying the restriction ρ to every formula in the proof, one can obtain a proof of ϕ|ρ from H|ρ alone. Therefore, as A solves the automatizability problem for S, we see that for each ρ drawn from M(D), A(ϕ|ρ, H|ρ) must accept with probability at least (1 - ϵ + γ), and Hoeffding's inequality again gives that the probability that more than ϵm of the runs reject is at most δ for this choice of m.

An illustration. We now describe how Algorithm 1 solves the aviary problem described in the introduction. Suppose that in 99% of the log entries, the bird is observed to eat something other than fish; the literal expressing that a bird in question doesn't eat fish is then witnessed true in a 99% fraction of the examples. This fact, together with our prior knowledge that the penguins eat fish and that all of the birds that aren't penguins can fly, is sufficient to complete a simple treelike resolution derivation of the conclusion that the bird in question can fly (the underlying proof appears in Figure 1). We now consider the partial examples obtained from the log entries: in 99% of these partial examples, the literal expressing that the bird eats fish is (known to be) false. Under the restrictions corresponding to such log entries, one obtains a resolution derivation that only invokes the restrictions of the background knowledge clauses as premises, as illustrated in Figure 1. If we run Algorithm 1 with a query corresponding to the literal "can fly," given as input the log examples, the background knowledge clauses, and ϵ = .05, then since a proof is found in more than 95% of the examples, the algorithm accepts, concluding that (most of) the birds can fly. Theorem 13 in turn guarantees that the statistical conclusions drawn by the algorithm accurately reflect the underlying composition of the aviary if there are sufficiently many examples.

The necessity of computationally feasible witnessing. Although our choice of witnessed formulas as the "common sense knowledge" that should be learned may seem like an ad hoc choice, we note that it is merely a "base case" for the learning-that is, it follows from our requirements on the algorithms in each case that any other knowledge that follows from a simple derivation over these witnessed formulas must also be discoverable by the algorithm. Thus, for each choice of proof system, there are (potentially) different collections of formulas that the algorithm is expected to be capable of discovering. We note that in any case, we require some collection of formulas for which (1 - ϵ)-validity is computationally feasible to verify: the specification of the problem requires that if we invoke our (efficient) algorithm on a query corresponding to some "common sense fact," the algorithm must verify that it is (1 - ϵ)-valid (which may be strengthened to verification on individual partial examples [Juba, 2012, Appendix B]). Witnessed evaluation is at least a natural class of formulas for which this test is possible (and easy), whereas many other natural classes, notably the class of formulas whose restrictions are tautologies as considered by Michael [2010], may be computationally infeasible to test, and thus inappropriate for our purposes.

4 Directions for future work

A possible direction for future work raised directly by this work involves the development of algorithms for reasoning in PAC-Semantics directly, that is, not obtained by applying Theorem 13 to algorithms for the automatizability problems under the classical (worst-case) semantics of the proof systems. We will elaborate on some possible starting points next.

4.1 Incorporating explicit learning

One approach concerns modern algorithms for deciding satisfiability; a well-known result due to Beame et al. [2004] establishes that these algorithms effectively perform a search for resolution proofs of unsatisfiability (or, satisfying assignments), and work by Atserias et al. [2011] shows that these algorithms (when they make certain choices at random) are effective for deciding bounded-width resolution.

The overall architecture of these modern "SAT-solvers" largely follows that of Zhang et al. [2001], and is based on improvements to DPLL [Davis and Putnam, 1960; Davis et al., 1962] explored earlier in several other works [MarquesSilva and Sakallah, 1999; Bayardo Jr. and Schrag, 1997; Gomes et al., 1997]. Roughly speaking, the algorithmmakes an arbitrary assignment to an unassigned variable, and then examines what other variables must be set in order to satisfy the formula; when a contradiction is entailed by the algorithm's decision, a new clause is added to the formula (entailed by the existing clauses) and the search continues on a different setting of the variables. A few simple rules are used for the task of exploring the consequences of a partial setting of the variables-notably, for example, unit propagation: whenever all of the literals in a clause are set to false except for one (unset) variable, that final remaining literal must be set to true if the assignment is to satisfy the formula.

One possibility for improving the power of such algorithms for reasoning under PAC-Semantics using examples is that one might wish to use an explicit learning algorithm such as WINNOW [Littlestone, 1988] to learn additional (approximately valid) rules for extending partial examples. If we are using these algorithms to find resolution refutations, then when a refutation was produced by such a modified architecture, it would establish that the input formula is only satisfied with some low probability (depending on the error of the learned rules that were actually invoked during the algorithm's run).

Given such a modification, one must then ask: does it actually improve the power of such algorithms? Work by Pipatsrisawat and Darwiche [2011] (related to the above work) has shown that with appropriate (nondeterministic) guidance in the algorithm's decisions, such algorithms do actually find general (i.e., DAG-like) resolution proofs in a polynomial number of iterations. Yet, it is still not known whether or not a feasible decision strategy can match this. Nevertheless, their work (together with the work of Atserias et al.) provides a potential starting point for such an analysis.

A suggestion for empirical work

Another obvious direction for future work is the development and tuning of real systems for inference in PAC-Semantics. While the algorithms we have presented here illustrate that such inference can be theoretically rather efficient and are evocative of how one might approach the design of a realworld algorithm, the fact is that (1) any off-the-shelf SAT solver can be easily modified to serve this purpose and (2) SAT solvers have been highly optimized by years of effort. It would be far easier and more sensible for a group with an existing SAT solver implementation to simply make the following modification, and see what the results are: along the lines of Algorithm 1, for a sample of partial examples {ρ(1) , . . . , ρ(m)}, the algorithm loops over i = 1, . . . ,m, taking the unmasked variables in ρ(i) as decisions and checks for satisfiability with respect to the remaining variables. Counting the fraction of the partial examples that can be extended to satisfying assignments then gives a bound on the validity of the input formula. Crucially, in this approach, learned clauses are shared across examples. Given that there is a common resolution proof across instances (cf. the connection between SAT solvers and resolution [Beame et al., 2004]) we would expect this sharing to lead to a faster running time than simply running the SAT solver as a black box on the formulas obtained by "plugging in" the partial examples (although that is another approach).

4.2 Exploiting limited kinds of masking processes

Another direction for possibly making more sophisticated use of the examples in reasoning under PAC-Semantics involves restricting the masking processes. In the pursuit of reasoning algorithms, it might be helpful to consider restrictions that allow some possibility of "extrapolating" from the values of variables seen on one example to the values of hidden variables in other examples, which is not possible in general since the masking process is allowed to "see" the example before choosing which entries to mask. (Relatedly, work by Bonet et al. [2004] shows, under cryptographic assumptions, that when some attributes are always masked, the automatizability problem for systems such as bounded-depth Frege can't be solved efficiently for some distributions.) If the masks were chosen independently of the underlying examples and occasionally revealed every attribute, this might enable such guessing to be useful. Some preliminary results in this direction have been obtained when the learning problem is restricted (to learning a system of parity constraints over a uniform distribution) and the masking process decides whether to mask each attribute by tossing a biased coin: the automatizability problem for general resolution can then be decided in quasipolynomial time [Juba, 2013].

4.3 Query-driven explicit learning

A final question is whether or not it might be possible to extend Algorithm 1 to produce an explicit proof from an explicit set of formulas that are satisfied with high probability from e.g., algorithms for finding treelike resolution proofs even when the CNF we need is not 1-valid. (It is generally easy to find (1 - ϵ)-valid premises when 1-valid premises exist by simply testing for consistency with the partial examples, given bounded concealment in the sense of Michael [2010].) Although this is a somewhat ambitious goal, if one takes Algorithm 1 as a starting point, the problem is of a similar form to one considered by Dvir et al. [2012]-there, they considered learning decision trees from restrictions of the target tree. The main catch here is that in contrast to their setting, we are not guaranteed that we find restrictions of the same underlying proof, even when one is assumed to exist.

Acknowledgements

This work was heavily influenced by conversations with Leslie Valiant. I thank the anonymous reviewers for their constructive comments.