Machine Learning with Guarantees using
Descriptive Complexity and SMT Solvers
Charles Jordan∗

skip@ist.hokudai.ac.jp

Hokkaido University

arXiv:1609.02664v1 [cs.LG] 9 Sep 2016

Lukasz Kaiser

lukaszkaiser@gmail.com

Google Brain & CNRS (LIAFA)

Abstract
Machine learning is a thriving part of computer science. There are many eﬃcientapproaches to machine learning that do not provide strong theoretical guarantees, and abeautiful general learning theory. Unfortunately, machine learning approaches that givestrong theoretical guarantees have not been eﬃcient enough to be applicable.
In this paper we introduce a logical approach to machine learning. Models are represented by tuples of logical formulas and inputs and outputs are logical structures. We
present our framework together with several applications where we evaluate it using SAT
and SMT solvers. We argue that this approach to machine learning is particularly suited
to bridge the gap between eﬃciency and theoretical soundness.
We exploit results from descriptive complexity theory to prove strong theoretical guarantees for our approach. To show its applicability, we present experimental results including
learning complexity-theoretic reductions rules for board games. We also explain how neural networks ﬁt into our framework, although the current implementation does not scale toprovide guarantees for real-world neural networks.

1. Introduction
Machine learning has a long history in computer science. It includes techniques like neuralnetworks, Bayesian models, genetic programming, inductive synthesis and many others.
In various applications such as voice recognition, these methods are now used by over abillion people. Some machine learning methods give some guarantees of success, but they
are usually dependent on a number of strong assumptions about the distribution of inputs
or the existence of a model with a particular form. One would hope for much stronger
theoretical guarantees of success, but no widely used machine learning methods provide
them, so it is diﬃcult to know when they will work.
One key question faced by any machine learning system is: what kind of models will it
generate? In neural networks one asks whether the architecture is feed-forward or recurrent
and how many layers it has. In genetic programming one asks for the program representation
and which functions are built-in. In general, each machine learning system must make thischoice. If the class of generated models or programs is too broad, it might be impossible
to learn them eﬃciently. If it is too narrow, it might not suﬃce for the task at hand. To
solve a diﬀerent task, one might need a diﬀerent kind of model. But is there an eﬃcientsystematic way to know the kind of model needed for a task?
∗. Supported in part by Kakenhi Grant No. 15H00847, ‘Exploring the Limits of Computation (ELC)’.

1

There exists a number of reasonably broad machine learning methods. So one eﬃcient
way to apply machine learning to a new task is to try all of these techniques in turn. But
what if they all fail? Since there are few theoretical guarantees, it is seldom clear whether
the reason for the failure is the model, wrong parameters or simply a bug. On the other
hand, there are systematic ways to explore the space of all models that come with strong
guarantees. One can, for example, just enumerate all programs in a programming languageof choice. Of course, this is too ineﬃcient for any practical purpose.
We propose an eﬃcient way to systematically explore the space of all models in given
computational complexity class. It is based on ﬁndings from descriptive complexity where
one studies how programs in diﬀerent complexity classes, such as NL, P, or NP, can be characterized syntactically. Recent work (Crouch, Immerman, & Moss, 2010; Itzhaky, Gulwani,
Immerman, & Sagiv, 2010; Jordan & Kaiser, 2013b) suggests that logical queries of various
logics are a particularly good choice for such syntactic representations. Using logical queries
allows us, on the one hand, to exploit results from descriptive complexity to get theoreticalguarantees for our algorithms. On the other hand, it allows us to leverage recent advancesin SAT, QBF and other SMT solvers to address more practical concerns. In general, learning correct models satisfying a given condition is not computable. We ﬁrst introduce some
restrictions on the size of structures and models that we look for and present an optimized
algorithm for that restricted problem. Then, we show how to iterate these solutions to getreasonably eﬃcient semi-decision procedures with strong theoretical guarantees.
One advantage of a machine learning approach with such strong guarantees is that it cangive negative answers to certain questions. For example, our approach can sometimes provethat there is no model in a certain class that is suﬃcient for the given machine learning
task. A main disadvantage is that this does not scale to large models. Still, it can be used
to enrich our understanding of complexity theory and model classes, even when only applied
on a small scale. For example, in Section 4.1 we show how our approach can be used toprove that certain reductions between complexity classes do not exist.
The rest of the paper is organized as follows. After introducing related work, we review
the necessary background from logic in Section 2. We deﬁne our learning model and provethe main theorems in Section 3. In particular, Theorem 2 shows that if a model satisfying
the speciﬁcation exists and its computational complexity is in a given complexity class (e.g.,
NL, P, NP), then our approach is guaranteed to ﬁnd it. Knowing the theoretical guarantees,
we devote Section 4 to applications and experiments. While our technique cannot reachthe scale of machine learning systems that come with no guarantees, we show results onlearning a number of non-trivial tasks that require very diﬀerent kinds of models. We also
show how other machine learning techniques, such as neural networks, ﬁt into our approach.
1.1 Related Work
Machine learning and inductive synthesis (the subﬁeld closest to our approach) have long
histories; there is a tremendous amount of work that we do not cover. We refer the reader
to (Gulwani, 2010; Kitzelmann, 2010) for a general perspective on inductive synthesis.
Much of our motivation comes from recent papers using ideas from descriptive complexity in inductive synthesis. For example, given a speciﬁcation in an expressive logic(second-order), (Itzhaky et al., 2010) synthesized equivalent formulas in less expressive log2

ics which can be evaluated more eﬃciently. Automatically ﬁnding complexity-theoretic
reductions between computational problems was ﬁrst considered by (Crouch et al., 2010).
They focused on quantiﬁer-free reductions, a weak class of reduction deﬁned by tuples ofquantiﬁer-free formulas.
Both problems are essentially the same – ﬁnding formulas in a particular form thatsatisfy desired properties. However, the implementations are separate and not publicly
available. (Jordan & Kaiser, 2013b) compared a number of diﬀerent approaches to reduction
ﬁnding. In this paper, we introduce a more general approach – allowing the user to specify
an outline of the desired formula and a speciﬁcation that it must satisfy. We provide a freely
available implementation that can be used to experiment with various synthesis problems.
Another source of motivation for this paper comes from recent successes (Heule, Kullmann, & Marek, 2016; Konev & Lisitsa, 2015) using logic solvers to resolve interesting
problems in mathematics. In a similar fashion, determining the existence of formulas canresolve open questions and our approach gives a way to leverage modern solvers in new areas. In particular, recent progress on sequential and parallel QBF solvers suggests that thismay be a promising approach to certain problems that do not have compact SAT encodings(assuming NP6=PSPACE).

2. Background in Logic and Descriptive Complexity
In this section we brieﬂy review the necessary background from descriptive complexity.
For more details, see (Immerman, 1999) or Chapter 3 of (Grädel, Kolaitis, Libkin, Marx,
Spencer, Vardi, Venema, & Weinstein, 2007) for an overview and background, or (Grädel& Meer, 1996) and (Grädel & Gurevich, 1998) for details on R-structures and their logics.
There are many possible representations of models or programs; in this paper, we focus
on logical representations. One beneﬁt of the logical approach is that we are able to treat
structures such as graphs directly, instead of encoding them into words or numbers. This
allows us to express many interesting models succinctly. Additionally, formulas have natural
normal forms. These provide guidance for hypothesis spaces, and improve understandabilityof learned models. Also, it turns out that searching for logical formulas can be translated
to inputs for SAT and SMT solvers in a natural way.
Here, we consider models (programs) that transform given inputs into outputs and we
represent these inputs and outputs as logical structures (for example, graphs or binary
strings). Although graphs are the most common and suﬃce for many examples, they do
not provide access to computation with real numbers. Metaﬁnite structures (Grädel &Gurevich, 1998) are an extension of relational structures that was introduced to resolve
issues of this kind. We use R-structures (Grädel & Meer, 1996), a particular kind of metaﬁnite structures that provides limited access to computation with real numbers (of course,
relational structures are available as a special case). This choice is not arbitrary – there aremany deep connections between logics and complexity classes, and the relevant logics for
R-structures maintain these connections (see below or (Grädel & Meer, 1996)).
An R-signature is a tuple of predicate symbols Ri with arities ai , constant symbols cj ,and function symbols fi with arities bi :
τ := (R1a1 , . . . , Rrar , c1 , . . . , cs , f1b1 , . . . , ftbt ) .
3

A τ -structure A consists of a ﬁnite set U , called the universe, an ai -ary relation over U foreach predicate symbol of τ , a deﬁnition – an element of U – for each constant symbol, anda deﬁnition mapping U bi to R for each function symbol:(U, R1 ⊆ U a1 , . . . , Rr ⊆ U ar , c1 ∈ U, . . . , cs ∈ U, f1 : U b1 → R, . . . , ft : U bt → R).
We always set n = |U | and identify U with the natural numbers {0, . . . , n − 1}. Signatures containing no function symbols are called relational signatures and the corresponding
structures are called relational structures.
Many models make use of function symbols on the ﬁnite part U of the structure, i.e.,functions g : U ag → U . We can represent these using a predicate for the characteristic
function. One can, in a similar fashion, represent predicates with function symbols for thecharacteristic function or represent constants with monadic predicates. We use the abovedeﬁnitions for simplicity.
Example 1. The (relational) signature for directed graphs contains a single, binary predicate symbol E and so a directed graph consists of a finite set U of vertices and a binary edge
relation. These graphs may contain loops. The R-signature for a complete weighted directed
graph contains one binary function symbol e which maps pairs from U to their weights.
We denote the set of all τ -structures by Struc(τ ) and the set of τ -structures with universe
size n as Strucn (τ ). We also use the notion of an R-modification of a structure A. We saythat B is an R-modiﬁcation of a structure A, written B ∼R A, if it has the same signature,
universe, constants and relations – but it may diﬀer on the values of its real-valued functions.
Our models are built from formulas in various logics. Formulas of first-order logic overa signature τ are built in the following way. First, we ﬁx a countable set of ﬁrst-ordervariables xi – these range only over the ﬁnite part U of structures. Then, we ﬁx an explicit
enumeration of the set of algebraic real numbers and denote these constants ri . Using those,
we deﬁne the set of atomic number terms t and first-order formulas ϕ by the following BNF
grammar.
Xt := ri | fi (x1 , . . . , xbi ) | t + t | t − t | t · t | t/t | sgn(t) |t |χ(ϕ)x

