summaries: This paper presents the NeuroSAT architecture, which uses a deep, message passing neural net for predicting the satisfiability of CNF instances. The architecture is also able to predict a satisfiable assignment in the SAT case, and the literals involved in some minimal conflicting set of clauses (i.e. core) in the UNSAT case. The NeuroSAT architecture is based on a vector space embedding of literals and clauses, which exploits (with message passing) some important symmetries of SAT instances (permutation invariance and negation invariance). This architecture is tested on various classes of random SAT instances, involving both unstructured (RS) problems, and structured ones (e.g. graph colorings, vertex covers, dominating sets, etc.).

summaries: This paper trains a neural network to solve the satisfiability problems. Based on the message passing neural network, it presents NeuroSAT and trains it as a classifier to predict satisfiability under a single bit of supervision. After training, NeuroSAT can solve problems that are larger and more difficult than it ever saw during training. Furthermore, the authors present a way to decode the solutions from the network's activations. Besides, for unsatisfiable problems, the paper also presents NeuroUNSAT, which learns to detect the contradictions in the form of UNSAT cores.

abstractText: We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.

authors:
Irwan Bello
Hieu Pham
Quoc V Le
Mohammad Norouzi
Samy Bengio

title: Neural combinatorial optimization with reinforcement learning

venue: arXiv preprint arXiv:1611.09940,

authors:
Armin Biere
Marijn Heule
Hans van Maaren
Toby Walsh

title: Conflict-driven clause learning sat solvers

venue: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications,

authors:
Alfredo Braunstein
Marc Mézard
Riccardo Zecchina

title: Survey propagation: An algorithm for satisfiability

venue: Random Structures & Algorithms,

title: The complexity of theorem-proving procedures

venue: In Proceedings of the third annual ACM symposium on Theory of computing,

authors:
Hanjun Dai
Elias B Khalil
Yuyu Zhang
Bistra Dilkina
Le Song

title: Learning combinatorial optimization algorithms over graphs

venue: arXiv preprint arXiv:1704.01665,

authors:
Richard Evans
David Saxton
David Amos
Pushmeet Kohli
Edward Grefenstette

title: Can neural networks understand logical entailment

venue: arXiv preprint arXiv:1802.08535,

authors:
Alex Flint
Matthew Blaschko

title: Perceptron learning of sat

venue: In Advances in Neural Information Processing Systems,

authors:
Justin Gilmer
Samuel S Schoenholz
Patrick F Riley
Oriol Vinyals
George E Dahl

title: Neural message passing for quantum chemistry

venue: arXiv preprint arXiv:1704.01212,

authors:
Cristian Grozea
Marius Popescu

title: Can machine learning learn a decision oracle for np problems? a test on sat

venue: Fundamenta Informaticae,

authors:
Shai Haim
Toby Walsh

title: Restart strategy selection using machine learning techniques

authors:
S. Hochreiter
J. Schmidhuber

title: Long short-term memory

venue: Neural Computation,

authors:
Diederik Kingma
Jimmy Ba

title: Adam: A method for stochastic optimization

venue: arXiv preprint arXiv:1412.6980,

title: The art of computer programming, volume 4, fascicle 6: Satisfiability

title: Computers and intractability. a guide to the theory of np-completeness

authors:
Yujia Li
Daniel Tarlow
Marc Brockschmidt
Richard Zemel

title: Gated graph sequence neural networks

venue: arXiv preprint arXiv:1511.05493,

authors:
Jia Hui Liang
Vijay Ganesh
Pascal Poupart
Krzysztof Czarnecki

title: Learning rate based branching heuristic for sat solvers

venue: In International Conference on Theory and Applications of Satisfiability Testing,

title: Networks: an introduction

venue: Oxford university press,

authors:
Rasmus Berg Palm
Ulrich Paquet
Ole Winther

title: Recurrent relational networks for complex relational reasoning

venue: arXiv preprint arXiv:1711.08028,

authors:
Razvan Pascanu
Tomas Mikolov
Yoshua Bengio

title: Understanding the exploding gradient problem

authors:
Franco Scarselli
Marco Gori
Ah Chung Tsoi
Markus Hagenbuchner
Gabriele Monfardini

title: The graph neural network model

venue: IEEE Transactions on Neural Networks,

authors:
Rishabh Singh
Joseph P Near
Vijay Ganesh
Martin Rinard

title: Avatarsat: An auto-tuning boolean sat solver

authors:
Niklas Sorensson
Niklas Een. Minisat v

title: 13-a sat solver with conflict-clause minimization

title: On the complexity ofderivation in propositional calculus

venue: Studies in Constrained Mathematics and Mathematical Logic,

authors:
L. Xu
F. Hutter
H.H. Hoos
K. Leyton-Brown

title: SATzilla: portfolio-based algorithm selection for SAT

venue: Journal of Artificial Intelligence Research (JAIR),

heading: 1 INTRODUCTION

text:
The propositional satisfiability problem (SAT) is one of the most fundamental problems of computer science. Cook (1971) showed that the problem is NP-complete, which means that searching for any kind of efficiently-checkable certificate in any context can be reduced to finding a satisfying assignment of a propositional formula. In practice, search problems arising from a wide range of domains such as hardware and software verification, test pattern generation, planning, scheduling, and combinatorics are all routinely solved by constructing an appropriate SAT problem and then calling a SAT solver (Gomes et al., 2008). Modern SAT solvers based on backtracking search are extremely well-engineered and have been able to solve problems of practical interest with millions of variables (Biere et al., 2009).
We consider the question: can a neural network learn to solve SAT problems? To answer, we develop a novel message passing neural network (MPNN) (Scarselli et al., 2009; Li et al., 2015; Gilmer et al., 2017), NeuroSAT, and train it as a classifier to predict satisfiability on a dataset of random SAT problems. We provide NeuroSAT with only a single bit of supervision for each SAT problem that indicates whether or not the problem is satisfiable. When making a prediction about a new SAT problem, we find that NeuroSAT guesses unsatisfiable with low confidence until it finds a solution, at which point it converges and guesses satisfiable with very high confidence. The solution itself can almost always be automatically decoded from the network’s activations, making NeuroSAT an end-to-end SAT solver. See Figure 1 for an illustration of the train and test regimes.
Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve SAT problems that are substantially larger and more difficult than it ever saw during training by simply performing more iterations of message passing. Despite only running for a few dozen iterations during training, at test time NeuroSAT continues to find solutions to harder problems after hundreds and even thousands of iterations. The learning process has yielded not a traditional classifier but rather a procedure that can be run indefinitely to search for solutions to problems of varying difficulty.
Moreover, NeuroSAT generalizes to entirely new domains. Since NeuroSAT operates on SAT problems and since SAT is NP-complete, NeuroSAT can be queried on SAT problems encoding any kind of search problem for which certificates can be checked in polynomial time. Although we train it using only problems from a single random problem generator, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.
The same neural network architecture can also be used to help construct proofs for unsatisfiable problems. When we train it on a different dataset in which every unsatisfiable problem contains a small contradiction (call this trained model NeuroUNSAT), it learns to detect these contradictions instead of searching for satisfying assignments. Just as we can extract solutions from NeuroSAT’s activations, we can extract the variables involved in the contradiction from NeuroUNSAT’s activations. When the number of variables involved in the contradiction is small relative to the total number of variables, knowing which variables are involved in the contradiction can enable constructing a resolution proof more efficiently.

heading: 2 PROBLEM SETUP