ϕ := xi = xj | xi = cj | xi < xj | xi < cj | Ri (x1 , . . . , xai ) | ¬ϕ |ϕ ∨ ϕ | ϕ ∧ ϕ | ∃xi ϕ | ∀xi ϕ | t = t | t < twhere xi are ﬁrst-order variables and t are number terms. The semantics, given an assignment of the variables xi to elements ei of the structure, is deﬁned in the natural way. We
interpret sgn(a) as the sign of the real number a, i.e.

−1 if a < 0sgn(a) = 0
if a = 01
if a > 0.

P
The sum x t(x) is computed in the natural way: we compute t(x) for each assignment ofx and add them. The term χ(ϕ) stands for the characteristic function of the formula ϕ,4

i.e., it is 1 if ϕ holds and 0 otherwise. We will often use the following abbreviation:
X
X
XX
···
t :=
χ(ϕ) · t .
x1 ,...,xn : ϕ

x1

x2

xn

Note that the quantiﬁers are restricted to the ﬁnite part U of structures, and do not range
over R. We use FO to refer to ﬁrst-order logic on relational structures and FOR to refer toﬁrst-order logic on R-structures.
Example 2. Consider the signature of weighted graphs, τw := (e2 ). The first-order formula∀x, y, z (x 6= y ∧ x 6= z ∧ y 6= z)→(e(x, z) ≤ e(x, y) + e(y, z))holds exactly if the triangle inequality is satisfied by all triangles in the graph. Note that we
use “≤” and “→”; formally these are abbreviations that can be rewritten according to ourdefinition of FO.
In descriptive complexity it is very common to add additional numeric predicates tostructures. Here, we use SUC(x, y) to mean y = x + 1 and insist that structures deﬁne
this faithfully. Note that this can be deﬁned using the ordering, equality and a ﬁrst-order
quantiﬁer. However, we often consider fragments of ﬁrst-order logic where quantiﬁers are
restricted or not available, and having SUC(x, y) can be important in such situations.
2.1 Queries
Single formulas can be used to deﬁne properties or decision problems, but in general we
represent models as queries (also called interpretations). Queries map σ-structures to τ structures, deﬁning the universe, relations, constants and functions using logical formulas.
A ﬁrst-order query from σ-structures to τ -structures is an r + s + t + 2-tuple,
q := (k, ϕ0 , ϕ1 , . . . , ϕr , ψ1 , . . . , ψs , δ1 , . . . , δt ) .
The number k ∈ N is the dimension of the query. Each ϕi , ψj is a ﬁrst-order formulaover the signature σ. Let A be a σ-structure with universe U A . The formula ϕ0 has freevariables x1 , . . . , xk and deﬁnes the universe U of q(A),U := (u1 , . . . , uk ) | ui ∈ U A , A |= ϕ0 (u1 , . . . , uk ) .
That is, the new universe consists of k-tuples of elements of the old universe, where ϕ0
determines which k-tuples are included.
Each remaining ϕi has free variables x11 , . . . , xk1 , x12 , . . . , xkai and deﬁnes
n

o
Ri :=
(u11 , . . . , uk1 ), . . . , (u1ai , . . . , ukai ) | A |= ϕi (u11 , . . . , ukai ) ∩ U ai .

That is, ϕi determines which of the ai -tuples of U are included in Ri . Next, each ψi has
free variables x1 , . . . , xk and deﬁnes ci as the lexicographically minimal (u1 , . . . , uk ) ∈ Usuch that A |= ψi (u1 , . . . , uk ). Finally, each δi is a number term that has free variables
x11 , . . . , xk1 , x12 , . . . , xkbi . It deﬁnes
fi (u11 , . . . , uk1 ), . . . , (u1bi , . . . , ukbi ) := δi (u11 , . . . , ukbi ) .
5

First-order queries therefore transform σ-structures into τ -structures, and we write q(A)to represent the resulting τ -structure. The restriction to ﬁrst-order logic here is not essential– given a logic L, we deﬁne L-queries in an analogous way.
Example 3. Consider the (relational) vocabularies τS := (S 1 ) and τG := (E 2 ). We interpret τS -structures as binary strings where bit i is 1 if S(i), and τG -structures as graphs.
The following first-order query gives a simple transformation from graphs to binary strings:
qA := 2, ⊤, E(x11 , x21 ) .

Given a graph with vertices U = {0, . . . , n − 1}, this query produces a binary string withbit positions labeled by pairs (i, j) ∈ U 2 . A bit (i, j) is 1 if E(i, j). Given that we always identify universes with subsets of the naturals, we re-label these pairs lexicographicallyand the resulting string is essentially the adjacency matrix of the input graph with rows
concatenated.
One important property of queries is that they can be easily substituted when one needs
to check a formula on the resulting structure. Given a τ → σ query q, imagine we need tocheck whether q(A) |= ϕ for some σ-formula ϕ. This can be done by replacing each relation
Ri and function fj in ϕ by the appropriate deﬁnition from q and additionally guarding all
quantiﬁers to only quantify elements satisfying ϕ0 , the universe selection formula from q.
Finally, we must add quantiﬁers for each constant, deﬁning it as the minimal tuple satisfying
its deﬁning formula, and use these variables in place of the constant symbol. In this way,
we get a new τ -formula ψ such that q(A) |= ϕ ⇐⇒ A |= ψ, as formulated in the following
lemma, equivalent to e.g., Proposition 3.5 of (Immerman, 1999).
Lemma 1. Let q be a τ → σ query and ϕ a σ-formula. There exists a τ -formula q −1 (ϕ)
which satisfies, for all τ -structures A,
q(A) |= ϕ ⇐⇒ A |= q −1 (ϕ).
2.2 Extensions of ﬁrst-order logic
So far, we have focused only on ﬁrst-order logic. However, ﬁrst-order logic on ﬁnite structures is often too limited from the computational perspective – it cannot express many
interesting queries that are easy to compute. In fact, over relational structures with additional numeric predicates, the ﬁrst-order deﬁnable properties correspond exactly to uniform
AC0 (cf. (Immerman, 1999)). There are many known correspondences between logics andcomplexity classes; we introduce some of the relevant ones here.
To remove this limitation of FO, one extends it in various ways. One option is toallow quantiﬁers over relation and function symbols, resulting in second-order logic. We
use SO to refer to second-order logic restricted to relational signatures and SOR to refer tosecond-order logic over R-signatures.
Formally, formulas of SO (and SOR ) are constructed in the same way as formulas of FO(FOR ) but with the added quantiﬁers ∃Xϕ and ∀Xϕ, where X is a new relation symbol(or function symbol, in SOR ) of a ﬁxed arity r, so ϕ can now contain atoms (or terms,
for function symbols) of the form X(x1 , . . . , xr ). In SOR it is also possible to introduce
second-order variables inside terms using sup, i.e., if t is a SOR -term then so is supF t,
6

where F ranges over all functions U r → R for a given universe U .1 Relational second-ordervariable X with arity r = 0 is called a bit-variable since the atom X can only be either
true or false. Existential second-order logic is the fragment of second-order logic where all
second-order quantiﬁers are existential (while ﬁrst-order quantiﬁers are not restricted), andthe sup operator is forbidden.
Example 4. Consider the following existential SO formula on graphs:
∃R, G, B ∀x, y R(x) ∨ G(x) ∨ B(x) ∧(E(x, y) → ¬ ((R(x) ∧ R(y)) ∨ (G(x) ∧ G(y)) ∨ (B(x) ∧ B(y)))) .

This formula defines the well-known NP-complete problem of 3-colorability – each vertex
is colored red, green or blue and adjacent vertices must have different colors. Note thatmulticolored vertices are allowed, a multicolored vertex can be colored any of its individualcolors.
As this example indicates, second-order logic is very powerful; existential SO corresponds
exactly to NP (Fagin, 1974). This implies that coNP is captured by universal SO, and thatfull SO captures the polynomial-time hierarchy. The situation is similar for R-structures,
where existential SOR captures NPR (Grädel & Meer, 1996), a class analogous to NP for
computations with reals that was deﬁned by (Blum, Shub, & Smale, 1989).
However, there is a large gap between uniform AC0 and NP and it is desirable to have
logics corresponding to classes such as P. This is done by extending ﬁrst-order logic withvarious operators. For example, the transitive closure operator allows us to write formulas of
the form TC[x1 , x2 .ϕ(x1 , x2 )](y1 , y2 ). This formula takes the transitive and reﬂexive closureof the (implicit) relation deﬁned by ϕ(x1 , x2 ) and evaluates it on (y1 , y2 ). The least fixedpoint operator allows recursive deﬁnitions in formulas of the form LFP[R(x1 , . . . , xk ) =ϕ(R, x1 , . . . , xk )](y1 , . . . , yk ), where R is a new relation symbol appearing only positively(i.e., under an even number of negations) in the inner formula ϕ. The result of this operator
is deﬁned as the least ﬁxed-point of the operator R(x) → ϕ(R, x). The functional fixed-point
is deﬁned in a similar way over R-structures, see (Grädel & Meer, 1996) for details.
Example 5. Consider the following formula on graphs augmented with constants s, t:
T C[x, y.E(x, y)](s, t) .
This formula takes the transitive closure of the edge relation, and checks whether (s, t) is in
the result. That is, it defines the well-known NL-complete problem of s, t-reachability.
Example 6. Consider the following formula on weighted graphs augmented with constantss, t.
T C[x, y.e(s, s) ≤ e(x, y)](s, t) .
1. We need to introduce separate variable binding for formulas and terms because formulas and terms are
distinct in our syntax. This can be avoided by using a term-only syntax where formulas are a specialcase, as done in, e.g., (Kaiser, Lang, Leßenich, & Löding, 2015). But our syntax allows to trivially decide
when to apply propositional solvers rather than ones for the whole theory of the real field. The particular
choice of sup simplifies some later proofs, and it can be defined in SOR . From a complexity-theoretic
perspective it complicates the relationship between certain fragments and complexity classes; this could
be avoided but is not relevant to our purposes.

7This formula takes the transitive closure of the edge relation restricted to edges with weightat least e(s, s). If we call this value k, then the formula defines the property of allowing a
k-flow from s to t that is never split over multiple edges.
Over relational structures2 , polynomial time is captured by least ﬁxed-point logic (LFP)(Immerman, 1986; Vardi, 1982), and the same holds for PR and functional ﬁxed-point (FFP)(Grädel & Meer, 1996). Although LFP is presumably more expressive than transitive closure
logic (TC), TC captures all problems solvable in non-deterministic logarithmic space (NL)on relational structures (Immerman, 1987).
Of course, one can also consider extending SO with these operators; the resulting logics
capture well-known classes. See (Immerman, 1999) for an overview of logics capturing othercomplexity classes. All logics that we consider here are contained in SOR .
2.3 Outlines
Given a logic L, we refer to the set of L-formulas which may contain certain placeholders
as L-formula outlines. Intuitively, an outline ﬁxes the structure of the formula but not theexact contents.
To be precise, we allow two kinds of placeholders. First, atoms a may be guarded bysome Boolean guard 3 Gi . Intuitively, the meaning of Gi a is “a if Gi and false otherwise”.
Boolean guards suﬃce for relational signatures. In the case of R-structures, formulas cancontain real constants and it is desirable to learn these constants automatically. Thus, inaddition to the Boolean guards, we allow real placeholders wi . Intuitively, they represent
real number constants which must be found.
More formally, we deﬁne L-formula outlines as follows. We ﬁx a countable set of Boolean
guards {G1 , . . .} and a countable set of real placeholders {w1 , . . .}. Then, we deﬁne Lformula outlines exactly in the same recursive way as L-formulas and number terms, withthe following two additional rules. First, for each outline ϕ and Boolean guard Gi , Gi ϕ isalso an outline. Second, each wi is also a number term outline. Then, the set of formula
outlines and number term outlines is built in the same way as formulas and terms are built.
The Boolean guards are intended to mean “a occurs here”, and given an instantiationof the guards I, we can instantiate an L-formula outline ψ to an L-formula ψ I by replacing
each Gi a by a if Gi is true in I, and by false otherwise. Similarly, an instantiation I mustassign an algebraic real number ri to each wi to make it a number term. We refer to queries
containing L-formula outlines as L-query outlines. We omit L when it is clear from context,
and use outline to refer to both query and formula outlines. Given an outline o, we write
inst(o) for the set of formulas or queries obtainable as instantiations of o.
Note that we do not allow the dimension of the query to be a placeholder, that leads
quickly to undecidability. One could allow a ﬁnite upper-bound on the dimension, but thiscan be simulated by a ﬁnite set of outlines.
2. Recall that our structures are always ordered. The existence of a logic capturing polynomial time onunordered structures is a major open question, cf. (Grohe, 2008).
3. We do not require that identical atoms share guards, that distinct atoms have different guards, or that
all atoms are guarded.

8

Outlines are in some sense the logical equivalent to program sketches (Solar-Lezama,
Tancau, Bodik, Seshia, & Saraswat, 2006). They have advantages including immediate
upper bounds on the complexity of synthesized formulas and clear normal forms.
Example 7. Consider a structure with a single binary relation symbol E. An example
outline of a formula defining a binary relation with variables x1 , x2 without equality is:
G1 E(x1 , x1 ) ∨ G2 E(x1 , x2 ) ∨ G3 E(x2 , x1 ) ∨ G4 E(x2 , x2 ) .
Allowing equality in addition, a bit more complex example that we will use for learning
actual reductions is an outline defining a binary relation over a signature with constants s, t
and binary relation E:_
ϑ1 :=(Gab1 E(a, b) ∨ Gab2 ¬E(a, b) ∨ Gab3 a = b ∨ Gab4 a 6= b) .
a,b∈{s,t,x1 ,x2 }We can use this formula outline as part of a query outline, e.g.
q1 := (k := 1, ϕ0 := ⊤, ϕ1 := ϑ1 ) .

3. Learning Logical Queries
In this section, we introduce our model of learning logical queries. The model consistsof a learner giving candidate queries or hypotheses and a teacher (or veriﬁer), which gives
counter-examples or accepts the query. A learning task is characterized by a few parameters,
ﬁrst is the target class C.
Let C ⊆ Struc(τ ) × Struc(σ) be a binary relation on R-structures, and deﬁne the domain
of C as dom(C) = {A | (A, B) ∈ C for some B}.
In our deﬁnition of the teacher and the learner, we distinguish between the relational partof a structure and its real-valued functions. Recall that a structure B is a R-modiﬁcationof a structure A, B ∼R A, if it only diﬀers in the values of the real-valued functions, but
keeps the relational part intact. The restriction we put on the teacher and the learnerwith respect to R-modiﬁcations will become clear later, when we discuss termination of thelearning process.
Deﬁnition 1. A C-teacher t is a functiont : (τ → σ)-queries → (dom(C) × (SOR (τ ) × SOR (σ))∗ ) ∪ {⊤}that satisfies the following condition.

if {(A, q(A)) | A ∈ dom(C)} ⊆ C,⊤1
1t(q) = (A, (ϕ , ψ ), . . . A ∈ dom(C), (A, q(A)) 6∈ C, |= ∨i ϕi , for each i ≤ l :. . . , (ϕl , ψ l )) A′ ∼R A, A′ |= ϕi ⇒ (B |= ψi ⇐⇒ (A′ , B) ∈ C)

That is, a teacher accepts a query q if for all A ∈ dom(C) we have (A, q(A)) ∈ C,
and otherwise replies with a counter-example A. In addition to the counter-example, theteacher provides a sequence of formulas (ϕi , ψ i ) that deﬁnes the acceptable output on all9R-modiﬁcations of A. Note the condition |= ∨i ϕi requires that at least one ϕi holds on
every structure. For relational signatures, the deﬁnition can be simpliﬁed to returning ⊤or (A, ψ) since the only R-modiﬁcation of a relational structure is the structure itself.
For R-structures, the requirement that the teacher speciﬁes the correct behavior on
all R-modiﬁcations implies that not all classes C have a teacher. In fact the teacher can
only specify Boolean combinations of polynomial inequalities of real-valued functions fromthe structure. As a result, classes that use real numbers for advanced computations (e.g.,
encoding undecidable problems in the digits of the real numbers appearing there) do nothave a teacher in this model. We accept this limitation as our motivation for R-structures
is only to allow easy access to basic computations with quantities.
Of course, in practice we generally restrict attention even more, to computable teachersand “reasonable” classes C. A natural extension would allow the teacher to return multiple(at least one) counter-examples A to an incorrect query, but we omit this possibility forclarity of presentation.
Example 8. As a running example, we will trace the learning process for a reduction from(directed) s, t-reachability to strong connectedness. These properties can be defined in thefollowing way.
Reach := T C[x, y.E(x, y)](s, t)

AllReach := ∀x1 , x2 (T C[y, z.E(y, z)](x1 , x2 )) ,and we write GReach = {A | A |= Reach} for the set of graphs satisfying Reach, and GAllReach ,G¬Reach , and G¬AllReach analogously. The target class C is{(GReach , GAllReach )} ∪ {(G¬Reach , G¬AllReach )} .
The (general) teacher for such reductions is⊤t(q) = (A, (Reach, AllReach))(A, (¬Reach, ¬AllReach))if ∀A : A |= Reach ⇐⇒ q(A) |= AllReach
where A |= Reach ∧ q(A) |= ¬AllReach
where A |= ¬Reach ∧ q(A) |= AllReach .