text:
Background. A formula of propositional logic is a boolean expression built using the constants true (1) and false (0), variables, negations, conjunctions, and disjunctions. A formula is satisfiable provided there exists an assignment of boolean values to its variables such that the formula evaluates to 1. For example, the formula (x1 ∨ x2 ∨ x3) ∧ ¬(x1 ∧ x2 ∧ x3) is satisfiable because it will evaluate to 1 under every assignment that does not map x1, x2 and x3 to the same value. For every formula, there exists an equisatisfiable formula in conjunctive normal form (CNF), expressed as a conjunction of disjunctions of (possibly negated) variables.1 Each conjunct of a formula in CNF is called a clause, and each (possibly negated) variable within a clause is called a literal. The formula above is equivalent to the CNF formula (x1∨x2∨x3)∧(¬x1∨¬x2∨¬x3), which we can represent more concisely as {1|2|3, 1|2|3}. A formula in CNF has a satisfying assignment if and only if it has an assignment such that every clause has at least one literal mapped to 1. A SAT problem is a formula in CNF, where the goal is to determine if the formula is satisfiable, and if so, to produce a satisfying assignment of truth values to variables. We use n to denote the number of of variables in a SAT problem, and m to denote the number of clauses.
Classification task. For a SAT problem P , we define φ(P ) to be true if and only if P is satisfiable. Our first goal is to learn a classifier that approximates φ. Given a distribution Ψ over SAT problems, we can construct datasetsDtrain andDtest with examples of the form (P, φ(P )) by sampling problems P ∼ Ψ and computing φ(P ) using an existing SAT solver. At test time, we get only the problem P and the goal is to predict φ(P ), i.e. to determine if P is satisfiable. Ultimately we care about the solving task, which also includes finding solutions to satisfiable problems.
1This transformation can be done in linear time such that the size of the resulting formula has only grown linearly with respect to the original formula (Tseitin, 1968).

heading: 3 MODEL

text:
A SAT problem has a simple syntactic structure and therefore could be encoded into a vector space using standard methods such as an RNN. However, the semantics of propositional logic induce rich invariances that such a syntactic method would ignore, such as permutation invariance and negation invariance. Specifically, the satisfiability of a formula is not affected by permuting the variables (e.g. swapping x1 and x2 throughout the formula), by permuting the clauses (e.g. swapping the first clause with the second clause), or by permuting the literals within a clause (e.g. replacing the clause 1|2 with 2|1. The satisfiability of a formula is also not affected by negating every literal corresponding to a given variable (e.g. negating all occurrences of x1 in {1|2, 1|3} to yield {1|2, 1|3}). We now describe our neural network architecture, NeuroSAT, that enforces both permutation invariance and negation invariance. We encode a SAT problem as an undirected graph with one node for every literal, one node for every clause, an edge between every literal and every clause it appears in, and a different type of edge between each pair of complementary literals (e.g. between xi and xi). NeuroSAT iteratively refines a vector space embedding for each node by passing “messages” back and forth along the edges of the graph as described in Gilmer et al. (2017). At every time step, we have an embedding for every literal and every clause. An iteration consists of two stages. First, each clause receives messages from its neighboring literals and updates its embedding accordingly. Next, each literal receives messages from its neighboring clauses as well as from its complement, then updates its embedding accordingly. Figure 2 provides a high-level illustration of the architecture.
More formally, our model is parameterized by two vectors (Linit, Cinit), three multilayer perceptrons (Lmsg, Cmsg, Lvote) and two layer-norm LSTMs (Ba et al., 2016; Hochreiter & Schmidhuber, 1997) (Lu, Cu). At every time step t, we have a matrix L(t) ∈ R2n×d whose ith row contains the embedding for the literal `i and a matrix C(t) ∈ Rm×d whose jth row contains the embedding for the clause cj , which we initialize by tiling Linit and Cinit respectively. We also have hidden states L (t) h ∈ R2n×d and C (t) h ∈ Rm×d for Lu and Cu respectively, both initialized to zero matrices. Let M be the (bipartite) adjacency matrix defined by M(i, j) = 1 {`i ∈ cj} and let Flip be the operator that takes a matrix L and swaps each row of L with the row corresponding to the literal’s negation. A single iteration consists of applying the following two updates:
(C(t+1), C (t+1) h )← Cu([C (t) h ,M >Lmsg(L (t))])
(L(t+1), L (t+1) h )← Lu([L (t) h ,Flip(L (t)),MCmsg(C (t+1))])
After T iterations, we compute L(T )∗ ← Lvote(L(T )) ∈ R2n, which contains a single scalar for each literal (the literal’s vote), and then we compute the average of the literal votes y(T ) ← mean(L(T )∗ ) ∈ R. We train the network to minimize the sigmoid cross-entropy loss between the logit y(T ) and the true label φ(P ).
Our architecture enforces permutation invariance by operating on nodes and edges according to the topology of the graph without any additional ordering over nodes or edges. Likewise, it enforces negation invariance by treating all literals the same no matter whether they originated as a positive or negative occurrence of a variable.
We stress that none of the learned parameters depend on the size of the SAT problem and that a single model can be trained and tested on problems of arbitrary and varying sizes. At both train and test time, the input to the model is simply any bipartite adjacency matrix M over any number of literals and clauses. The learned parameters only determine how each individual literal and clause behaves in terms of its neighbors in the graph. Variation in problem size is handled by the aggregation operators: we sum the outgoing messages of each of a node’s neighbors to form the incoming message, and we take the mean of the literal votes at the end of message passing to form the logit y(T ).

heading: 4 TRAINING DATA

text: We want our neural network to be able to classify (and ultimately solve) SAT problems from a variety of domains that it never trained on. One can easily construct distributions over SAT problems for which it would be possible to predict satisfiability with perfect accuracy based only on crude statistics; however, a neural network trained on such a distribution would be unlikely to generalize to problems from other domains. To force our network to learn something substantive, we create a distribution SR(n) over pairs of random SAT problems on n variables with the following property: one element of the pair is satisfiable, the other is unsatisfiable, and the two differ by negating only a single literal occurrence in a single clause. To generate a random clause on n variables, SR(n) first samples a small integer k (with mean 5) 2 then samples k variables uniformly at random without replacement, and finally negates each one with independent probability 50%. It continues to generate clauses ci in this fashion, adding them to the SAT problem, and then querying a traditional SAT solver (we used Minisat Sorensson & Een (2005)), until adding the clause cm finally makes the problem unsatisfiable. Since {c1, . . . , cm−1} had a satisfying assignment, negating a single literal in cm must yield a satisfiable problem {c1, . . . , cm−1, c′m}. The pair ({c1, . . . , cm−1, cm}, {c1, . . . , cm−1, c′m}) are a sample from SR(n).

heading: 5 PREDICTING SATISFIABILITY