Note that in general, it is uncomputable to check whether A |= Reach ⇐⇒ q(A) |=AllReach for all A.
Next, we deﬁne our learners. To shorten the deﬁnition, let us say that a query q is
consistent with the series of examples (A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ)m ) iﬀ, for each i ≤ mand each A′i ∼R Ai , it holds that if A′i |= ϕji then q(A′i ) |= ψij . Note that this is exactly therequirement from the teacher deﬁnition above.
Deﬁnition 2. Let H be a class of logical queries. An H-learner L is a function that, givena sequence of examples e = (A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ)m ), satisfies(h,L((A1 , (ϕ, ψ) 1 ), . . . , (Am , (ϕ, ψ)m )) =⊥,10h ∈ H, h is consistent with e,
if no such h ∈ H exists .

A learning task is speciﬁed by the pair (C, H).
Note that our learners must always be consistent, and they return ⊥ iﬀ there is no
consistent query in the hypothesis space. The logic used in the query is determined by H.
While Deﬁnitions 1 and 2 have some appeal from a theoretical perspective, in practicethey have a number of disadvantages. In particular, we are interested in implementing ourmodel and these deﬁnitions may not be computable, and even when they are, they stillrequire a new implementation of the teacher and learner for each learning task. In thenext subsections, we introduce a restricted and uniform learning model based on formula
outlines. Restricted uniform learners and teachers have a number of practical advantages –for example, they are computable and the learning process is guaranteed to terminate.
3.1 Restricted Uniform Learner
We begin by presenting restricted uniform learners. These are deﬁned as outline learners,
which are the following.
Deﬁnition 3. An outline learner is any H-learner such that H = inst(q) for some query
outline q.
Example 9. To complement the teacher defined in Example 8, we define an outline learnerwith H = inst(q1 ) using the outline q1 from Example 7.
The outline is uniform as it gives a compact representation of a hypothesis space, andcan even enforce certain restrictions on the query. For example, outlines can require a queryto generate an extension 4 of the structure, which is useful when searching for models togive explicit isomorphisms or satisfying solutions to SAT instances.
Outlines are also quite restricted. For example, for relational signatures, there are onlyﬁnitely-many instantiations of a query outline. It is therefore possible to simply try them
all and return a suitable one. However the following construction is preferable as it allows
to use modern eﬃcient SMT solvers.
We start the construction with a technical lemma that simpliﬁes formula outlines forevaluation on structures of a ﬁxed size. Intuitively, we build a formula ϕ|n that is in essencea QBF equivalent to ϕ on structures of size n.
Lemma 2. Let ϕ be a SOR formula outline over a signature σ and n ∈ N. For a structure
A of size n, let Ac be an extension of A by the constants {0, . . . , n − 1} with constanti interpreted as element i. There exists a SOR formula outline ϕ|n over the signatureσ ∪ {0, . . . , n − 1} such that all items below hold.
(1) For all structures A with universe of size n and all instantiations I,
A |= ϕI ⇐⇒ Ac |= ϕ|In .
(2) The guards and real placeholders in ϕ|n are the same as in ϕ.
(3) The size of ϕ|n is polynomial in n and the size of ϕ (for a fixed σ).
4. An extension of a structure is formed by adding new predicates while leaving existing predicates unchanged.

11

(4) There are no first-order quantifiers or sum terms in ϕ|n .
(5) All relational second-order quantifiers in ϕ|n are over bit-variables.
Proof. The construction of ϕ|n from ϕ proceeds inductively. FirstP order quantiﬁers are
replaced by relational second-order bit variables. For sum terms
x t we ﬁrst introduce aPsecond-order function variable to deﬁne t and then replace x t by an explicit sum overpossible x. Finally, second order relational quantiﬁers are replaced by quantifying over allbits that the actual relations can address on a structure of size n.
More formally, we set ϕ|n = ϕ for all atomic formulas ϕ and t|n = t for constant terms t
and real placeholders. We then deﬁne (¬ϕ)|n = ¬(ϕ|n ), (ϕ ∨ ψ)|n = ϕ|n ∨ ψ|n , (ϕ ∧ ψ)|n =ϕ|n ∧ ψ|n , (t = s)|n = (t|n = s|n ) and (t < s)|n = (t|n < s|n ). For guarded formulasset (Gi ϕ)|n = Gi (ϕ|n ). Analogously for terms: (s + t)|n = s|n + tn , (s − t)|n = s|n − tn ,(s · t)|n = s|n · tn , (s/t)|n = s|n /tn , and sgn(t)|n = sgn(tn ). For ﬁrst-order quantiﬁers, wedeﬁne:(∃x ϕ)|n = ∃X0 . . . Xn−1 (exactly one(Xi ) ∧ ϕ′ ) .
Here, exactly one(Xi ) is the polynomial-size propositional formula stating that exactly oneof the Xi is true, and ϕ′ is formed from ϕ|n by replacing each atom containing x, e.g.
A(x, z), with_(Xi ∧ A(i, z)) .
i∈{0,...,n−1}

Function terms, e.g., f (x, y), are replaced with

χ(X0 )f (0, y) + χ(X1 )f (1, y) + · · · + χ(Xn−1 )f (n − 1, y) .
For sum terms we deﬁne the |n operation as follows:!
XXt(x) |n = sup χ (∀x t(x) = Ft (x)) |n ·xFti∈{0,...,n−1}

Ft (i) .

Note that the summation on the right is an abbreviation and not a sum term – it is thelinear-size explicit sum of the Ft (i).
Finally a second-order relational quantiﬁer is replaced by a series of quantiﬁers over
bit-variables. For example, ∃Xϕ where X has arity 2, is replaced by∃X00 X01 . . . X0n X10 X11 X12 . . . Xnn ϕ|n .
W
Then, each atom X(x, y) in ϕ|n is replaced by i,j∈{0,...,n−1} (x = i ∧ y = j ∧ Xij ). The
properties listed in the lemma follow directly from this construction.
The proof above was done directly for SOR formulas, but it also works for operatorssuch as TC and LFP. One can convert them in various ways, for example they can bedeﬁned using second-order quantiﬁers. However – assuming the representation of formulas12can handle deﬁnitions eﬃciently – it is more eﬃcient to deﬁne each stage of the induction
in such operators in terms of the previous stage and deﬁne the initial stage using the
given formula. For a structure of ﬁxed size, such inductive deﬁnitions must halt after
logarithmically (for TC) or polynomially (for LFP) many steps, so the converted formula size
remains polynomial. The advantage of such conversion over using a second-order deﬁnitionis that we minimize the number of variables introduced.
Let us now use the above conversion to show how restricted uniform learners can becomputed in practice.
Lemma 3. Assume that we are given a τ → σ SOR -query outline q and a sequence of m
examples e = (A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ) m ) where each Ai is a finite τ -structure, each ϕji
is a SOR (τ )-formula and each ψij is a SOR (σ)-formula. We can compute a q-learner, i.e.,a function Lq satisfying:(h, h ∈ inst(q), h is consistent with e,q
L ((A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ)m )) =⊥, if no such h ∈ H exists .
Proof. We will reduce the task of ﬁnding h to the task of model-checking a second-order{+, ·} formula β(q, e) using only second-order bit-variables over the real ﬁeld (R, +, ·). Notethat ﬁrst-order quantiﬁers in this formula range over all real numbers, contrary to all formulas used elsewhere in this paper. Since second-order bit-variables can be simulated byﬁrst-order real-valued variables (e.g., by assuming the bit X is true iﬀ the corresponding variable x = 0), one can convert β(q, e) to a ﬁrst-order formula over (R, +, ·). Model-checking
ﬁrst-order formulas over the real ﬁeld is known to be computable (Tarski, 1951) and eﬃcient algorithms for this problem exist (Renegar, 1998). Importantly, SMT solvers can beapplied to check β(q, e) directly. This is more eﬃcient, since the nature of bit-variables canbe utilized in the solver. We will also ensure that the size of β(q, e) is polynomial in thesize of q and e and the maximum of the sizes of Ai .
To construct β(q, e), recall that, by deﬁnition, h is consistent with e iﬀ for each i ≤ mand each A′i ∼R Ai , it holds that if A′i |= ϕji then h(A′i ) |= ψij .
Recall from Lemma 1 that q I (A′i ) |= ψij is equivalent to A′i |= (q I )−1 (ψij ). So theconsistency condition above can be formulated as^ j
A′i |=
ϕi → (q I )−1 (ψij ) .
jRecall that the construction for q −1 (ϕ) was just a substitution of the deﬁnitions from q into
ϕ, so it also works when q is a query outline – only then q −1 (ϕ) is a formula outline. Let
therefore θi denote the formula outline that deﬁnes consistency with the i-th example:

^ j
θi =
ϕi → q −1 (ψij ) .
jWe can now equivalently reformulate our task as computing Lq such that:(q I , A′i |= θiI for all i ≤ m, A′i ∼R Ai ,q
L ((A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ)m )) =⊥, if no such instantiation I exists .
13

Now, since the size of each Ai (and so each A′i ∼R Ai ) is known, as these structures are
given, we can use Lemma 2 and instead of checking if A′i |= θi we can check if A′i |= θi ||Ai | .
Let θi′ = θi ||Ai | . Since θi has no free variables, the construction from Lemma 2 provides a
θi′ that uses no ﬁrst-order variables at all, only constants appear in its atoms. Moreover,each relational atom, which now has the form R(i1 , . . . , ir ) for i1 , . . . , ir ∈ {0, . . . , |Ai |}, hasa known truth value in A′i – it’s the same as R(i1 , . . . , ir ) in Ai since A′i ∼R Ai . So we canremove those, and we are left only with Boolean guards Gi and number terms in which allfunction terms have constants in their variables, i.e, are of the form fj (i1 , . . . , ir ). Note thatby Lemma 2 all relational second-order quantiﬁers in θi′ are already over bit-variables, but
we still need to handle second-order quantiﬁers over real-valued function terms.
Let θi′′ be the formula θi′ with each fj (i1 , . . . , ir ) replaced by a new variable namedi
xfj (i1 ,...,ir ) . These variables now range over real numbers. Also, replace each second-order
quantiﬁer over a real-valued function term, e.g., ∀fj , by a string of ﬁrst-order quantiﬁers
over the corresponding newly introduced real variables for all occurrences containing fj , e.g.,t.
∀xifj (0) xifj (1) xifj (2) . Each term of the form supfj t is similarly replaced by supxi ...xi
fj (0)

fj (n)

By Lemma 2 there are no sum terms in θi′ , and we leave terms of the form χ(ϕ) intact forthe moment. We replace each guarded formula Gi ϕ by (Gi ∧ ϕ) and we will treat the guards
Gi as free bit-variables. We also treat real placeholders as variables and all number-term
functions (+, −, ·, etc.) as ﬁrst-order functions. Note that now the formula θi′′ is in thesignature {+, −, ·, /, sgn, <, ri } with additional sup and χ operators and uses only secondorder bit-variables. Note also that the condition that for all A′i ∼R Ai holds A′i |= θiI is
equivalent to(R, +, −, ·, /, sgn, <, ri ) |= ∀xifj (i1 ,...,ir ) (θi′′ )I ,where the quantiﬁer preﬁx ranges over all newly introduced variables xifj (i1 ,...,ir ) . Let us
therefore construct the following {+, −, ·, /, sgn, <, ri }-formula:^α(q, e) =∀xifj (i1 ,...,ir ) θi′′ .
i=1,...,m