text:
Although our ultimate goal is to solve SAT problems arising from a variety of domains, we begin by training NeuroSAT as a classifier to predict satisfiability on SR(40). Problems in SR(40) are small enough to be solved efficiently by modern SAT solvers—a fact we rely on to generate the
2We use 2 + Bernoulli(0.3) + Geo(0.4) so that we generate clauses of varying size but with only a small number of clauses of length 2, since too many random clauses of length 2 make the problems too easy on average.
problems—but the classification problem is highly non-trivial from a machine learning perspective. Each problem has 40 variables and over 200 clauses on average, and the positive and negative examples differ by negating only a single literal occurrence out of a thousand. We were unable to train an LSTM on a many-hot encoding of clauses (specialized to problems with 40 variables) to predict with>50% accuracy on its training set. Even the canonical SAT solver MiniSAT (Sorensson & Een, 2005) needs to backjump3 almost ten times on average, and needs to perform over a hundred primitive logical inferences (i.e. unit propagations) to solve each problem.
We instantiated the NeuroSAT architecture described in §3 with d = 128 dimensions for the literal embeddings, the clause embeddings, and all the hidden units; 3 hidden layers and a linear output layer for each of the MLPs Lmsg, Cmsg, and Lvote; and rectified linear units for all non-linearities. We regularized by the `2 norm of the parameters scaled by 10−10, and performed T = 26 iterations of message passing on every problem. We trained our model using the ADAM optimizer (Kingma & Ba, 2014) with a learning rate of 2 × 10−5, clipping the gradients by global norm with clipping ratio 0.65 (Pascanu et al., 2012). We batched multiple problems together, with each batch containing up to 12,000 nodes (i.e. literals plus clauses). To accelerate the learning, we sampled the number of variables n uniformly from between 10 and 40 during training (i.e. we trained on SR(U(10, 40))), though we only evaluate on SR(40). We trained on millions of problems.
After training, NeuroSAT is able to classify the test set correctly with 85% accuracy. In the next section, we examine how NeuroSAT manages to do so and show how we can decode solutions to satisfiable problems from its activations. Note: for the entire rest of the paper, NeuroSAT refers to the specific trained model that has only been trained on SR(U(10, 40)).

heading: 6 DECODING SATISFYING ASSIGNMENTS

text:
Let us try to understand what NeuroSAT (trained on SR(U(10, 40))) is computing as it runs on new problems at test time. For a given run, we can compute and visualize the 2n-dimensional vector of literal votes L(t)∗ ← Lvote(L(t)) at every iteration t. Figure 3 illustrates the sequence of literal votes L (1) ∗ to L (24) ∗ as NeuroSAT runs on a satisfiable problem from SR(20). For clarity, we reshape each L (t) ∗ to be an Rn×2 matrix so that each literal is paired with its complement; specifically, the ith row contains the scalar votes for xi and xi. Here white represents zero, blue negative and red positive. For several iterations, almost every literal is voting unsat with low confidence (light blue). Then a few scattered literals start voting sat for the next few iterations, but not enough to affect the mean vote. Suddenly, there is a phase transition and all the literals (and hence the network as a whole) start to vote sat with very high confidence (dark red). After the phase transition, the vote for each literal converges and the network stops evolving.
NeuroSAT seems to exhibit qualitatively similar behavior on every satisfiable problem that it predicts correctly. The problems for which NeuroSAT guesses unsat are similar except without the phase change: it continues to guess unsat with low-confidence for as many iterations as NeuroSAT runs for. NeuroSAT never becomes highly confident that a problem is unsat, and it almost never guesses sat on an unsat problem. These results suggest that NeuroSAT searches for a certificate of satisfiability, and that it only guesses sat once it has found one.
Let us look more carefully at the literal votes L(24)∗ from Figure 3 after convergence. Note that most of the variables have one literal vote distinctly darker than the other. Moreover, the dark votes are all approximately equal to each other, and the light votes are all approximately equal to each other as well. Thus the votes seem to encode one bit for each variable. It turns out that these bits encode a satisfying assignment in this case, but they do not do so reliably in general. Recall from §3 that NeuroSAT projects the higher dimensional literal embeddings L(T ) ∈ R2n×d to the literal votes L(T )∗ using the MLP Lvote. Figure 4 illustrates the two-dimensional PCA embeddings for L(12) to L(26) (skipping every other time step) as NeuroSAT runs on a satisfiable problem from SR(40). Blue and red dots indicate literals that are set to 0 and 1 in the satisfying assignment that it eventually finds, respectively. The blue and red dots cannot be linearly separated until the phase transition at the end, at which point they form two distinct clusters according to the satisfying assignment. We
3i.e. backtrack multiple steps at a time
observe a similar clustering almost every time the network guesses sat. Thus the literal votes L(T )∗ only ever encode the satisfying assignment by chance, when the projection Lvote happens to preserve this clustering.
Our analysis suggests a more reliable way to decode solutions from NeuroSAT’s internal activations: 2-cluster L(T ) to get cluster centers ∆1 and ∆2, partition the variables according to the predicate ‖xi−∆1‖2+‖xi−∆2‖2 < ‖xi−∆2‖2+‖xi−∆1‖2, and then try both candidate assignments that result from mapping the partitions to truth values. This decoding procedure (using k-means to find the two cluster centers) successfully decodes a satisfying assignment for over 70% of the satisfiable problems in the SR(40) test set. Table 1 summarizes the results when training on SR(U(10, 40)) and testing on SR(40).
Recall that at training time, NeuroSAT is only given a single bit of supervision for each SAT problem. Moreover, the positive and negative examples in the dataset differ only by the placement of a single edge. NeuroSAT has learned to search for satisfying assignments solely to explain that single bit of supervision.

heading: 7 EXTRAPOLATING TO OTHER PROBLEM DISTRIBUTIONS

heading: 7.1 BIGGER PROBLEMS

text: Even though we only train NeuroSAT on SR(U(10, 40)), it is able to solve SAT problems sampled from SR(n) for n much larger than 40 by simply running for more iterations of message passing. Figure 5 shows NeuroSAT’s success rate on SR(n) for a range of n as a function of the number of iterations T . For n = 200, there are 2160 times more possible assignments to the variables than any problem it saw during training, and yet it can solve 25% of the satisfiable problems in SR(200) by running for four times more iterations than it performed during training. On the other hand, when restricted to the number of iterations it was trained with, it solves under 10% of them. Thus we see that its ability to solve bigger and harder problems depends on the fact that the dynamical system it has learned encodes generic procedural knowledge that can operate effectively over a wide range of time frames.

heading: 7.2 DIFFERENT PROBLEMS

text:
Every problem in NP can be reduced to SAT in polynomial time, and SAT problems arising from different domains may have radically different structural and statistical properties. Even though NeuroSAT has learned to search for satisfying assignments on problems from SR(n), we may still find that the dynamical system it has learned only works properly on problems similar to those it was trained on.
To assess NeuroSAT’s ability to extrapolate to different classes of problems, we generated problems in several other domains and then encoded them all into SAT problems (using standard encodings). In particular, we started by generating one hundred graphs from each of six different random graph distributions (Barabasi, Erdös-Renyi, Forest-Fire, Random-k-Regular, Random-Static-Power-Law, and Random-Geometric).4 We found parameters for the random graph generators such that each graph has ten nodes and seventeen edges on average. For each graph in each collection, we generated graph coloring problems (3 ≤ k ≤ 5), dominating-set problems (2 ≤ k ≤ 4)), clique-detection problems (3 ≤ k ≤ 5), and vertex cover problems (4 ≤ k ≤ 6).5 We chose the range of k for each problem to include the threshold for most of the graphs while avoiding trivial problems such as 2-clique. As before, we used Minisat Sorensson & Een (2005) to determine satisfiability. Figure 6 shows an example graph from the distribution. Note that the trained network does not know anything a priori about these tasks; the generated SAT problems need to encode not only the graphs themselves but also formal descriptions of the tasks to be solved.
Out of the 7,200 generated problems, we kept only the 4,888 satisfiable problems. On average these problems contained over two and a half times as many clauses as the problems in SR(40). We ran NeuroSAT for 512 iterations on each of them and found that we could successfully decode solutions for 85% of them. In contrast, Survey Propagation (SP) (Braunstein et al., 2005), the canonical (learning-free) message passing algorithm for satisfiability, does not on its own converge to a satisfying assignment on any of these problems.6 This suggests that NeuroSAT has not simply found a way to approximate SP, but rather has synthesized a qualitatively different algorithm.
4See Newman (2010) for an overview of random graph distributions. 5See (Lewis, 1983) for an overview of these problems as well as the standard encodings. 6We implementated the version with reinforcement messages described in Knuth (2015), along with the
numerical trick explained in Exercise 359.

heading: 8 FINDING UNSAT CORES

text:
NeuroSAT (trained on SR(U(10, 40))) can find satisfying assignments but is not helpful in constructing proofs of unsatisfiability. When it runs on an unsatisfiable problem, it keeps searching for a satisfying assignment indefinitely and non-systematically. However, when we train the same architecture on a dataset in which each unsatisfiable problem has a small subset of clauses that are already unsatisfiable (called an unsat core), it learns to detect these unsat cores instead of searching for satisfying assignments. The literals involved in the unsat core can be decoded from its internal activations. When the number of literals involved in the unsat core is small relative to the total number of literals, knowing the literals involved in the unsat core can enable constructing a resolution proof more efficiently.
We generated a new distribution SRC(n, u) that is similar to SR(n) except that every unsatisfiable problem contains a small unsat core. Here n is the number of variables as before, and u is an unsat core over x1, . . . , xk (k < n) that can be made into a satisfiable set of clauses u′ by negating a single literal. We sample a pair from SRC(n, u) as follows. First, we initialize a problem with u′, and then we sample clauses (over x1 to xn) just as we did for SR(n) until the problem becomes unsatisfiable. We can now negate a literal in the final clause to get a satisfiable problem ps, and then we can swap u′ for u in ps to get pu, which is unsatisfiable since it contains the unsat core u. We created train and test datasets from SRC(40, u) with u sampled at random for each problem from a collection of three unsat cores ranging from three clauses to nine clauses: the unsat core R from Knuth (2015), and the two unsat cores resulting from encoding the pigeonhole principles PP(2, 1) and PP(3, 2).7 We trained our architecture on this dataset, and we refer to the trained model as NeuroUNSAT.
NeuroUNSAT is able to predict satisfiability on the test set with 100% accuracy. Upon inspection, it seems to do so by learning to recognize the unsat cores. Figure 7 shows NeuroUNSAT running on a pair of problems from SRC(30,PP(3, 2)). In both cases, the literals in the first six rows are involved in the unsat core. In Figure 7a, NeuroUNSAT inspects the modified core u′ of the satisfiable problem but concludes that it does not match the pattern exactly. In Figure 7b, NeuroUNSAT finds the unsat core u and votes unsat with high confidence (dark blue). As in §6, the literals involved in the unsat core can sometimes be decoded from the literal votes L(T )∗ , but it is more reliable to 2- cluster the higher-dimensional literal embeddings L(T ). On the test set, the small number of literals involved in the unsat core end up in their own cluster 98% of the time.
Note that we do not expect NeuroUNSAT to generalize to arbitary unsat cores: as far as we know it is simply memorizing a collection of specific subgraphs, and there is no evidence it has learned a generic procedure to prove unsat.

heading: 9 RELATED WORK

text:
There have been many attempts over the years to apply statistical learning to various aspects of the SAT problem: restart strategies (Haim & Walsh, 2009), branching heuristics (Liang et al., 2016;
7The pigeonhole principle and the standard SAT encoding are described in Knuth (2015).
Grozea & Popescu, 2014; Flint & Blaschko, 2012), parameter tuning (Singh et al., 2009), and solver selection (Xu et al., 2008). None of these approaches use neural networks, and instead make use of both generic graph features and features extracted from the runs of SAT solvers. Moreover, these approaches are designed to assist existing solvers and do not aim to solve SAT problems on their own.
From the machine learning perspective, the closest work to ours is Palm et al. (2017), which showed that an MPNN can be trained to predict the unique solutions of Sudoku puzzles. We believe that their network’s success is an instance of the phenomenon we study in this paper, namely that MPNNs can synthesize local search algorithms for constraint satisfaction problems. Evans et al. (2018) present a neural network architecture that can learn to predict whether one propositional formula entails another by randomly sampling and evaluating candidate assignments. Unlike NeuroSAT, their network does not perform heuristic search and can only work on simple problems for which random guessing is tractable. There have also been several recent papers showing that various neural network architectures can learn good heuristics for NP-hard combinatorial optimization problems (Vinyals et al., 2015; Bello et al., 2016; Dai et al., 2017); however, finding low-cost solutions to optimization problems requires less precise reasoning than finding satisfying assignments.

heading: 10 DISCUSSION

text:
Our main motivation has been scientific: to better understand the extent to which neural networks are capable of precise, logical reasoning. Our work has definitively established that neural networks can learn to perform discrete search on their own without the help of hard-coded search procedures, even after only end-to-end training with minimal supervision. We found this result surprising and think it constitutes an important contribution to the community’s evolving understanding of the capabilities and limitations of neural networks.
Although not our primary concern, we also hope that our findings eventually lead to improvements in practical SAT solving. As we stressed early on, as an end-to-end SAT solver the trained NeuroSAT system discussed in this paper is still vastly less reliable than the state-of-the-art. We concede that we see no obvious path to beating existing SAT solvers. One approach might be to continue to train NeuroSAT as an end-to-end solver on increasingly difficult problems. A second approach might be to use a system like NeuroSAT to help guide decisions within a more traditional SAT solver, though it is not clear that NeuroSAT provides any useful information before it finds a satisfying assignment. However, as we discussed in §8, when we trained our architecture on different data it learned an entirely different procedure. In a separate experiment omitted for space reasons, we also trained our architecture to predict whether there is a satisfying assignment involving each individual literal in the problem and found that it was able to predict these bits with high accuracy as well. Unlike NeuroSAT, it made both type I and type II errors, had no discernable phase transition, and could make reasonable predictions within only a few rounds. We believe that architectures descended from NeuroSAT will be able to learn very different mechanisms and heuristics depending on the data they are trained on and the details of their objective functions. We are cautiously optimistic that a descendant of NeuroSAT will one day lead to improvements to the state-of-the-art.

heading: ACKNOWLEDGEMENTS

text: We thank Steve Mussmann, Alexander Ratner, Nathaniel Thomas, Vatsal Sharan and Cristina White for providing valuable feedback on early drafts. We also thank William Hamilton, Geoffrey Irving and Arun Chaganty for helpful discussions. This work was supported by Future of Life Institute grant 2017-158712.


summaries: The paper describes a framework for training a self-driving policy by augmenting imitation loss with additional loss terms that penalize undesired behaviors and that encourage progress. The policy takes as input a parsed representation of the scene (rather than raw images) and outputs pose trajectories for a down-stream controller. The method is trained on simulated data that includes perturbations to improve generalizability. The framework is evaluated in simulation through a series of ablations to better understand the contribution of the different loss terms.

summaries: The paper proposes a vehicle’s trajectory planner that iteratively predict next-step (longitudinal and latitudinal) position of an ego-vehicle. Instead of using a raw image, a set of handcrafted features (i.e., the status of traffic lights, route, roadmap, etc) are mapped onto a fixed-size of bird-eye view map, which is then fed into the recurrent neural network. Additional regularizing loss terms are explored for the robustness of the model. The effectiveness of the method is demonstrated in simulation and real-world experiment.

abstractText: Our goal is to train a policy for autonomous driving via imitation learning that is robust enough to drive a real vehicle. We find that standard behavior cloning is insufficient for handling complex driving scenarios, even when we leverage a perception system for preprocessing the input and a controller for executing the output on the car: 30 million examples are still not enough. We propose exposing the learner to synthesized data in the form of perturbations to the expert’s driving, which creates interesting situations such as collisions and/or going off the road. Rather than purely imitating all data, we augment the imitation loss with additional losses that penalize undesirable events and encourage progress – the perturbations then provide an important signal for these losses and lead to robustness of the learned model. We show that the model can handle complex situations in simulation, and present ablation experiments that emphasize the importance of each of our proposed changes and show that the model is responding to the appropriate causal factors. Finally, we demonstrate the model driving a car in the real world.

authors:
Mariusz Bojarski
Davide Del Testa
Daniel Dworakowski
Bernhard Firner
Beat Flepp
Prasoon Goyal
Lawrence D Jackel
Mathew Monfort
Urs Muller
Jiakai Zhang

title: End to end learning for self-driving cars

venue: arXiv preprint arXiv:1604.07316,

authors:
Mariusz Bojarski
Philip Yeres
Anna Choromanska
Krzysztof Choromanski
Bernhard Firner
Lawrence Jackel
Urs Muller

title: Explaining how a deep neural network trained with end-toend learning steers a car

venue: arXiv preprint arXiv:1704.07911,

authors:
Chenyi Chen
Ari Seff
Alain Kornhauser
Jianxiong Xiao

title: Deepdriving: Learning affordance for direct perception in autonomous driving

venue: In Proceedings of the IEEE International Conference on Computer Vision, pp

authors:
Felipe Codevilla
Matthias Müller
Alexey Dosovitskiy
Antonio López
Vladlen Koltun

title: Endto-end driving via conditional imitation learning

venue: arXiv preprint arXiv:1710.02410,

authors:
Nemanja Djuric
Vladan Radosavljevic
Henggang Cui
Thi Nguyen
Fang-Chieh Chou
Tsung-Han Lin
Jeff Schneider

title: Motion prediction of traffic actors for autonomous driving using deep convolutional networks

venue: arXiv preprint arXiv:1808.05819,

authors:
Alexey Dosovitskiy
German Ros
Felipe Codevilla
Antonio Lopez
Vladlen Koltun

title: Carla: An open urban driving simulator

venue: arXiv preprint arXiv:1711.03938,

authors:
Nathaniel Fairfield
Chris Urmson

title: Traffic light mapping and detection

venue: In Robotics and Automation (ICRA),

authors:
Simon Hecker
Dengxin Dai
Luc Van Gool

title: Learning driving models with a surround-view camera system and a route planner

venue: arXiv preprint arXiv:1803.10158,

authors:
Alex Kuefler
Jeremy Morton
Tim Wheeler
Mykel Kochenderfer

title: Imitating driver behavior with generative adversarial networks

venue: In Intelligent Vehicles Symposium (IV),

authors:
Michael Laskey
Caleb Chuck
Jonathan Lee
Jeffrey Mahler
Sanjay Krishnan
Kevin Jamieson
Anca Dragan
Ken Goldberg

title: Comparing human-centric and robot-centric sampling for robot deep learning from demonstrations

authors:
Michael Laskey
Jonathan Lee
Roy Fox
Anca Dragan
Ken Goldberg

title: Dart: Noise injection for robust imitation learning

venue: arXiv preprint arXiv:1703.09327,

authors:
Donghan Lee
Youngwook Paul Kwon
Sara McMains
J Karl Hedrick

title: Convolution neural network-based lane change intention prediction of surrounding vehicles for acc

venue: In Intelligent Transportation Systems (ITSC),

authors:
Jesse Levinson
Jake Askeland
Jan Becker
Jennifer Dolson
David Held
Soeren Kammel
J Zico Kolter
Dirk Langer
Oliver Pink
Vaughan Pratt

title: Towards fully autonomous driving: Systems and algorithms

authors:
Wenjie Luo
Bin Yang
Raquel Urtasun

title: Fast and furious: Real time end-to-end 3d detection, tracking and motion forecasting with a single convolutional net

authors:
Matthias Müller
Alexey Dosovitskiy
Bernard Ghanem
Vladen Koltun

title: Driving policy transfer via modularity and abstraction

venue: arXiv preprint arXiv:1804.09364,

authors:
Brian Paden
Michal Čáp
Sze Zheng Yong
Dmitry Yershov
Emilio Frazzoli

title: A survey of motion planning and control techniques for self-driving urban vehicles

venue: IEEE Transactions on intelligent vehicles,

authors:
Xinlei Pan
Yurong You
Ziyan Wang
Cewu Lu

title: Virtual to real reinforcement learning for autonomous driving

venue: arXiv preprint arXiv:1704.03952,

authors:
Kexin Pei
Yinzhi Cao
Junfeng Yang
Suman Jana

title: Deepxplore: Automated whitebox testing of deep learning systems

venue: In Proceedings of the 26th Symposium on Operating Systems Principles,

title: Alvinn: An autonomous land vehicle in a neural network

venue: In Advances in neural information processing systems,

authors:
Stéphane Ross
Geoffrey Gordon
Drew Bagnell

title: A reduction of imitation learning and structured prediction to no-regret online learning

venue: In Proceedings of the fourteenth international conference on artificial intelligence and statistics,

authors:
Axel Sauer
Nikolay Savinov
Andreas Geiger

title: Conditional affordance learning for driving in urban environments

venue: arXiv preprint arXiv:1806.06498,

authors:
Shai Shalev-Shwartz
Shaked Shammah
Amnon Shashua

title: Safe, multi-agent, reinforcement learning for autonomous driving

venue: arXiv preprint arXiv:1610.03295,

authors:
Yuchi Tian
Kexin Pei
Suman Jana
Baishakhi Ray

title: Deeptest: Automated testing of deepneural-network-driven autonomous cars

venue: In Proceedings of the 40th International Conference on Software Engineering,

authors:
Huazhe Xu
Yang Gao
Fisher Yu
Trevor Darrell

title: End-to-end learning of driving models from large-scale video datasets

venue: In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition,

heading: 1 INTRODUCTION

text:
In order to drive a car, a driver needs to see and understand the various objects in the environment, predict their possible future behaviors and interactions, and then plan how to control the car in order to safely move closer to their desired destination while obeying the rules of the road. This is a difficult robotics challenge that humans solve well, making imitation learning a promising approach. Our work is about getting imitation learning to the level where it has a shot at driving a real vehicle; although the same insights may apply to other domains, these domains might have different constraints and opportunities, so we do not want to claim contributions there.
We built our system based on leveraging the training data (30 million real-world expert driving examples, corresponding to about 60 days of continual driving) as effectively as possible. There is a lot of excitement for end-to-end learning approaches to driving which typically focus on learning to directly predict raw control outputs such as steering or braking after consuming raw sensor input such as camera or lidar data. But to reduce sample complexity, we opt for mid-level input and output representations that take advantage of perception and control components. We use a perception system that processes raw sensor information and produces our input: a top-down representation of the environment and intended route, where objects such as vehicles are drawn as oriented 2D boxes along with a rendering of the road information and traffic light states. We present this mid-level input to a recurrent neural network (RNN), which then outputs a driving trajectory that is consumed by a controller which translates it to steering and acceleration. The further advantage of these midlevel representations is that the net can be trained on real or simulated data, and can be easily tested and validated in closed-loop simulations before running on a real car.
Our first finding is that even with 30 million examples, and even with mid-level input and output representations that remove the burden of perception and control, pure imitation learning is not sufficient. As an example, we found that this model would get stuck or collide with another vehicle parked on the side of a narrow street, when a nudging and passing behavior was viable. The key challenge is that we need to run the system closed-loop, where errors accumulate and induce a shift from the training distribution (Ross et al. (2011)). Scientifically, this result is valuable evidence about the limitations of pure imitation in the driving domain, especially in light of recent promising
results for high-capacity models (Laskey et al. (2017a)). But practically, we needed ways to address this challenge without exposing demonstrators to new states actively (Ross et al. (2011); Laskey et al. (2017b)) or performing reinforcement learning (Kuefler et al. (2017)).
We find that this challenge is surmountable if we augment the imitation loss with losses that discourage bad behavior and encourage progress, and, importantly, augment our data with synthesized perturbations in the driving trajectory. These expose the model to non-expert behavior such as collisions and off-road driving, and inform the added losses, teaching the model to avoid these behaviors. Note that the opportunity to synthesize this data comes from the mid-level input-output representations, as perturbations would be difficult to generate with either raw sensor input or direct controller outputs.
We evaluate our system, as well as the relative importance of both loss augmentation and data augmentation, first in simulation. We then show how our final model successfully drives a car in the real world and is able to negotiate situations involving other agents, turns, stop signs, and traffic lights. Finally, it is important to note that there are highly interactive situations such as merging which may require a significant degree of exploration within a reinforcement learning (RL) framework. This will demand simulating other (human) traffic participants, a rich area of ongoing research. Our contribution can be viewed as pushing the boundaries of what you can do with purely offline data and no RL.

heading: 2 RELATED WORK

text: Decades-old work on ALVINN (Pomerleau (1989)) showed how a shallow neural network could follow the road by directly consuming camera and laser range data. Learning to drive in an end-toend manner has seen a resurgence in recent years. Recent work by Chen et al. (2015) demonstrated a convolutional net to estimate affordances such as distance to the preceding car that could be used to program a controller to control the car on the highway. Researchers at NVIDIA (Bojarski et al. (2016; 2017)) showed how to train an end-to-end deep convolutional neural network that steers a car by consuming camera input. Xu et al. (2017) trained a neural network for predicting discrete or continuous actions also based on camera inputs. Codevilla et al. (2017) also train a network using camera inputs and conditioned on high-level commands to output steering and acceleration. Kuefler et al. (2017) use Generative Adversarial Imitation Learning (GAIL) with simple affordancestyle features as inputs to overcome cascading errors typically present in behavior cloned policies so that they are more robust to perturbations. Recent work from Hecker et al. (2018) learns a driving model using 360-degree camera inputs and desired route planner to predict steering and speed. The CARLA simulator (Dosovitskiy et al. (2017)) has enabled recent work such as Sauer et al. (2018), which estimates several affordances from sensor inputs to drive a car in a simulated urban environment. Using mid-level representations in a spirit similar to our own, Müller et al. (2018) train a system in simulation using CARLA by training a driving policy from a scene segmentation network to output high-level control, thereby enabling transfer learning to the real world using a different segmentation network trained on real data. Pan et al. (2017) also describes achieving transfer of an agent trained in simulation to the real world using a learned intermediate scene labeling representation. Reinforcement learning may also be used in a simulator to train drivers on difficult interactive tasks such as merging which require a lot of exploration, as shown in Shalev-Shwartz et al. (2016). A convolutional network operating on a space-time volume of bird’s eye-view representations is also employed by Luo et al. (2018); Djuric et al. (2018); Lee et al. (2017) for tasks like 3D detection, tracking and motion forecasting. Finally, there exists a large volume of work on vehicle motion planning outside the machine learning context and Paden et al. (2016) present a notable survey.

heading: 3 MODEL ARCHITECTURE

heading: 3.1 INPUT OUTPUT REPRESENTATION

text:
We begin by describing our top-down input representation that the network will process to output a drivable trajectory. At any time t, our agent (or vehicle) may be represented in a top-down coordinate system by pt, θt, st, where pt = (xt, yt) denotes the agent’s location or pose, θt denotes the heading or orientation, and st denotes the speed. The top-down coordinate system is picked such that our
agent’s pose p0 at the current time t = 0 is always at a fixed location (u0, v0) within the image. The orientation of the coordinate system is randomly picked for each training example to be within an angular range of θ0 ±∆, where θ0 denotes the heading or orientation of our agent at time t = 0. As shown in Fig. 1, the input to our model consists of several images of size W ×H pixels rendered into this top-down coordinate system. (a) Roadmap: a color (3-channel) image with a rendering of various map features such as lanes, stop signs, cross-walks, curbs, etc. (b) Traffic lights: a temporal sequence of grayscale images where each frame of the sequence represents the known state of the traffic lights at each past timestep. Within each frame, we color each lane center by a gray level with the brightest level for red lights, intermediate gray level for yellow lights, and a darker level for green or unknown lights1. (c) Speed limit: a single channel image with lane centers colored in proportion to their known speed limit. (d) Route: the intended route along which we wish to drive, generated by a router (think of a Google Maps-style route). (e) Current agent box: this shows our agent’s full bounding box at the current timestep t = 0. (f) Dynamic objects in the environment: a temporal sequence of images showing all the potential dynamic objects (vehicles, cyclists, pedestrians) rendered as oriented boxes. (g) Past agent poses: the past poses of our agent are rendered into a single grayscale image as a trail of points.
We use a fixed-time sampling of δt to sample any past or future temporal information, such as the traffic light state or dynamic object states in the above inputs. The traffic lights and dynamic objects are sampled over the past Tscene seconds, while the past agent poses are sampled over a potentially longer interval of Tpose seconds. This simple input representation, particularly the box representation of other dynamic objects, makes it easy to generate input data from simulation or create it from real-sensor logs using a standard perception system that detects and tracks objects. This enables testing and validation of models in closed-loop simulations before running them on a real car. This also allows the same model to be improved using simulated data to adequately explore rare situations such as collisions for which real-world data might be difficult to obtain. Using a topdown 2D view also means efficient convolutional inputs, and allows flexibility to represent metadata and spatial relationships in a human-readable format. Papers on testing frameworks such as Tian et al. (2018), Pei et al. (2017) show the brittleness of using raw sensor data (such as camera images or lidar point clouds) for learning to drive, and reinforce the approach of using an intermediate input representation.
1We employ an indexed representation for roadmap and traffic lights channels to reduce the number of input channels, and to allow extensibility of the input representation to express more roadmap features or more traffic light states without changing the model architecture.
If I denotes the set of all the inputs enumerated above, then the RNN recurrently predicts future poses of our agent conditioned on these input images I as shown by the green dots in Fig. 1(h).
pt+δt = RNN(I,pt) (1)
In Eq. (1), current pose p0 is a known part of the input, and then the RNN performs N iterations and outputs a future trajectory{pδt,p2δt, ...,pNδt} along with other properties such as future speeds. This trajectory can be fed to a controls optimizer that computes detailed driving control (such as steering and braking commands) within the specific constraints imposed by the dynamics of the vehicle to be driven. Different types of vehicles may possibly utilize different control outputs to achieve the same driving trajectory, which argues against training a network to directly output lowlevel steering and acceleration control. Note, however, that having intermediate representations like ours does not preclude end-to-end optimization from sensors to controls.

heading: 3.2 MODEL DESIGN

text:
Broadly, the driving model is composed of several parts as shown in Fig. 2. The main model shown in part (a) of the figure consists of a convolutional feature network (FeatureNet) that consumes the input data to create a digested contextual feature representation that is shared by the other networks. These features are consumed by a recurrent agent network (AgentRNN) that iteratively predicts successive points in the driving trajectory. Each point at time t in the trajectory is characterized by its location pt = (xt, yt), heading θt and speed st. The AgentRNN also predicts the bounding box of the vehicle as a spatial heatmap at each future timestep. In part (b) of the figure, we see that two other networks are co-trained using the same feature representation as an input. The Road Mask Network predicts the drivable areas of the field of view (on-road vs. off-road), while the recurrent perception network (PerceptionRNN) iteratively predicts a spatial heatmap for each timestep showing the future location of every other agent in the scene. We believe that doing well on these additional tasks using the same shared features as the main task improves generalization on the main task. Fig. 2(c) shows the various losses used in training the model, which we will discuss in detail below.
Fig. 3 illustrates the models in more detail. The rendered inputs shown in Fig. 1 are fed to a largereceptive field convolutional FeatureNet with skip connections, which outputs features F that capture the environmental context and the intent. These features are fed to the AgentRNN which predicts the next point pk on the driving trajectory, and the agent bounding box heatmap Bk, conditioned on the features F from the FeatureNet, the iteration number k ∈ {1, . . . , N}, the memory Mk−1
of past predictions from the AgentRNN, and the agent bounding box heatmap Bk−1 predicted in the previous iteration.
pk, Bk = AgentRNN(k, F,Mk−1, Bk−1) (2)
The memory Mk is an additive memory consisting of a single channel image. At iteration k of the AgentRNN, the memory is incremented by 1 at the location pk predicted by the AgentRNN, and this memory is then fed to the next iteration. The AgentRNN outputs a heatmap image over the next pose of the agent, and we use the arg-max operation to obtain the coarse pose prediction pk from this heatmap. The AgentRNN then employs a shallow convolutional meta-prediction network with a fully-connected layer that predicts a sub-pixel refinement of the pose δpk and also estimates the heading θk and the speed sk. Note that the AgentRNN is unrolled at training time for a fixed number of iterations, and the losses described below are summed together over the unrolled iterations. In the next section, we show how to train the model above to imitate the expert.

heading: 4 IMITATING THE EXPERT

heading: 4.1 IMITATION LOSSES

heading: 4.1.1 AGENT POSITION, HEADING AND BOX PREDICTION

text:
The AgentRNN produces three outputs at each iteration k: a probability distribution Pk(x, y) over the spatial coordinates of the predicted waypoint obtained after a spatial softmax, a heatmap of the predicted agent box at that timestep Bk(x, y) obtained after a per-pixel sigmoid activation that represents the probability that the agent occupies a particular pixel, and a regressed box heading output θk. Given ground-truth data for the above predicted quantities, we can define the corresponding losses for each iteration as:
Lp = H(Pk, P gtk ) (3)
LB = 1
WH ∑ x ∑ y H(Bk(x, y), Bgtk (x, y)) (4)
Lθ = ∥∥θk − θgtk ∥∥1 (5)
where the superscript gt denotes the corresponding ground-truth values, and H(a, b) is the crossentropy function. Note that P gtk is a binary image with only the pixel at the ground-truth target coordinate bpgtk c set to one.

heading: 4.1.2 AGENT META PREDICTION

text:
The meta prediction network performs regression on the features to generate a sub-pixel refinement δpk of the coarse waypoint prediction as well as a speed estimate sk at each iteration. We employ L1 loss for both of these outputs:
Lp−subpixel = ∥∥δpk − δpgtk ∥∥1 (6)
Lspeed = ∥∥sk − sgtk ∥∥1 (7)
where δpgtk = p gt k − bp gt k c is the fractional part of the ground-truth pose coordinates.

heading: 4.2 PAST MOTION DROPOUT

text: During training, the model is provided the past motion history as one of the inputs (Fig. 1(g)). Since the past motion history during training is from an expert demonstration, the net can learn to “cheat” by just extrapolating from the past rather than finding the underlying causes of the behavior. During closed-loop inference, this breaks down because the past history is from the net’s own past predictions. For example, such a trained net may learn to only stop for a stop sign if it sees a deceleration in the past history, and will therefore never stop for a stop sign during closed-loop inference. To address this, we introduce a dropout on the past pose history, where for 50% of the examples, we keep only the current position (u0, v0) of the agent in the past agent poses channel of the input data. This forces the net to look at other cues in the environment to explain the future motion profile in the training example.

heading: 5 BEYOND PURE IMITATION

text: In this section, we go beyond vanilla cloning of the expert’s demonstrations in order to teach the model to arrest drift and avoid bad behavior such as collisions and off-road driving by synthesizing variations of the expert’s behavior.

heading: 5.1 SYNTHESIZING PERTURBATIONS

text: Running the model as a part of a closed-loop system over time can cause the input data to deviate from the training distribution. To prevent this, we train the model by adding some examples with realistic perturbations to the agent trajectories. The start and end of a trajectory are kept constant, while a perturbation is applied around the midpoint and smoothed across the other points. Quantitatively, we jitter the midpoint pose of the agent uniformly at random in the range [−0.5, 0.5] meters in both axes, and perturb the heading by [−π/3, π/3] radians. We then fit a smooth trajectory to the perturbed point and the original start and end points. Such training examples bring the car back to its original trajectory after a perturbation (see appendix for an example). We filter out some perturbed trajectories that are impractical by thresholding on maximum curvature. But we do allow the perturbed trajectories to collide with other agents or drive off-road, because the network can then experience and avoid such behaviors even though real examples of these cases are not present in the training data. In training, we give perturbed examples a weight of 1/10 relative to the real examples, to avoid learning a propensity for perturbed driving.

heading: 5.2 BEYOND THE IMITATION LOSS

heading: 5.2.1 COLLISION LOSS

text:
Since our training data does not have any real collisions, the idea of avoiding collisions is implicit and will not generalize well. To alleviate this issue, we add a specialized loss that directly measures the overlap of the predicted agent box Bk with the ground-truth boxes of all the scene objects at each timestep.
Lcollision = 1
WH ∑ x ∑ y Bk(x, y) . Obj gt k (x, y) (8)
whereBk is the likelihood map for the output agent box prediction, andObj gt k is a binary mask with ones at all pixels occupied by other dynamic objects (other vehicles, pedestrians, etc.) in the scene at timestep k. At any time during training, if the model makes a poor prediction that leads to a collision, the overlap loss would influence the gradients to correct the mistake. However, this loss would be effective only during the initial training rounds when the model hasn’t learned to predict close to the ground-truth locations due to the absence of real collisions in the ground truth data. This issue is alleviated by the addition of trajectory perturbation data, where artificial collisions within those examples allow this loss to be effective throughout training without the need for online exploration like in reinforcement learning settings.

heading: 5.2.2 ON ROAD LOSS

text:
Trajectory perturbations also create synthetic cases where the car veers off the road or climbs a curb or median because of the perturbation. To train the network to avoid hitting such hard road edges, we add a specialized loss that measures overlap of the predicted agent box Bk in each timestep with a binary mask Roadgt denoting the road and non-road regions within the field-of-view.
Lonroad = 1
WH ∑ x ∑ y Bk(x, y) . (1−Roadgt(x, y)) (9)

heading: 5.2.3 GEOMETRY LOSS

text:
We would like to explicitly constrain the agent to follow the target geometry independent of the speed profile. We model this target geometry by fitting a smooth curve to the target waypoints and rendering this curve as a binary image in the top-down coordinate system. The thickness of this curve is set to be equal to the width of the agent. We express this loss similar to the collision loss by measuring the overlap of the predicted agent box with the binary target geometry image Geomgt. Any portion of the box that does not overlap with the target geometry curve is added as a penalty to the loss function.
Lgeom = 1
WH ∑ x ∑ y Bk(x, y) . (1−Geomgt(x, y)) (10)

heading: 5.2.4 AUXILIARY LOSSES

text:
Similar to our own agent’s trajectory, the motion of other agents may also be predicted by a recurrent network. Correspondingly, we add a recurrent perception network PerceptionRNN that uses as input the shared features F created by the FeatureNet and its own predictions Objk−1 from the previous iteration, and predicts a heatmap Objk at each iteration. Objk(x, y) denotes the probability that location (x, y) is occupied by a dynamic object at time k. For iteration k = 0, the PerceptionRNN is fed the ground truth objects at the current time.
Lobjects = 1
WH ∑ x ∑ y H(Objk(x, y), Objgtk (x, y)) (11)
Co-training a PerceptionRNN to predict the future of other agents by sharing the same feature representation F used by the PerceptionRNN is likely to induce the feature network to learn better features that are suited to both tasks.
We also co-train to predict a binary road/non-road mask by adding a small network of convolutional layers to the output of the feature net F . We add a cross-entropy loss to the predicted road mask output Road(x, y) which compares it to the ground-truth road mask Roadgt.
Lroad = 1
WH ∑ x ∑ y H(Road(x, y), Roadgt(x, y)) (12)

heading: 5.3 IMITATION DROPOUT

text:
Overall, our losses may be grouped into two sub-groups: the imitation losses Limit = {Lp,LB ,Lθ,Lp−subpixel,Lspeed} and the environment losses Lenv =
{Lcollision,Lonroad,Lgeom,Lobjects,Lroad}. The imitation losses cause the model to imitate the expert’s demonstrations, while the environment losses discourage undesirable behavior such as collisions. To further increase the effectiveness of the environment losses, we experimented with randomly dropping out the imitation losses for a random subset of training examples. We refer to this as “imitation dropout”. In the experiments, we show that imitation dropout yields a better driving model than simply under-weighting the imitation losses. During imitation dropout, the weight on the imitation losses wimit is randomly chosen to be either 0 or 1 with a certain probability for each training example. The overall loss is given by:
L = wimit ∑
`∈Limit
`+ wenv ∑
`∈Lenv
` (13)

heading: 6 EXPERIMENTS

heading: 6.1 MODELS

text: We train and test not only our final model, but a sequence of models that introduce the ingredients we describe one by one on top of behavior cloning. We start withM0, which does behavior cloning with past motion dropout to prevent using the history to cheat. M1 adds perturbations without modifying the losses. M2 further adds our environment losses Lenv in Section 5.2. M3 andM4 address the fact that we do not want to imitate bad behavior – M3 is a baseline approach, where we simply decrease the weight on the imitation loss, whileM4 uses our imitation dropout approach with a dropout probability of 0.5. Table 2 lists the configuration for each of these models.

heading: 6.2 DATA

text: The training data to train our model was obtained by randomly sampling segments of real-world expert driving and removing segments where the car was stationary for long periods of time. Since our input field of view is 80m × 80m, we also removed any segments of highway driving for the experiments presented here, because highway driving would need a larger field of view. Our dataset contains approximately 26 million examples which amount to about 60 days of continuous driving. As discussed in Section 3, the vertical-axis of the top-down coordinate system for each training example is randomly oriented within a range of ∆ = ±25◦ of our agent’s current heading, in order to avoid a bias for driving along the vertical axis. The rendering orientation is set to the agent heading (∆ = 0) during inference. Data about the prior map of the environment (roadmap) and the speed-limits along the lanes is collected apriori. For the dynamic scene entities like objects and traffic-lights, we employ a separate perception system based on laser and camera data similar to existing works in the literature (Fairfield & Urmson (2011); Levinson et al. (2011)). Table 1 lists the parameter values used for all the experiments in this paper.

heading: 6.3 EVALUATION

text: To evaluate our learned model on a specific scenario, we replay the segment through the simulation until a buffer period of max(Tpose, Tscene) has passed. This allows us to generate the first rendered snapshot of the model input using all the replayed messages until now. The model is evaluated on this input, and the fitted controls are passed to the vehicle simulator that emulates the dynamics of the vehicle thus moving the simulated agent to its next pose. At this point, the simulated pose might be different from the logged pose, but our input representation allows us to correctly render the new input for the model relative to the new pose. This process is repeated until the end of the segment, and we evaluate scenario specific metrics like stopping for a stop-sign, collision with another vehicle etc. during the simulation. Since the model is being used to drive the agent forward, this is a closed-loop evaluation setup.

heading: 6.3.1 MODEL ABLATION TESTS

text:
Here, we present results from experiments using the various models in the closed-loop simulation setup. We first evaluated all the models on simple situations such as stopping for stop-signs and red traffic lights, and lane following along straight and curved roads by creating 20 scenarios for each situation, and found that all the models worked well in these simple cases. Therefore, we will focus below on specific complex situations that highlight the differences between these models.
Nudging around a parked car. To set up this scenario, we place the agent at an arbitrary distance from a stop-sign on an undivided two-way street and then place a parked vehicle on the right shoulder between the the agent and the stop-sign. We pick 4 separate locations with both straight and curved roads then vary the starting speed of the agent between 5 different values to create a total of 20 scenarios. We then observe if the agent would stop and get stuck behind, collide with the parked car, or correctly pass around the parked car, and report the aggregate performance in Fig. 4(row 1). We find that other thanM4, all other models cause the agent to collide with the parked vehicle about half the time. The baselineM0 model can also get stuck behind the parked vehicle in some of the scenarios. The modelM4 nudges around the parked vehicle and then brings the agent back to the lane center. This can be attributed to the model’s ability to learn to avoid collisions and nudge around objects because of training with the collision loss the trajectory perturbation. Comparing modelM3 andM4, it is apparent that “imitation dropout” was more effective at learning the right behavior than only re-weighting the imitation losses.
Recovering from a trajectory perturbation. To set up this scenario, we place the agent approaching a curved road and vary the starting position and the starting speed of the agent to generate a total of 20 scenario variations. Each variation puts the agent at a different amount of offset from the lane center with a different heading error relative to the lane. We then measure how well the various models are at recovering from the lane departure. Fig. 4(row 2) presents the results aggregated across these scenarios and shows the contrast between the baseline modelM0 which is not able to recover in any of the situations and the modelsM3 andM4 which handle all deviations well. All models trained with the perturbation data are able to handle 50% of the scenarios which have a lower starting speed. At a higher starting speed, we believe thatM3 andM4 do better thanM1 andM2 because they place a higher emphasis on the imagination losses.
Slowing down for a slow car. To set up this scenario, we place the agent on a straight road at varying initial speeds and place another car ahead with a varying but slower constant speed, generating a total of 20 scenario variations, to evaluate the ability to slow for and then follow the car ahead. From Fig. 4(row 3), we see that some models slow down to zero speed and get stuck. For the
variation with the largest relative speed, there isn’t enough time for most models to stop the agent in time, thus leading to a collision. For these cases, modelM3 which uses imitation loss re-weighting works better than the model M4 which uses imitation dropout. M4 has trouble in two situations due to being over aggressive in trying to maneuver around the slow car and then grazes the left edge.

heading: 6.3.2 INPUT ABLATION TESTS

text:
With input ablation tests, we want to test the finalM4 model’s ability to identify the correct causal factors behind specific behaviors, by testing the model’s behavior in the presence or absence of the correct causal factor while holding other conditions constant. In simulation, we have evaluated our model on 20 scenarios with and without stop-signs rendered, and 20 scenarios with and without other vehicles in the scene rendered. The model exhibits the correct behavior in all scenarios, thus confirming that it has learned to respond to the correct features for a stop-sign and a stopped vehicle.
6.3.3 OPEN LOOP EVALUATION
In an open-loop evaluation, we take test examples of expert driving data and for each example, compute the L2 distance error between the predicted and ground-truth waypoints. Unlike the closed-loop setting, the predictions are not used to drive the agent forward and thus the network never sees its own predictions as input. Fig. 5 shows the L2 distance metric in this open-loop evaluation setting for models M0 and M4 on a test set of 10,000 examples. These results show that modelM0 makes fewer errors than the full modelM4, but we know from closed-loop testing thatM4 is a far better driver thanM0. This shows how open-loop evaluations can be misleading, and closed-loop evaluations are critical while assessing the real performance of such driving models.

heading: 6.3.4 REAL WORLD DRIVING

text: We have also evaluated this model on our self-driving car by replacing the existing planner module with the learned modelM4 and have replicated the driving behaviors observed in simulation. The videos of several of these runs are available here.

heading: 6.4 FAILURE MODES

text: At our ground resolution of 20 cm/pixel, the agent currently sees 64 m in front and 40 m on the sides and this limits the model’s ability to perform merges on T-junctions and turns from a highspeed road. Specific situations like U-turns and cul-de-sacs are also not currently handled, and will require sampling enough training data. The model occasionally gets stuck in some low speed nudging situations. It sometimes outputs turn geometries that make the specific turn infeasible (e.g. large turning radius). We also see some cases where the model gets over aggressive in novel and rare situations for example by trying to pass a slow moving vehicle. We believe that adequate simulated exploration may be needed for highly interactive or rare situations.

heading: 7 DISCUSSION

text: In this paper, we presented our experience with what it took to get imitation learning to perform well in real-world driving. We found that key to its success is synthesizing interesting situations around the expert’s behavior and augmenting appropriate losses that discourage undesirable behavior. This constrained exploration is what allowed us to avoid collisions and off-road driving even though such examples were not explicitly present in the expert’s demonstrations. To support it, and to best leverage the expert data, we used middle-level input and output representations which allow easy mixing of real and simulated data and alleviate the burdens of learning perception and control. With these ingredients, we got a model good enough to drive a real car. That said, there is room for improvements: comparing to end-to-end approaches, or investigating alternatives to imitation dropout are among them. But most importantly, we believe that augmenting the expert demonstrations with a thorough exploration of rare and difficult scenarios in simulation, perhaps within a reinforcement learning framework, will be the key to improving the performance of these models especially for highly interactive scenarios.

heading: A SYSTEM ARCHITECTURE

text: Fig. 6 shows a system level overview of how the neural net is used within the self-driving system. At each time, the updated state of our agent and the environment is obtained via a perception system that processes sensory output from the real-world or from a simulation environment as the case may be. The intended route is obtained from the router, and is updated dynamically conditioned on whether our agent was able to execute past intents or not. The environment information is rendered into the input images described in Fig. 1 and given to the RNN which then outputs a future trajectory. This is fed to a controls optimizer that outputs the low-level control signals that drive the vehicle (in the real world or in simulation).

heading: B PERFORMANCE

text:
The model runs on a NVidia Tesla P100 GPU in 160ms with the detailed breakdown in Table 3.
C VISUAL EXAMPLES
Fig. 7 shows an example of perturbing the current agent location (red point) away from the lane center and the fitted trajectory correctly bringing it back to the original target location along the lane center. Fig. 8 shows the various predictions and losses for a single example processed through the model.

heading: D OPEN LOOP EVALUATION ON PERTURBATION DATA

text: We also compare the performance of models M0 and M1 on our perturbed evaluation data w.r.t the L2 distance metric in Fig. 9. Note that the model trained without including perturbed data (M0) has larger errors due to its inability to bring the agent back from the perturbation onto its original trajectory. Fig. 10 shows examples of the trajectories predicted by these models on a few representative examples showcasing that the perturbed data is critical to avoiding the veering-off tendency of the model trained without such data.

heading: E SAMPLING SPEED PROFILES

text:
The waypoint prediction from the model at timestep k is represented by the probability distribution Pk(x, y) over the spatial domain in the top-down coordinate system. In this paper, we pick the mode of this distribution pk to update the memory of the AgentRNN . More generally, we can also sample from this distribution to allow us to predict trajectories with different speed profiles. Fig. 11 illustrates the predictions P1(x, y) and P5(x, y) at the first and the fifth iterations respectively, for a training example where the past motion history has been dropped out. Correspondingly, P1(x, y) has a high uncertainity along the longitudinal position and allows us to pick from a range of speed samples. Once we pick a specific sample, the ensuing waypoints get constrained in their ability to pick different speeds and this shows as a centered distribution at the P5(x, y).
The use of a probability distribution over the next waypoint also presents the interesting possibility of constraining the model predictions at inference time to respect hard constraints. For example, such constrained sampling may provide a way to ensure that any trajectories we generate strictly obey legal restrictions such as speed limits. One could also constrain sampling of trajectories to a designated region, such as a region around a given reference trajectory.

title: LEARNING TO DRIVE BY OBSERVING THE BEST AND SYNTHESIZING THE WORST