By the previous construction and the above equivalence we have(q I , (R, +, −, ·, /, sgn, <, ri ) |= α(q, e)I ,q
L ((A1 , (ϕ, ψ)1 ), . . . , (Am , (ϕ, ψ)m )) =⊥, if no such instantiation I exists .
We will convert the formula α(q, e) constructed above to an equivalent formula over theﬁrst-order theory of (R, +, ·). First, let us remove the sup and χ operators. To that end,
assume a supx r or χ(ψ) appears as a sub-term of t in an expression t = s (or t < s). Lett′ be the term t with the χ(ψ) or supx r sub-term replaced by a new variable z. In case of
χ(ψ), we replace t = s by∃z (ψ → z = 1) ∧ (¬ϕ → z = 0) ∧ (t′ = s) .
In case of supx r(x), we replace the expression t = s by∃z (∀x(r(x) ≤ z)) ∧ (∀z ′ (∀x(r(x) ≤ z) → z ≤ z ′ ) ∧ (t′ = s) .
14

After recurrently applying the replacement procedure above, we are left with a ﬁrstorder formula over −, /, sgn, <. Recall that −, /, sgn, < and all algebraic real numbers aredeﬁnable in the real ﬁeld using only · and +. We can thus write a {+, ·} formula α′ (q, e)that is equivalent to α(q, e). Let now {G1 , . . . , Gk } be the set of all Boolean guards in q
and {w1 , . . . , wl } the set of all real placeholders in this outline. Note that these are all freevariables in α′ (q, e). So we setβ(q, e) = ∃G1 . . . Gk ∃w1 . . . wl α′ (q, e) .
By the above construction, β(q, e) holds in the real ﬁeld iﬀ the assignment I of the leading
existential variables provides the q I we are searching for. So we can use an SMT solver tosolve β(q, e) and set Lq = ⊥ if it answers false and otherwise get the leading assignment
I and set Lq = q I .
The formula β(q, e) constructed in the proof above is polynomial in the size of q, e andmaxi |Ai | if one allows to use deﬁnitions inside formulas (which is allowed by all modern
solvers). Note also that if we work only on relational signatures, then there are no realvalued variables or quantiﬁers in β(q, e). Thus, it is purely a quantiﬁed Boolean formula(QBF) and there has been much recent progress in eﬃcient QBF solvers5 . SAT solvers
suﬃce for relational signatures when the entire system is existential. In many applications(see Section 4 for examples) we do not require full SOR and these more limited formalisms
can oﬀer better performance. An advantage of our approach is that in each application thecomplexity is clear from syntax and so one can automatically choose to use SAT or QBF
solvers when possible.
3.2 Restricted Uniform Teacher
Deﬁnition 4. Let C ⊆ Struc(τ ) × Struc(σ) be a target class,
PC = {(Φ1 , Ψ1 ), . . . , (Φp , Ψp )}be a finite set of formula pairs, and n ∈ N. We say that (PC , n) is a speciﬁcation of C if allof the following items hold.
(1) Each Φi is a second-order τ -formula and Ψi a second-order σ-formula.
(2) For all A ∈ dom(C), the size of A’s universe is n.
(3) dom(C) = {A | A ∈ Strucn (τ ), A |=(4) For A ∈ dom(C), (A, B) ∈ C iff
B |=

^

W

i Φi }.

Ψi .

{i|A|=Φi }5. See, e.g., the recent QBF (Lonsing, Seidl, & Van Gelder, 2016; Janota, Jordan, Klieber, Lonsing, Seidl,& Gelder, 2016) competitions.

15

Intuitively, PC is a conjunction of implications that deﬁnes the class C, i.e, the acceptablebehavior of the desired model q. Given an input structure A, if A |= Φi then we require
q(A) |= Ψi . The restriction here to structures of size n is needed to guarantee that theteacher in the following deﬁnition is computable. One could similarly restrict attention to
structures of size at most n. To specify problems without restricting the size, we say that
PC above is a uniform unrestricted speciﬁcation of C if all above items except for (2) andthe restriction to Strucn in (3) hold (we will re-visit those in subsection 3.4).
Deﬁnition 5. A uniform restricted teacher is a C-teacher for a class C that has a specification S = ({(Φ1 , Ψ1 ), . . . , (Φp , Ψp )}, n).
Note that a uniform restricted teacher is only concerned with structures of size n. Also,
recall that by Deﬁnition 1 it returns ⊤ iﬀ {(A, q(A)) | A ∈ dom(C)} ⊆ C. Given the speciﬁcation S, this condition is equivalent to saying thatfor all A ∈ Strucn (τ ), i ≤ p,

A |= Φi =⇒ q(A) |= Ψi .

Otherwise, the teacher is required to return a counter-example and a speciﬁcation of whatshould be done on R-modiﬁcations of it: (A, (ϕ1 , ψ 1 ), . . . , (ϕl , ψ l )). A uniform teacher canalways return the full speciﬁcation (Φ1 , Ψ1 ), . . . , (Φp , Ψp ) instead of a list suited to thespeciﬁc counter-example. Still, we leave the possibility to return other formulas as it might
improve the eﬃciency of learning. Note also that there may be multiple choices of a counterexample A. Any is acceptable, however the overall eﬃciency of learning may depend on the
choice.
Example 10. The teacher from Example 8 is nearly uniform – all that remains is to fix n
as any finite value and restrict the teacher to graphs of size n. Then the teacher is uniformwith specification
Tn := ({(Reach, AllReach), (¬Reach, ¬AllReach)}, n) .
We will now show that uniform restricted teachers are computable. This is easy to provefor purely relational structures: there are only ﬁnitely-many relational structures of size nwhen the signature is ﬁxed, and one can simply try them all. In practice the following
construction is preferable.
Lemma 4. Let S = (PC , n) be a specification of the class C. There exists a computableuniform restricted C-teacher tS .
Proof. The proof is similar to that for Lemma 3, and we will again construct a second-order{+, ·} formula β(q) using only second-order bit-variables and check it over the real ﬁeld
(R, +, ·). Only this time the assignment of the leading existentially quantiﬁed variables will
provide the counter-example structure A.
By deﬁnition of a uniform restricted teacher, it returns ⊤ iﬀ for all structures A of sizen and all i it holds that A |= Φi =⇒ q(A) |= Ψi . By Lemma 1 we can rewrite q(A) |= Ψi
as A |= q −1 (Ψi ) so the whole condition becomes:^Φi → q −1 (Ψi ) .
A |=
i

16

Since we are only concerned with structures of size n, let^Φi → q −1 (Ψi ) |n .
θ=i

Our task now is to ﬁnd a structure A of size n that is a model of ¬θ, or return ⊤ if no such
structure exists.
To this end, let again θ ′ be the formula θ with each fj (i1 , . . . , ir ) replaced by a newvariable named xifj (i1 ,...,ir ) that ranges over reals. Again, replace each second-order quantiﬁer
over a real-valued function term, e.g., ∀fj , by a string of ﬁrst-order quantiﬁers over thecorresponding newly introduced real variables containing fj , and similarly replace terms oft. Also, treat all number-term functions (+, −, ·, etc.) as
the form supfj t by supxi ...xi
fj (0)

fj (n)

ﬁrst-order functions. Finally, replace each relational atom Rk (i1 , . . . , ir ) by a new secondorder bit-variable XRk (i1 ,...,ir ) . In this way, the constructed formula θ ′ is in the signature{+, −, ·, /, sgn, <, ri } and uses only second-order bit-variables (and sup and χ operators).
The condition that for some structure A of size n we have A |= ¬θ is equivalent to:(R, +, −, ·, /, sgn, <, ri ) |= ∃XRk (i1 ,...,ir ) ∃xifj (i1 ,...,ir ) ¬θ ′ ;the quantiﬁer preﬁx ranges over all newly introduced bit-variables XRk (i1 ,...,ir ) and realvalued variables xifj (i1 ,...,ir ) .
Similarly as in the proof of Lemma 3, we use the fact that −, /, sgn, < and all algebraic
real numbers are deﬁnable in the real ﬁeld using only · and +, and that sup and χ canbe deﬁned as well. Substituting these deﬁnitions into the formula on the right-hand side
above yields the {+, ·}-formula β(q) which we then solve using an SMT solver. If there is
no solution, the teacher tS (q) returns ⊤. Otherwise, the SMT solver provides a witness forthe outermost quantiﬁed variables XRk (i1 ,...,ir ) and xifj (i1 ,...,ir ) . We construct the counterexample structure A of size n by putting (i1 , . . . , ir ) ∈ Rk if XRk (i1 ,...,ir ) is set to true, andsetting fj (i1 , . . . , ir ) = xifj (i1 ,...,ir ) (if some tuple is not quantiﬁed at all, we can set it to any
number, e.g., 0). By the construction above, the reconstructed structure A satisﬁes ¬θ andis thus a counter-example, as required. So we set tS (q) = (A, PC ) in this case.
While a general learning task is deﬁned by (C, H), a uniform restricted learning task isgiven by a speciﬁcation and outline: ((PC , n), q).
Example 11. To continue Example 8, our (uniform restricted) reduction learning task forstructures of size n is (Tn , q1 ), where Tn is from Example 10 and q1 from Example 7. We
will see in Example 12 in Subsection 4.1 that one can learn a correct reduction for thisexample, using the specification and techniques presented above.
3.3 Termination of Uniform Restricted Learning
Let L be a learner and t a teacher. We deﬁne the sequence Lti of the interactions between L
and t inductively as follows. We set Lt0 := L(), the hypothesis that L returns on an empty
list of examples. If for some i we get Lti = ⊥ then the sequence is ﬁnished – there is noh ∈ H that satisﬁes the teacher. Else, let Ei := t(Lti ) be the answer of the teacher to Lti . If
17

Ei = ⊤ the sequence Lti is ﬁnished, the last hypothesis was accepted. In the other case, set
Lti+1 = L(E0 , . . . , Ei ).
An outline learner is, essentially, a learner with a uniform hypothesis space and a uniform
restricted teacher is a uniform way of producing correct counter-examples. In the proofs
for Lemmas 3 and 4 we saw how to convert the main conditions of outline learners anduniform restricted teachers into model-checking on (R, +, ·). This can be solved, and so we
can guarantee an alternating sequence of consistent hypotheses and counter-examples.
One concern is that we would like for the above sequence to terminate, i.e. to know afterﬁnite time whether there is an instantiation of the query outline that satisﬁes the teacher.
While this is usually not achievable in the most general case, it is always guaranteed foroutline learners and uniform restricted teachers.
Theorem 1. Let S be a specification of a class C, tS the uniform restricted teacher from
Lemma 4, and L an outline learner for some SOR -query outline q. All of the following
items hold.
(1) L is a consistent and conservative inst(q)-learner.
(2) If tS (h) = ⊤ for some h ∈ inst(q) then the sequence LtiS is finite and its last element gsatisfies tS (g) = ⊤.
(3) If there is no h ∈ inst(q) for which tS (h) = ⊤ then the sequence LtiS is finite and its
last element is ⊥.
Proof. The fact that L is a consistent and conservative inst(q)-learner, as well as the correctness of the sequence LtiS follows directly from the deﬁnitions. The only remaining thing is toshow that the sequence LtiS is ﬁnite. But note that there are only ﬁnitely-many τ -structuresof size n with diﬀerent R-modiﬁcations. Given that each outline must hold on all previous
counter-examples (by Deﬁnition 2) and each next example must be a counter-example (byDeﬁnition 1), the sequence must terminate after ﬁnitely-many steps.
For a given speciﬁcation S and query outline q, we will write L(S, q) for the last elementof the sequence LtiS considered above (which is well deﬁned, since the sequence is ﬁnite).
Note that the proof above relies on the condition we imposed on teachers and learners
that all R-modiﬁcations of a structure are handled simultaneously in each step. It is easy
to imagine a simpler learning deﬁnition, where in each step the teacher only has to respondwith a single R-structure and a condition applicable only to this structure, not all of its
R-modiﬁcations. The learner would then construct a hypothesis correct only for thesestructures.
We did not use this simple model exactly because learning might not terminate. Consider
structures of size 1, i.e., with only one element 0, and only a single real-valued function f .
Imagine an outline r > f (0) with a single real placeholder r. Intuitively, the learner seeks anumber r greater than the value f (0) in the structure. For any ﬁnite sequence of examples
A1 , . . . , Am , the learner will easily ﬁnd such an r = maxi≤m f Ai (0)+1. But then, the teacher
can respond with another example Am+1 where f (0) = r + 1. This would clearly result in
an inﬁnite learning sequence. Observe that the condition on R-modiﬁcations prevents thisbehavior: the learner will be forced to answer ⊥ already in the ﬁrst step, as there is no r
bigger than all numbers f (0).
18

3.4 Unrestricted Uniform Learning
In the previous two subsections we presented a restricted learning model that can exploit
the eﬃciency of SMT solvers. Let us now show how to iterate the use of this model to get anunrestricted one. Theorems from descriptive complexity will provide strong guarantees forthis unrestricted learning model. To this end, we need to say when a sequence of outlines
covers a logic L.
Deﬁnition 6. Let Q = {q1 , q2 , . . .} be a sequence of query outlines in a signature σ and let
L be a logic. We say that Q covers L if for every σ-outline q from L, we have inst(q) ⊆∪qi ∈Q inst(qi ) .
The deﬁnition above does not make any assumptions about computability of Q, but inpractice we will only use sequences Q that are easily enumerable. It is the advantage of
our logic approach that such sequences can easily be found by taking advantage of normal
forms of formulas.
For example, consider a query outline qji that consists of i disjunctions of j conjunctionsof guarded atoms or guarded negated atoms from the signature σ. The sequence Q0 = {qji |i, j ∈ N} consists of all outlines of formulas in DNF. Since every quantiﬁer-free formula canbe converted to DNF, we know that Q0 covers all quantiﬁer-free formulas. Similarly, we canconstruct Q1 by enumerating quantiﬁer preﬁxes and putting them in front of formulas fromQ0 . Since every ﬁrst-order formula has a prenex normal form, we get that Q1 covers FO.
Putting a least ﬁxed-point operator in front of formulas from Q1 gets us the set Q2 thatcovers LFP, because all LFP formulas have a normal form with just one LFP operator in
the front. In the next section, we will show a few sequences of query outlines that worked
well for practical applications.
Given a restricted speciﬁcation S and a sequence of query outlines Q = {q1 , q2 , . . . }, we
can run the restricted learning procedure and compute ﬁrst L(S, q1 ). If it is not ⊥ then,by item (2) of Theorem 1, L(S, q1 ) is the solution for S. Otherwise, since L(S, q1 ) = ⊥, weproceed to consider q2 , q3 , and so on. If Q covers a logic L and S has a solution in L, thenit will ﬁnally be found, since our procedure is complete. We write L(S, Q) = L(S, qi ) for
the smallest i for which L(S, qi ) 6= ⊥ and L(S, Q) = ⊥ otherwise.
Consider now an unrestricted speciﬁcation PC of a class C, and let Sn = (PC , n) be its
restriction to structures of size n. If q ∈ Q is the ﬁrst query from Q that is an unrestricted
solution for PC , then the sequence L(Si , Q) will stabilize on q from some i on. We only geta guarantee that it is correct on structures of size i and below, but in practice it seems thatqueries that are correct on moderately sized examples are usually correct in general (where“moderate” depends on the complexity of the query). In addition, the following theorem
shows that if a solution exists in the complexity class we consider and we use a suitablesequence of query outlines, then we will eventually converge to a correct solution.
Theorem 2. Let Q be a sequence of query outlines covering FO (FO(TC), FO(LFP), FFP,
existential SO, existential SOR ). Assume PC is an unrestricted specification of a class C andthat there exists a solution f for C (i.e. (A, f (A)) ∈ C for all A) that is in the complexity
class uniform-AC0 (NL, P, PR , NP, NPR ). Then L((PC , i), Q) 6= ⊥ for each i and for somek holds(A, L((PC , l), Q)(A)) ∈ C for all A and l ≥ k,19

i.e., L((PC , l), Q) is a solution for C for all l ≥ k.
Proof. By theorems from descriptive complexity cited in Subsection 2.2, if C has a solution
f in uniform-AC0 (NL, P, PR , NP, NPR ), then there exists a query q in FO (FO(TC),
FO(LFP), FFP, existential SO, existential SOR ) that is also a solution for C. Since Q
covers this logic, we know that there exists a solution qi ∈ Q.
Let Sn = (PC , n). Since qi is a solution for the unrestricted class C, it is also a solution
for Sn . So L(Sn , Q) 6= ⊥ since it will stop at qi at the latest. Also, for each j < i such thatqj is not a solution for C, there exists a counter-example for qj of size nj . Let k = maxj<i nj .
By Theorem 1 we will discard all false qj in L(Sl , l) for all l ≥ k, and thus return a generally
correct solution.

The above theorem provides strong guarantees for our learning method: if a solution
exists, even in a broadly-deﬁned complexity class such as P or NP, then it will be found.
The question remains whether this is a practical method. In the next section, we examinevarious learning tasks, look for reasonable teachers and outline sequences, and show thatwith modern SAT, QBF and SMT solvers this method can indeed be practically applied.

4. Applications
As described above, the learning problem in our model consists of the speciﬁcation of theteacher and the outline for the learner. For diﬀerent learning tasks, it might be advantageous to choose diﬀerent outlines. For example, some tasks might only require a very
simple Boolean circuit to solve, while for other we might need the full power of polynomial
time programs with loops and intermediate deﬁnitions. In this section we introduce a few
parametrized classes of outlines with increasing computational power. With each class ofoutlines, we present a sample learning task that is well suited for this outline and discuss
how the task is solved in our model.
We start with outlines for very simple quantiﬁer-free ﬁrst-order formulas. It turns outthat even such basic outlines are useful: they are a good candidate for ﬁnding reductions, as
we discuss in the next section. After that, we move to ﬁrst-order outlines. These correspondto uniform AC0 circuits and we show that they can be used for learning patterns and rules
on relational structures, and even rules for board games. Next, we discuss how thresholdcircuits can be encoded in our model. Threshold gates allow to build neural networks and weshow how such networks can be represented in our model. Finally, we present outlines withﬁxed-point operators. Such outlines can encode complicated polynomial-time programs andare hard to learn. We present a few experiments where simple programs with loops anddeﬁnitions are successfully learnt in our model.
We focus here on examining how these sample applications can be achieved in our model,
in order to see that a variety of natural learning tasks can be modeled. Subsections 4.1
and 4.2 contain comparisons to existing, alternative approaches and show that our methods
are competitive. Subsections 4.3 and 4.4 are primarily intended to show the range of ourapproach and do not contain exhaustive experimental results.
20

4.1 Learning Quantiﬁer-Free First-Order Formulas
Complexity-theoretic reductions are an important tool to determine the relative hardnessof computational problems and other applications exist. For example, SAT solvers are
now commonly used as general NP solvers and the necessary transformations are generally
reductions. This naturally leads to the question of (automatically) learning and verifying
reductions.
Learning reductions was ﬁrst considered by Crouch et al. (Crouch et al., 2010), and wehave also (Jordan & Kaiser, 2013b) implemented, benchmarked and evaluated a number ofdiﬀerent approaches to the problem.
Problem In descriptive complexity, a reduction from the τ -property deﬁned by ϕ to theσ-property deﬁned by ψ is a (τ → σ)-query q that satisﬁes
A |= ϕ ⇐⇒ q(A) |= ψ(1)for all τ -structures A. Of course, reductions should have less computational power thanthe complexity classes they are used in and descriptive complexity usually focuses on weakclasses of reductions, such as ﬁrst-order reductions (i.e., ﬁrst-order queries as reductions).
Here, we study quantiﬁer-free ﬁrst-order reductions, an even weaker class that still suﬃces
to capture important complexity classes. While polynomial time or logspace reductions aremost common, such power is usually not necessary for reductions and only causes additionaldiﬃculties (Agrawal, 2011; Agrawal, Allender, Impagliazzo, Pitassi, & Rudich, 2001; Veith,1998). Here we introduce learning reductions in the context of our model, see (Jordan &Kaiser, 2013b) for more details, other approaches and experimental comparisons.
In order to make ﬁnding quantiﬁer-free reductions decidable, we restrict attention toa ﬁxed size n, i.e., we require Formula (1) to hold only for structures of size at most n.
Assume that we are searching for a dimension-k reduction from the τ -property deﬁned by
ϕ to the σ-property deﬁned by ψ.
Let P be the set of τ -structures of size at most n that satisfy ϕ, Q be the set of σstructures of size at most nk that satisfy ψ, and P and Q be their complements up to thesize bounds. Our target class is C = (P × Q)∪ (P × Q) – we want a query that maps positive
instances to positive instances and negative instances to negative instances.
Outline As an outline, we focus on reductions in which all formulas are in DNF with cconjunctions. We ﬁx ϕ0 to be always true and the dimension k (so the new universe is theset of k-tuples of elements of the old universe). Finally, we have a number of parameters
determining the atomic formulas that may occur – for example, whether to allow certain
numeric predicates such as successor.
Teacher

When the teacher receives a candidate hypothesis q, it checks Formula (1), i.e.

A |= ϕ =⇒ q(A) |= ψ∧

A 6|= ϕ =⇒ q(A) 6|= ψ

for all structures A of size at most n. The teacher returns (A, ψ) if A |= ϕ and (A, ¬ψ)otherwise.
21

(c, n)de-gmsrareqsdepqbfgringolparseRedFind(1, 3)
0
0
0
40
51
1

(2, 3)
0
0
142
393
396
152

(3, 3)
10
16
547
590
605
396

(1, 4)
0
19
16
72
75
2

(2, 4)
5
65
297
593
635
347

(3, 4)
103
204
711
836
850
547

Table 1: Number of timeouts for tested reduction ﬁnding approaches, k = 1.
Results See (Jordan & Kaiser, 2013b) for an extended comparison of our approach using
various SAT, QBF, ASP and BDD packages, along with the earlier system developed by
Crouch et al. (Crouch et al., 2010). Here we present a short summary of the results.
Learning quantiﬁer-free reductions (with the restrictions described above) between problems in NP ∩ coNP is essentially a Σ2p problem. Therefore it can be solved using a reasonablesized encoding and single call to either a QBF solver or ASP solver supporting disjunctive
programs. We therefore compare our approach with modern QBF and ASP solvers.
We refer to (Jordan & Kaiser, 2013b) for precise details and an extended experimental
comparison of various approaches to this problem. In particular, there we present an opensource implementation (DE6 ) of our approach specialized to reduction-ﬁnding. QBF and
ASP instance generation is done using ReductionTest.native (part of Toss, see (Jordan& Kaiser, 2013a) for details)7 .
Table 1 considers a set of 48 decision problems in NL (including e.g. directed andundirected reachabililty, but also several simpler problems) and presents results for all
2304 = 482 reduction-ﬁnding problems constructed between these problems. These 48
decision problems are from the ReductionFinder implemented by Crouch et al. (Crouch
et al., 2010) and therefore allow us to compare with ReductionFinder as well. However,ReductionFinder considers a slightly diﬀerent class of reductions, generally resulting insomewhat simpler instances. A fair comparison is therefore diﬃcult and ReductionFinder
is included for completeness. The timeout was set to 120s in Table 1.
We see that our approach, along with the QBF solver rareqs, are the best among
these choices. Interestingly, rareqs is an expansion-based QBF solver (Janota, Klieber,Marques-Silva, & Clarke, 2012) and so in this case it essentially functions like our approachby reﬁning a series of hypotheses (abstractions) using counter-examples.
While the parameters used in Table 1 result in comparatively easy instances, extended
experiments with more diﬃcult parameters give similar results, cf. (Jordan & Kaiser, 2013b).
In addition, the teacher in Table 1 considers only counter-examples of size exactly n. Allowing counter-examples of size at most n greatly improves performance of our approach –very small counter-examples result in easy sub-problems that tell us a great deal about the
space of possible solutions.
6. Available at http://www-alg.ist.hokudai.ac.jp/~ skip/de, configured as de-gms using GlueMiniSat
2.2.5 as solver. Equivalent functionality is available as part of Toss: http://toss.sf.net/ and a visualinterface is also available at http://toss.sf.net/reduct.html
7. The input files used in this section are available at http://toss.sf.net/reductGen.html

22

Example 12. We complete our running Example 8 here. Recall that the task was to finda reduction between two NL-complete problems: directed s, t-reachability (given a directed
graph with labeled vertices s and t, determine whether t is reachable from s) and all-pairs
reachability (determine if a directed graph is strongly connected). The problems were definedby these 2 formulas.
Reach := T C[x, y.E(x, y)](s, t)

AllReach := ∀x1 , x2 (T C[y, z.E(y, z)](x1 , x2 )) .

We were searching through the space of outlines as described above, and structures of increasing sizes. Our system finds the following correct reduction for outline q1 as in Example 7
and sizes n ≥ 3:
(k := 1, ϕ0 := true, ϕ1 := x1 = s ∨ x2 = t ∨ E(x2 , x1 )) .
This reverses all edges in the original graph, adds directed edges from s to all vertices andalso adds directed edges to t from all vertices. A similar reduction exists without reversing
the edges – however the above is our actual output.
4.2 Learning First-Order Formulas
Recently, a system was implemented (Kaiser, 2012) that represents board games as relational structures and learns their rules from observing example play videos. Fundamentally,
the system works by computing minimal distinguishing formulas for sets of structures, e.g.,
formulas satisﬁed by structures representing winning positions and by none of the losing
ones. We implement the computation of distinguishing formulas in our framework andcompare the performance.
Problem Let P and N be ﬁnite sets of τ -structures. We want to learn a formula ϕ
without free variables such that A |= ϕ for all A ∈ P and for no A ∈ N . Unlike previous
tasks, we want a minimal such formula, not just an arbitrary one.
Outline and Teacher The outlines in this case are not quantiﬁer-free any more, butthey are built by adding quantiﬁer preﬁxes to quantifer-free outlines similar to the ones
used above. In this case, we start with a CNF formula with c clauses and k additionalvariables. Then, we quantify the k additional variables existentially. The ﬁnal outline isthen a disjunction of l such quantiﬁed CNF formulas, each with k added variables and at
most c clauses. Moreover, to ﬁnd minimal formulas we iterate through k, for each k we
range l from 1 to k + 1, and c as well. The teacher is simple: given a formula ϕ it checks
if A |= ϕ for all A ∈ P, and if not, it returns (A, true) for some A 6|= ϕ. Then, it checks if
A 6|= ϕ for all A ∈ N and returns (A, false)8 if this is not the case for some A |= ϕ.
Results We substituted our SAT-based learner for the procedure for computing distinguishing formulas used in (Kaiser, 2012). To replicate the experiments, we used the mostrecent revision of Toss9 and ran each experiment 3 times on a 4Ghz Intel i7-4790K processor.
8. Here, “true” and “false” are satisfied by encoded Boolean structures.
9. Revision 1935 on Sourceforge, compiled with OCaml 4.02.1.

23

Since the variance in time was negligible, we only report the mean running time.10 Comparing the results, the SAT-based approach appears to oﬀer signiﬁcantly better performance,even though it is more general and competes against a system hand-crafted speciﬁcally forthis problem.
Original system
SAT-based system

Breakthrough39s
2s

Connect4
14s
5s

Gomoku4s
2s

Pawn-Whopping
473s
130s

We use the same example plays for both systems – these examples were chosen by handfor the original system (Kaiser, 2012). But our SAT-based approach searches (faster) for
formulas in more expressive logics, beyond reach for the original system. For this reason,
the resulting formulas are not always correct – they are for Breakthrough and Gomoku,
but not for Connect4 and Pawn-Whopping. It would be easy to overcome this by adding
examples or changing the outline to match the more restrictive logics used by the original
system.
4.3 Learning Threshold Circuits (Formulas with Reals)
Let us now show how neural networks can be represented in our model. We will focus on
deep convolutional networks, but the ideas generalize to other models easily.
Convolutional neural networks share weights using sliding windows over the input vector
and often alternate such shared-weights-layers with max-pooling layers which just compute
maximum over a window to reduce the number of neurons and, more importantly, to capture
diﬀerent scales, e.g. in image recognition. In the convolutional layer, each neuron is aso called rectified linear unit. This means that each neuron multiplies its inputs by therespective weights, adds the result, subtracts another weight, and sends to its output the
maximum of this result and 0.
...

max
w

w

...

max
w

w

...
window of 4

The ﬁgure above sketches a convolutional network. We wrote w in each neuron toemphasise that the same weight vector is used in all neurons in this layer. For visionapplications, the sliding window and max-pooling window can be 2D, e.g. 3 × 3. For
classiﬁcation, there is often a fully-connected layer before the output layer. All these can be
encoded in our formalism in an analogous way, so we focus on 1D convolutional networks.
The input to a 1D network is a n-bit vector of real numbers. We represent it as arelational structure over U = {0, . . . , n − 1} with a unary function f0 , such that f0 (i) is theith component of the input vector.
10. To replicate, after getting Toss, do make Learn/LearnGameTest.native and then LearnGameTest.native-dir Learn/examples/ -f Breakthrough001, or Connect4001, etc. for the original results, and with -s
to use our SAT solver technique.

24

To keep our reduction simple, let us assume our network has two convolutional layerswith a window of size 3 and two maps each, with one max-pooling layer in between. The
outline we provide for this network generalizes in an easy way to other network architectures.
By deﬁnition, the output of the ith neuron of the ﬁrst map of the ﬁrst convolutional
layer, which we denote f11 (i), is given by
f11 (i) = max(0, w11 · f0 (i) + w21 · f0 (i + 1) + w31 · f0 (i + 2) − w01 ).
In our formalism, we can write max(0, t) as t · χ(t > 0), so let us use max as a more readable
shorthand. We can formalize the above as follows:X
w11 · f0 (x) + w21 · f0 (y) + w31 · f0 (z) − w01  .
f11 (x) = max 0,y,z:SUC(x,y)∧SUC(y,z)

Note that w01 , w11 , w21 , and w31 are now the real placeholders of our outline. We deﬁne
f12 analogously with wi2 (i = 0,. . . ,3) and get the 2 maps of the ﬁrst convolutional layercomplete in this way.
However, we must still construct the max-pooling and following layer, where there arefewer neurons due to the scaling eﬀect of max-pooling. This is done by skipping every otherelement. Let us ﬁrst deﬁne the max-pooling outputs:Xi
f1i (y)
fm(x) = max f1i (x),y:SUC(x,y)

for i = 1, 2. Let SUC2 (x, y) := ∃z(SUC(x, z) ∧ SUC(z, y)). We create the second convolutional layer by skipping over every other element.
f2i (x) = max 0,

X

1
1
1
w12 · fm(x) + w22 · fm(y) + w32 · fm
(z)+y,z:SUC2 (x,y)∧SUC2 (y,z)
222w42 · fm(x) + w52 · fm(y) + w62 · fm(z) − w0!

.

Now, we can trivially make a query that selects even elements from our input structure anduses f21 and f22 as functions. It represents exactly the output of the second convolutional
layer in a network.
As we have seen, neural networks ﬁt nicely into our model, in fact they correspondexactly to a speciﬁc syntactic class of formulas. But we observed a problem when experimenting with such encodings using the method presented in the proofs above: SMT solvers
are generally not eﬃcient when dealing with neural network problems of this kind. Similar
issues have been previously reported (Pulina & Tacchella, 2012) and we are not aware ofa fully satisfying solution at this time. Still, the approach we present can be adapted tomake use of partial procedures, such as stochastic gradient descent, as part of the learnerprocess.
25

4.4 Learning Polynomial-Time Programs
In this section, we consider synthesizing programs for a given logical speciﬁcation. Itzhaky etal. (Itzhaky et al., 2010) considered a similar problem, however they focused on synthesizing
formulas in more specialized logics.
Problem In program synthesis, we are given a speciﬁcation and hope to ﬁnd an eﬃcient
program satisfying it. For us, a speciﬁcation is a way to verify whether the output q(A) is
accepted for A. There are two major variations – either the output for each structure isunique (as in our example here), or there is a set of acceptable outputs (e.g., when ﬁnding
some satisfying solution for SAT instances).
In our example here, we have a query s in an expressive logic (SO) and wish to ﬁnd
an equivalent query in a less-expressive logic. In particular, we consider the problem ofidentifying winning regions in ﬁnite games – i.e., directed graphs with a predicate V0 (x)meaning that vertex x belongs to Player 0. Decidability requires restricting the size of thegames to n, and we set C to be the set of pairs (A, B) such that A is a ﬁnite game of size
at most n and B is the extension of A with the winning region identiﬁed in a new monadic
predicate W .
Outline Here, we re-use the outlines introduced for learning games, but with an added
extension to least ﬁxed-point formulas for added expressive power. We focus on least ﬁxedpoint formulas, with a single LFP operator that is outermost11 . We ﬁx the arity a of theﬁxed-point predicate, and assume, as before, that the inner formula is a disjunction of lquantiﬁed CNF formulas with k variables and c clauses each. We use such an outline forexactly one selected relation W in the query, all others are set to identity.
Teacher Assume that we have a SO query s that produces the desired extension withthe winning region identiﬁed. Given a hypothesis q, the teacher can guess a game A ofsize at most n such that in q(A) the new relation W (x) is not equivalent to the region ins(A). Let a1 , . . . ,Wak be the winning
positions in s(A). The teacher then returns the pairA, ∀x (W (x) ↔ i (x = ai )) .

Example Consider the case of identifying winning regions in ﬁnite reachability games.
When the current vertex belongs to a player, that player chooses an outgoing edge andmoves to a connected vertex. Player 1 loses if the play reaches a vertex that belongs to her
and has no outgoing edge. Similarly, Player 0 loses if the play reaches a position where hemust but cannot move, but also if the play becomes a cycle and goes on forever. The goal
is to identify the vertices from which Player 0 has a winning strategy. That is, we want aformula ϕ(x) which holds exactly on the vertices for which Player 0 has a winning strategy.
Reachability games are positional, i.e., it suﬃces to consider strategies that depend only
on the current position and not on the history of the game. Therefore, a strategy of Player 1
can be deﬁned as a binary relation S1 that is a subset of the edges and that, for vertices ofPlayer 0, contains all successors of the vertex as well. Then, x is winning for Player 1 (by S1 )if all vertices reachable from x by S1 either belong to Player 0 or have an S1 -successor. This

11. This is a normal-form for fixed-point logics, although the arity of the fixed point may increase when weconvert to it (see Corollary 4.11 in (Immerman, 1999)).

26

is easily expressible using the TC operator and guessing the strategy leads to a second-orderformula ϕ0 (x) which holds exactly if x is winning for Player 0.
In reachability games, the following LFP formula deﬁnes the winning region for Player 0:hn
LFP W (x) = (¬∃x1 : (¬W (x1 ) ∧ E(x, x1 )) ∧ ¬V0 (x)) ∨oi∃x1 : (W (x1 ) ∧ E(x, x1 ) ∧ V0 (x)) (x) .

The LFP operator recursively deﬁnes W (x), starting with the empty set and adding
tuples that satisfy the formula on the right until a ﬁxed-point is reached. Therefore, thisformula says that a position x is winning for Player 0 if(a) it is the opponent’s move and all outgoing edges go to positions we win; or (b) it isPlayer 0’s move and there is an edge to a winning position.
Recall that the ﬁxed-point predicate is initially empty. Therefore, the winning positions
after one iteration are the positions belonging to the opponent with no outgoing edges.
Then, the winning region grows gradually until it is the attractor of those positions – whichis correct. An equivalent, slightly longer formula is found by our program in less than aminute for n ≥ 3.12
Further work The LFP formula for reachability games can be written by hand, but our
motivation for presenting this example is the hope to compute polynomial-time solvers forother games. In particular, weak parity games and parity games are also positional, so
it is trivial to write a SO formula deﬁning the winning region (as we did for reachability
games). But the polynomial-time program for solving weak parity games is complicated,
and the existence of a polynomial-time solver for full parity games (which is equivalent to
the existence of an LFP formula) is a long-standing open problem.
Our implementation can also search for other programs, e.g., for graph isomorphism,
graph coloring or SAT. There are classes where these problems are in polynomial-time13 .

5. Conclusions and Future Work
Above, we introduced our machine learning approach and its implementation using modern
SMT solvers. We prove that our approach comes with strong theoretical guarantees: aslong as a model exists in a given complexity class (e.g., NL, P, NP), it will be found.
Thanks to the eﬃciency of modern SAT and QBF solvers, our general procedure outperforms
specialized approaches both in learning reductions (Crouch et al., 2010) and in learning fromexamples (Kaiser, 2012). We consider these early results promising and encourage further
experimentation with our freely available implementation14 .
There are many questions we leave unanswered. For example, there is a large variance inruntime depending on the precise series of counter-examples given by the teacher. We would
like to know how to choose “good” counter-examples and whether randomness (Zeugmann,2006) can help. We ask what outlines are “good”, how to choose them to ﬁnd the desired
12. To replicate, after getting Toss, do make Learn/LfpTest.native and then run it.
13. E.g., isomorphism of planar graphs, bounded-degree graphs, and graphs excluding a minor; k-SAT and
k-coloring are NL-complete for k = 2 and NP-complete for k ≥ 3.
14. Available from http://toss.sf.net, see (Jordan & Kaiser, 2013b) for learning instructions.

27

programs quickly and to make them readable. We are interested in re-using sub-formulas
found for one problem to speed up learning in another one, a form of knowledge transfer.
Finally, eﬃciency of our approach in quantitative settings has been disappointing. It
seems that at present SMT solvers are not suited for tasks such as veriﬁcation or synthesisof neural networks. But SMT solvers are evolving and hopefully will improve in this regard.
One could also use stochastic gradient descent directly in our learner. How to utilize suchincomplete procedures eﬃciently remains an open question, but we hope that this work will
motivate further studies on the boundary between SMT solvers and machine learning.
Acknowledgements We appreciate the encouragement and support of Neil Immerman
and Thomas Zeugmann, without whom this paper would not exist.

References
Agrawal, M. (2011). The isomorphism conjecture for constant depth reductions. Journalof Computer and System Sciences, 77 (1), 3–13.
Agrawal, M., Allender, E., Impagliazzo, R., Pitassi, T., & Rudich, S. (2001). Reducing thecomplexity of reductions. Computational Complexity, 10 (2), 117–138.
Blum, L., Shub, M., & Smale, S. (1989). On a theory of computation and complexity over
the real numbers: N P -completeness, recursive functions and universal machines. Bull.
Amer. Math. Soc. (N.S.), 21 (1), 1–46.
Crouch, M., Immerman, N., & Moss, J. E. B. (2010). Finding reductions automatically. In
Fields of Logic and Computation – Essays Dedicated to Yuri Gurevich on the Occasionof His 70th Birthday, Vol. 6300 of Lecture Notes in Computer Science, pp. 181–200.
Fagin, R. (1974). Generalized ﬁrst-order spectra and polynomial-time recognizable sets. In
Complexity of Computation, SIAM-AMS Proceedings, Vol. 7, pp. 43–73.
Grädel, E., & Gurevich, Y. (1998). Metaﬁnite model theory. Information and Computation,
140 (1), 26–81.
Grädel, E., Kolaitis, P. G., Libkin, L., Marx, M., Spencer, J., Vardi, M. Y., Venema, Y., &Weinstein, S. (2007). Finite Model Theory and Its Applications. Springer.
Grädel, E., & Meer, K. (1996). Descriptive Complexity Theory over the Real Numbers.
Mathematics of Numerical Analysis: Real Number Algorithms, 32, 381–403.
Grohe, M. (2008). The quest for a logic capturing PTIME. In Proceedings, Twenty-Third
Annual IEEE Symposium on Logic in Computer Science, LICS 2008, pp. 267–271.
Gulwani, S. (2010). Dimensions in program synthesis. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative
Programming, PPDP ’10, pp. 13–24.
Heule, M. J. H., Kullmann, O., & Marek, V. W. (2016). Solving and verifying the boolean
Pythagorean triples problem via cube-and-conquer. In Theory and Applications ofSatisfiability Testing, 19th International Conference, SAT 2016, Bordeaux, France,
July 2016, Proceedings, Vol. 9710 of Lecture Notes in Computer Science, pp. 228–245.
Immerman, N. (1986). Relational queries computable in polynomial time. Inform. Control,
68, 86–104.
28

Immerman, N. (1987). Languages that capture complexity classes. SIAM J. Comput.,
16 (4), 760–778.
Immerman, N. (1999). Descriptive Complexity. Springer-Verlag.
Itzhaky, S., Gulwani, S., Immerman, N., & Sagiv, M. (2010). A simple inductive synthesis
methodology and its applications. In Proceedings of the 25th Annual ACM SIGPLAN
Conference on Object-Oriented Programming, Systems, Languages, and Applications,OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA, pp. 36–46.
Janota, M., Jordan, C., Klieber, W., Lonsing, F., Seidl, M., & Gelder, A. V. (2016). QBF
Gallery 2014: The QBF competition at the FLoC 2014 Olympic Games. Journal on
Satisfiability, Boolean Modeling and Computation, 9, 187–206.
Janota, M., Klieber, W., Marques-Silva, J., & Clarke, E. (2012). Solving QBF with counterexample guided reﬁnement. In Theory and Applications of Satisfiability Testing,
SAT 2012, 15th International Conference, Trento, Italy, June 2012, Proceedings, Vol.
7317 of Lecture Notes in Computer Science, pp. 114–128.
Jordan, C., & Kaiser, L. (2013a). Benchmarks from reduction ﬁnding. In Lonsing, F.,& Seidl, M. (Eds.), International Workshop on Quantified Boolean Formulas 2013,
Informal Workshop Report, pp. 40–43.
Jordan, C., & Kaiser, L. (2013b). Experiments with reduction ﬁnding. In Theory and Applications of Satisfiability Testing, 16th International Conference, SAT 2013, Helsinki,
Finland, July 2013, Proceedings, Vol. 7962 of Lecture Notes in Computer Science, pp.
192–207.
Kaiser, L. (2012). Learning games from videos guided by descriptive complexity. In Proceedings of the 26th Conference on Artificial Intelligence, AAAI-12, pp. 963–970.
Kaiser, L., Lang, M., Leßenich, S., & Löding, C. (2015). A uniﬁed approach to boundedness
properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic(CSL 2015), Vol. 41 of LIPIcs, pp. 441–456.
Kitzelmann, E. (2010). Inductive programming: A survey of program synthesis techniques.
In Approaches and Applications of Inductive Programming, Third International Workshop, AAIP 2009, Edinburgh, UK, September 2009, Revised Papers, Vol. 5812 of Lecture Notes in Computer Science, pp. 50–73.
Konev, B., & Lisitsa, A. (2015). Computer-aided proof of Erdős discrepancy properties.
Artificial Intelligence, 224, 103–118.
Lonsing, F., Seidl, M., & Van Gelder, A. (2016). The QBF Gallery: Behind the scenes.
Artificial Intelligence, 237, 92–114.
Pulina, L., & Tacchella, A. (2012). Challenging SMT solvers to verify neural networks. AI
Commun., 25 (2), 117–135.
Renegar, J. (1998). Recent progress on the complexity of the decision problem for thereals. In Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts andMonographs in Symbolic Computation, pp. 220–241. Springer Vienna.
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., & Saraswat, V. (2006). Combinatorialsketching for ﬁnite programs. In Proceedings of the 12th International Conference on
29Architectural Support for Programming Languages and Operating Systems, ASPLOS
XII, pp. 404–415.
Tarski, A. (1951). A Decision Method for Elementary Algebra and Geometry. University ofCalifornia Press. Originally published as RAND Report R-109, 1948. Also available inQuantifier Elimination and Cylindrical Algebraic Decomposition, pp. 24–84, Springer
1998.
Vardi, M. Y. (1982). The complexity of relational query languages. In Proceedings of the
14th Annual ACM Symposium on Theory of Computing, May 1982, San Francisco,California, USA, pp. 137–146.
Veith, H. (1998). Succinct representation, leaf languages, and projection reductions. Information and Computation, 142 (2), 207–236.
Zeugmann, T. (2006). From learning in the limit to stochastic ﬁnite learning. Theoret.
Comput. Sci., 364 (1), 77–97.

30