Algorithmic Improvisation for Dependable and Secure Autonomy

>>We’re very happy to welcome Sanjit Seshia, was
a Professor at UC Berkeley. Sanjit is a longtime friend
and collaborator. He has visited us
many times and today, he is giving a talk on
algorithmic improvisation for dependable and secure
autonomy and I guess based mostly on the PLDI paper recently or maybe broadly many
other things as well. Okay. Welcome, Sanjit.>>All right. Thank you, Sriram.
It’s always good to be back. In fact, today’s talk is really a combination of two previous talks I’ve given here on previous visits. So back about four years ago, I spoke about
algorithmic improvisation which at the time we had
just done the theory, some of the initial
theory work on it. So it was really more
of a theory talk, in the sense of CS theory. Then later, when I was here for a longer period of
time two years ago, I talked about our work on
semi-autonomous systems, autonomous cars
interacting with humans. That’s the second part and
really, this talk is where both of those come
together and it’s as usual work that’s joined with many excellent students,
and post-docs, and colleagues, and in
particular Daniel Fremont, whose name you see at the beginning is the PhD student who
did much of this work so a lot of credit to him about
what I’m talking about today. So the context for
a lot of our work here is what we call Human
Cyber-Physical Systems which is, so cyber-physical systems are computational systems interacting
with the physical world and Humans Cyber-Physical
Systems are CPS where they also interact with humans and that’s
a critical component of the overall functioning
of the system. So there are many examples
shown here on the slide. So at the bottom right you can see cars with self-driving features, not fully self-driving but there’s a person in the car whom the system has to interact with, there are people outside the car that it also has to interact with. You also see things like humans working with
robots like in the top left or robotic surgery
and things like that. So these things are already
becoming real and many of them as you can see in
this picture are safety critical. They also are systems that operate in fairly
complex environments like cars with such driving features. So the challenge of ensuring they are safe and correct operation
is quite a large one. Just if you’ve been following
the popular press you know that this challenge is already caused
some unfortunate incidents. Like this is a picture of the investigation of
the fatal Uber crash. While the final report
is still not out yet, last year in the initial
report there were hints that software
and algorithms and especially it could be AI machine learning based
perception algorithms could have been one of the factors. So if you look at a snippet
from the report it says that in fact, the car’s detection, the perception system
observe this lady who was walking her bicycle
across the road in front of the car that was in
self-driving mode and that happens six seconds before
impact which is for a reasonably alert driver, enough
time to avoid the collision. But in fact, the vehicle was
confused about what it was seeing. So there seems to be
certainly some hints that the perception played a role. As we all know, AI and
deep neural networks are very commonly used in
perception these days. So it’s conceivable that if we
don’t know the details but it’s probably deep learning-based system
may have been used there. Okay. So that’s just an example. In my group what we tried to do is take formal methods which is
an area this lab knows well which are really mathematically
based techniques that are also algorithmic, that
are also automated to model, design, analyze systems, and about three, four years ago, I and my colleagues,
we tried to understand what are the special challenges that AI based systems bring to
the problem domain for ensuring correctness in
verifying the systems. So that’s the paper
we wrote down there. What we are trying to do is prove rigorous guarantees about the safety of the system when that’s possible. That’s not always possible because these systems are
very complex and also the environments are
probably impossible to model in complete generality to capture all possible
behaviors in a sound way. So what we at least want
to do in those situations is use formal methods to guide, to search for bugs or
unsafe scenarios, and to do that in a way that complements work on testing and simulation so that you gain higher assurance. Okay. So a lot of what
I’ll talk about today is really more on
the second category. Okay. But this talk
really is also about this topic of
algorithmic improvisation. So far I’ve just talked
about the challenges in autonomous and
semi-autonomous systems. So what this talk is about is
that randomness can actually play a crucial role in the
use of formal methods for improving safety and
security of autonomy. Okay. Some of the places where we found randomized
algorithms to be useful is first of all in modeling
an anonymous algorithms but also formalisms that
can capture randomness, as in first of modeling autonomous
systems and their environments. Then in doing verification
and here we’re actually trying to
draw inspiration from the use of randomized algorithms in hardware verification
and verifying chips. So things like constraint
random simulation and probabilistic verification. Then finally, we also are looking at the use of randomized
algorithms in synthesis. In synthesizing plans or control strategies for
autonomous systems. But the idea here is that
the plan or the controller itself is randomized, is
anonymous algorithm. Okay. What we found
is there are problems where you really want
that. All right. So just to summarize some of the contributions that
I’ll speak about today. So I’ll talk a little bit about
randomized controller synthesis. This is based on work that was
presented at CAV last year. The idea here is to, for a robot to produce lots of
different trajectories for the robot to explore
so there’s a diversity but it’s also, each of
them obeys safety. We’ve also done a lot of work
on modeling human behavior. As one can expect, human behavior is random
in different ways. So the same person exhibits
different behavior on different days at different times. Of course, a population, there’s usually some variety
over their behaviors. So if you want to model
human behavior for these Human CPS, then it turns out
randomness is useful. Then we’ve also recently used
it for systematically training and testing Machine
Learning models by generating diverse
and tunable datasets. The nice thing really here is that these three looks like very
different applications, but the core theory
that’s behind all of this is the stuff I talked
about four years ago, which is this topic of
algorithmic improvisation. So first, what I’ll do
in the next few minutes is give you a little bit
of more detail on these applications about
where randomness comes up, and then I’ll talk
about improvisation. So this first application, the most recent one that
appeared at PLDI is about generator for generating training and test sets for neural network that
does object detection, in this case, detecting cars. So what you’d like to do is
generate a diverse dataset. The challenge here is
that if you say, okay, the scenario I want to
test the neural network on is bumper to bumper traffic,
then even that, there is not one way in which bumper to bumper traffic
manifests itself, and you’ve seen
three photographs down here where the environment
around the traffic is different, the lighting conditions
are different, the time of day is different, the spacing between cars maybe
different, models of cars, the colors, there’s lots of
details that can be different, but they all share
some common characteristics. So if you’re generating the data, you want to be able to cover this and randomness helps you do that. Another reason for
randomness is again, in modeling human behavior. So here’s an application where statistically one of
my colleagues actually, the idea here is that if you’re away from your home on
vacation for a while, but you want to make sure
that potential burglar doesn’t know that
this home is unoccupied, then you get these devices
which turn lights off on and off at
certain fixed intervals of time, but that can be deterministic and therefore easy for
a burglar to know that, oh, it’s turning on at seven in the evening and then
turning off at 10. So you want to randomize that. But you want to randomize it
in a way that is realistic. That mimics typical human behavior. Somebody gets up in the middle of the night to go to
the fridge to get something, so that can happen, but it
doesn’t happen all the time. So you want to be able to mimic that, that it turned out
to be actually used improvisation for exactly
this application. Then finally, if you think about robotics surveillance
as an application, so here the idea is imagine that is a drone that has to patrol an area, and you have to come up with
a trajectory for the drone. If you come up with
the same trajectory every single day when
you fly the drone, then the adversary
on the ground knows exactly 09:00 PM it’s
going to be here, at 10:00 PM it’s going to be there, and so they can plan
the bad stuff accordingly, right. So what you want to do is really
randomized the trajectory. Of course, you can’t do a completely
random thing because we all know energy constraints and
there’s like other constraints, and you also want to maintain safety. So this is another example
where randomness is useful, but complete randomness
is not going to cut it. Okay. I’ll explain the animation
at the bottom very soon. All right. So what’s going on here, there are three
different applications. Randomness plays an essential role, but we also know that it’s, from my description, completely
random behavior also is not good. In the first case,
you want to make sure that we satisfy constraints like the turning on and off lights is
realistic and it uses less power, then second, the images
you generate have to satisfy certain realism constraints, and then the third, you have some safety specifications
and other things like that. So the core problem here is you want to synthesize random behavior, but you also want that to
be controlled in some way. That’s the core mathematical problem, that is what we call as
algorithmic improvisation or what we previously called
it as control improvisation. It’s really a framework
for automatically synthesizing systems
with random behavior that also satisfy formal guarantees. The systems could be reactive or not. This term reactive is
used in formal methods to talk about systems
that have to operate in adversarial environments and they have to interact with
those environments. So what you want here are two kinds of things to
consider guarantees, first we call it guaranteed safety. So you may have what we’ll explain as hard and soft constraints
on the behavior, and then you also want
guaranteed randomness. Now, the first, Guaranteed safety, that’s a very common requirement
in formal methods, but guaranteed randomness is
slightly different beast. So here what you want
to say is that you want a system that exhibits random behavior in
a prescribed fashion. I want to see some specified
distribution over the behaviors. That’s one of the key novelties here, that the requirement
for random behavior is in fact part of
the specification itself. All right, so now for
the rest of the talk and maybe the next 40 minutes or so, I’ll explain what control
improvisation is at the beginning, I’ll give you the
mathematical definition, I’ll go through some of
the motivating applications again, then I’ll dive into the theory
of controlling proposition, which is really about
when can you device efficient algorithms and what’s
the complexity and so on, then I’ll pop back
to the applications, and I’ll focus in particular
on one of them the most recent one that
appeared at PLDI, which is on design analysis
of perception systems, and then I’ll conclude and
talk about future work. So let’s talk about
controlling improvisation. So I’ll go back to this robotics
surveillance applications. So here, at a high level, the specification is you
want to patrol an area in a way that is hard for
the adversary to predict. So what you’re seeing in
that picture up there, and I don’t know how to get rid of that banner at the top
unfortunately but, okay, it’s blocking the way. So you just have to
use your imagination. So there’s a black line and
then a blue dashed line. So the black line, there’s a triangle at the bottom, that’s the starting location, the triangle at the bottom
is the starting location of the patrolling robot. So the black line is
the patrolling robot. If you can get rid of
the top bar, that will be great. Now, the four red circles
in the middle are locations that the
patrolling robot has to visit. Then there’s this blue dashed line, there’s a triangle at the top right, and that’s an adversary robot
or adversary agent, the adversary agent is trying to basically collide with the black one. The specification is you first
of all, you want the robot, the black line to visit
each location sufficiently often, you also want it to take
a route that’s closest to the shortest possible one
to those red circles. But you also want some
diversity in the routes, every time you run it you want
hopefully a different route. So the first kind of
constraint we’ll call as a hard constraint because
here it’s the job, the patrolling
specification, so you want the robot to be able to
visit all those locations, so it’s a property
that it must satisfy. The second one, we’ll call it as a soft constraint because
there’s a metric, like the distance
and there’s a notion of being close to the shortest, so you don’t necessarily
want the shortest but you want to get within some
epsilon factor of that. Then the third is a
randomness constraint, which it’s not obvious there but
you might imagine that you want some distribution over
the possible routes. Now, this surveillance thing may look like potentially a toy application but this is something
that we were able to implement on a robotic platform, and then this is showing
a deployment in the lab. So there’s a top view, those blue things are obstacles, the white squares,
papers are locations. The location on the extreme left
is a charging location, where it has to visit
every now and often, and then other waypoints
that it has to visit, I’ll probably get to the
specification later in the talk, but the main point I
want to make here is that this control improvisation thing is something that we’ve got a pipeline down to
actually robotic platforms. So that’s application number one, and I will talk a little bit more
about that maybe in 10 minutes. The second application is this
data generation application, the idea there is you’re
training a neural network for example for autonomous vehicle, that has to detect objects around it, and you want to generate
a diverse set of images. The way people actually
do this sort of thing in autonomous car companies
is as you might know, they actually go and drive around, collect lots of images, real images. But the challenge with that
is you get the common case, but you may be missing
the edge cases, and also the edge cases can
occur in different ways. So if you actually come across
a construction site one day, and they have one
construction site set of images one day out of 1000 days, but that may just
have certain specific characteristics and
your neural network may overfit to certain properties
of that particular thing. So you want a diverse set
of images for every possible scenario that
your autonomous vehicle can be in, so there’s a lot of interest
in doing this synthetically using rendering engines for
games and for simulators, so that’s the context here. Even if you do that,
you want the generation to satisfy some constraints like the objects in the image
shouldn’t intersect, so you want realistic stuff. You want a notion of similarity, so you want that synthetic data
to be close to real-world data, and then you also want diversity. So the way we can also think about this is the first
is a hard constraint, every image should
satisfy that constraint, the second is like
a similarity notion, that’s like a soft constraint, and the third is again,
randomness constraint. So two applications,
and there’s actually a number of other
applications that we have found over the last
four or five years. The roots of this
work are actually in a collaboration I had with
a Professor of Music at Berkeley, and that’s something that I talked about in my talk four years ago, so this whole idea of
improvisation actually grew out of a conversation I
had with David Wessel on the use of algorithms
to make a program improvise the way
a human musician would. They actually had work on
music improvisation approach for jazz but for other music that could have
certain symbolic encodings, then we also looked at fuzz testing, so alpha fuzz testing also has very similar characteristics that I can tell you about
if you’re interested. Now, I’m going to try to move
to a more abstract level, so if you think about all the
applications I have seen so far, they are about data generation. You can think of data
in the same way as you might have learned in a
theoretical computer science class, like a Turing machine operating
on a sequence of symbols. So think about your data as
encoded as a sequence of bytes or some symbols
from a finite alphabet, so your data generator is
generating these kinds of sequences subject to
three kinds of constraints. The first is a hard constraint, that is every sequence
that comes out of data generator has to
satisfy some property. Second, it’s a soft constraint, in this case, I’m going to take a particular instantiation of soft constraint, which
is probabilistic, so you’re saying that
this generator is random and more sequences that come out
of it satisfy some property. The third is a randomness constraint, which is a constraint on the output
distribution of the generator. So we say that
a data generation problem whose output has to satisfy
three kinds of constraint is an instance of
control improvisation. What we realized at the
time is when we looked in the literature in the theoretical
computer science literature, there really wasn’t
anything like this problem, so there were
other problems that people had explored both in
the theory and in the motor systems literature on problems that have
some characteristics of it but nothing quite like it. So what you’re seeing here
is just a selection of related work columns in a hard,
soft, random, and reactive, these are the properties
of the problem. So do you have to generate data subject to hard constraints
at the first column? Second one is subject to
soft constraints, etc. The last column is, is it
also in this context of a reactive setting where the system is interacting
with the environment? So if you think about
things like fuzz testing, so mutational fuzzers
and generative fuzzers, there are typically some constraints on the type of test
cases that you want, file formats and things like that. You may have some
randomness constraints on, “I want to generate
something that is uniformly at random from the space
of possible inputs.” But it doesn’t have
all three of those, it doesn’t have hard soft and reactive and there’s
no notion of hard, soft and random, it doesn’t
have a notion of reactivity. There’s also informal methods, there’s this area called
reactive synthesis which is synthesizing planners
from specifications, so there there are constraints
with other specifications but it doesn’t have
any notion of randomness. So that’s just a selection of things, so that’s what made us
feel like there’s actually a lot more to be investigated
here just in terms of the types of
theoretical problem here. So now, I’m going to walk you
through this little example but also illustrate what control
improvisation is in a formal sense. So as I mentioned
before, the problem is to generate sequences of
a certain prescribed length, let’s call that N from
a finite alphabet sigma. So for this little problem here, let’s discretize what
the robots do into, say the robot has to take
steps to move around, and each step is going to be moving North, South, East, or West, so the alphabet of actions
for the robot is NSEW, and let’s say it can take
at most 30 steps, N is 30. The hard constraints are going
to be that it has to visit all the circles and it
has to avoid collisions, so there’s the robot
up in the top corner or the agent up in the top corner,
which is the adversary. Then the soft constraint is
going to be that you don’t want the path to be redundant in
the sense of you don’t want the location to be visited twice, if you’ve visited the circle already, you don’t have to go back there. But we leave it soft because
sometimes to evade the adversary, you may need to go back
to where you were before. So hard and soft constraints, I’ll talk about the
randomness constraint later, so now let’s think about the space
of all possible trajectories. So that’s going to be sigma to the N, all possible sequences
of actions of length N. Some of them are going
to be bad sequences.>>Yeah. So [inaudible]. It seems like there could
be two ways, right? One is to use randomness, the
other is to also consider where diversity is as
one of your inputs. Would you do both, or
do you do only one?>>Yeah. So if you want to
avoid the adversary and that’s the only thing and there’s
no other requirement, then what you’re saying
is absolutely right, you react to where the adversary is. The missing part of
the specification here is the randomness requirement. So you also want to make it hard for the adversary to
guess where you’ll be, not because the adversary
will collide, but because the job
of patrolling is to actually make the path
of this hard to guess. it’s like think of a museum robot. So the museum robot takes a route, trying to go for drive
around the museum, and you want to make sure that the burglars don’t know where
the robot is going to be. So that’s the other part
of the specification here. So Sigma to the end of the set
of all possible paths, and some of them are bad, the ones that collide in this case. So what you want is everything that
excludes the the bad behavior. So you want things that
satisfy the hard constraint,. So that’s the red set here,
we’ll call that capital I. Now, this red set could contain things that violate
the soft constraint, like visiting the same circle twice. So ideally what we’d like to be
is inside the light blue circle, which is the set of
all things that satisfy also the hard and soft constraints. But there’s also this randomness constraint which I
haven’t talked about yet. So that’s going to be
the next part of the definition. So here’s the formal definition of a control improvisation problem. You’re given a hard constraint H, a soft constraint S, a length n, and then you are given
for the soft constraint, there is a probability with
which you can violate it, which is epsilon and
then you’re given some parameters Lambda and Rho. First of all, we’re going to define what’s an improvising distribution. So this is something that maps
sequences to probability, so assigns probability
masses to sequences. The first hard constraints says that, everything in the support of the output distribution has to
satisfy the soft constraints. So it has to be in I, the red set. The soft constraint says that, with probability 1 minus epsilon, you have to be in the light blue set. The randomness requirement, which I haven’t talked about
yet, but here it is, is that for every sequence
that’s in capital I, the red set, the mass
you assigned to that, has to be between Lambda and Rho. So Rho as an upper bound,
Lambdas are lower bound. So the way to think about
the anonymous requirement here, is that the Rho is
seeing something like don’t generate
any sequence too often. It’s an upper bound on on
how often you generated. The Lambda is saying,
generate at least so much, and what we found as
Lambda and Rho can be useful in different
applications in different ways. So for example in first testing, you want a lower bound typically, because you want to be able
to hit every sequence. The upper bound is
not that important. In the case of music or
even this patrolling example, the upper bound becomes
more important, because you want a
diversity of output. So that’s the thing. So we really can play
with these parameters depending on the application. Also the interesting thing
is, using Lambda and Rho, you can specify distribution
requirements as well. So you can specify
uniform random distribution, using Lambda and Rho for example. Okay. So yeah, question?>>Reactive [inaudible].>>I’ll give the reactive
definition next. All right. So this is
the non-reactive settings, the environment is not reacting
to what the system does. So a problem instance is
going to be the sixth tuple, which is hard constraint,
soft constraint, length, Epsilon, Lambda, Rho, and we’ll say that the
instance is feasible, if an improvising
distribution exists. So not all instances are feasible, and then a improviser itself
is a probabilistic algorithm that samples from
this output distribution. So again, this little toy example. So let’s again for the sake
of argument imagine that the cardinality of
capital A is just three, there are just three parts
possible, A1, A2, A3. Then let’s say that in I
minus A, which is things that satisfy the hard constraint
but not the soft constraint, there are two sequences I1 and I2. One strategy I can use if I
say that I cannot generate any sequence with probability
more than a quarter, so Rho is a quarter. So I can’t generate any sequence
probably more than a quarter, I can’t simply sample
from the light blue set, because I’m going to go above a quarter because
there’s only 3 of them. So what I need to do is, sample from light blue
some of the time, and then sample from the red
that is outside the light blue, some of the time. One possible strategy
is to sample I1 and I2 with probability one over eight, and then A1, A2, A3
probably 1 over 4. This is again, highly
simplified example where you can actually see, the elements of the set typically
the sets are really huge. Now, let me get to the question
that was asked which is, how do things change in
the reactive setting? So in this case the adversary
is actively trying, it’s not just driving
some fixed route, but actively trying to chase
and collide with the robot. So the setting here
is very similar to the traditional
reactive synthesis setting, whether you can model
it as a two-player game between the system and the adversary, and we’ll think about it
as a turn-based game. So first, the robot moves and
then the adversary moves and so on. The main way in which we lift the definition to the reactive
setting is we say that, we need to satisfy the hard-soft
and randomness constraints for every possible adversary. No matter what the adversary does. Then we go for the improviser is
not just generating a sequence, but has a strategy, which is basically you can think
of it as a branching structure, where the improviser mixes step, and then if the adversary does this, then it’ll do something, if
your adversary does something else, it will do something else, etc. This whole thing is bounded time. So we’re only looking at strategies
that will run for length n, so that’s one key point
of difference with the traditional literature
on reactive synthesis. So for this little toy example, the hard constraint is the same, you want to visit the four circles
and avoid the adversary. The soft constraint is also the same, except I now have a probability
I want to say that, three-fourths of the time, I will
visit each circuit exactly once. The random list requirement is that only have a row and upper bound, and actually want the smallest
possible upper bound. So in this case it turns out to
be around 10 to the minus 12. Using this, we can
actually have a generator that takes in these constraints
and introduce plants, like the ones that you
see animated here. Good. So now so far I’ve
talked about the definitions, so control improvisation and then reactive controlling
improvisation, now I want to talk about
algorithms and complexity. So the first question is, if
I have a problem instance, when is it even possible to solve it? Doesn’t solution exists,
and how do I find that? Now, to our pleasant surprise, it turned out that this question
is quite easy to answer. Easy in the sense of mathematics, not that easy computationally though. So it just requires these sets
I and A to be large enough. So remember, I is the set of
all possible improvisations, everything that satisfies
hard constraints, A is the set that satisfies
additionally the soft constraint. The theorem we have is if you’re
given a problem instance, then it’s feasible that
it’s solution exists, if and only if the set I, set of all possible improvisations
is at least one over Rho. Rho is the probability that upper bound probability
on generating any output, and then the set A, which also
satisfies the soft constraints should be at least one
minus Epsilon over Rho. What’s actually interesting about
these inequalities is that, they match what you
might think intuitively, because for instance
for the first one, if I was not as big as one over Rho, then you’re not going
to be able to sample from within I with
probability at most Rho, there’s not enough things in it, and similar reasoning for A. But the nice thing is this theorem
works if and only if. If you are interested
in the reasoning, you can go over it later. All right. So now what do you need to do then? You have to be able to
count the cardinality of I, and count the cardinality of A, and then just compare
with these inequalities. Now, if I and A small,
that’s not a problem, if I and A are huge, and they’re presented
to you symbolically, that can be challenging. It’s like typically a
sharp P complete problem. So that’s the
computational challenge. But at least in the terms of
the mathematics, it’s very simple. So now, what is an improviser? What is the problem we’re solving? So first, we have
his notion of what we call an improvisation scheme. The idea here is, you have
a problem instance and the improvisation scheme
is something that takes a problem instance
and produces an improviser, so it produces an algorithm such that every time you run the algorithm
and it does something different, and that’s what the output is. That’s an improviser. So
think about this as really a synthesis algorithm in
the sense of program synthesis. The orange box is
generating a program. But the program is
a probabilistic program, and now what we want is an efficient improvisation scheme,
ideally polynomial-time. So what that means is that if I have a certain class
of problem instances, then what I would like is a scheme S such that given any problem instance, if that instance is feasible, it will return an improviser,
otherwise bottom. So this is just saying that
you want it to be correct, Then the second is saying that, the scheme as well as
the output algorithms it generates, have to run in time that’s polynomial
in the size of the instance. So that’s what we want ideally. A polynomial-time
improvisation scheme that also generates
polynomial time improvisers. Now, in the initial work on this, we didn’t really have
a clear idea of how to do this as the specification
type changes. So hard and soft constraints, I’ve kept them pretty
abstract so far. They’re just sets of behaviors. But in program verification, we know there are many
ways in which you can write specifications and some of them are more
powerful than others, and so what we’ve found
is that the complexity of the problem varies with the type
of specification you write. But what’s really nice and
this is all due to Daniel, is that we found
a common meta algorithm that works for
all specification types. It’s like a generic improvisation
scheme that works if you can do four things really on
the types of specifications. So first, you want to be able to
think of specifications as sets. So you should be able
to intersect that sets and take the set difference, which is typically
quite easy and it works for all specifications that are sets. Then the second thing is you
want to look at specifications that are over
bounded length sequences. So some specifications are not, they over infinite length
sequences and those are not things that we are looking at. Now, the third and fourth
are the tricky ones. So you have to be able to count the number of words
that satisfy a spec, and the fourth is you need to
be able to sample uniformly at random from the set corresponding
to the specification, and these can be
nontrivial as I mentioned. So for instance if your spec
is just a Boolean constraint, then this is essentially the problem
of model counting the number of satisfying solutions or sampling from the set of satisfying solutions. But if you can do
those four operations, and you can do them efficiently, then there’s a polynomial time
synchronization scheme, and this is how it works. You construct the specification that correspond to
the hard constraints, I, the soft constraints A, and then the set
difference of the two. You count I and A and you check those feasibility inequalities,
and if it’s feasible, then there’s a very simple algorithm but you can just sample from either I minus A with
the right probabilities, and of course three is
a highly abstracted version of the actual algorithm
which is in the paper. But that’s how it works, and so it just uses
those four operations as oracles. So what can we do efficiently? So it turns out, if
your specifications are DFAs, so they’re regular languages
that can be expressed as DFAs, then you have a
polynomial time scheme. If it’s an unambiguous CFG which can be the case for
testing applications, then also it’s polynomial time. Yeah.>>Questions. How would the
reactive system be modeled to DFA?>>So remember this is, so far
this is not the reactive setting. This is the non-reactive setting.
I’ll get to the reactive setting. But you can think about
in the reactive setting, you’re looking at things like
safety games or reachability games. So the controller, the system
is a finite state transducer. The environment is similar. So that’s the correspondence. Here of course we are in the->>Then you’re basically [inaudible]>>Exactly. It’s common [inaudible] , and remember, here we’re
talking about DFAs as opposed to Buchi Automata because they’re
all finite length sequences. But anything more than DFAs and unambiguous CFGs gives
us higher complexity. So we have polynomial time
for those two cases., and then if you have
a regular language but you’re expressing it as an NFA, then the algorithm, I mean
we can’t find anything that is better than sharp P in
the size of the specification, and it turns out, I’m having,
completed this picture. But if you have specifications
that are more complicated, it can even become undecidable. You could think of the specification
as given as explicit form. If you give it in symbolic form, then we can have approximate
polynomial time improvisation schemes that assume that you are using
a SAT-solver as an oracle. So you just count the number
of calls to a SAT-solver not the actual complexity of
solving SAT. All right. So now to the reactive case. So it turns out again the
feasibility for the reactive setting is very similar and also
reduces the counting. But you’re counting
something different. You’re counting not the
cardinality of the things in the specification but the number of ways the system can win
the, two player game. But the inequalities
look almost exactly the same except what’s on
the left-hand side is different. So what that thing is, is something we defined
called the width of the game which is the
number of winning plays. So play is basically a sequence of actions alternating
between the system and environment between
the two players, and so if the width of
the game is big enough, then the problem is feasible. That’s what it means. For
the interest of time, I’ll skip over the definition. But the gist of it is that it turns
out that the feasibility check is very similar to what we
had in the non-reactive keys. Now, what can we do in terms
of efficient algorithms? Again, for DFA specifications, we have an efficient scheme
and what we mean by DFA specification is really that the play if you think
about it as a sequence of symbols alternating
between the two players, that should lie in a regular
language represented by DFA. There are other ways of
representing regular languages that also give us
polynomial-time implementations. But anything more than
that including NFAs, CFGs, and then also versions of
Linear Temporal Logic, and linear dynamic logic
for finite line traces. All of those are higher complexity
turns out to be P space. But a comment there. So this is exactly
the same complexity as standard reactive synthesis. So coming up with
a randomized strategy seems to be no harder than coming up with a deterministic strategy
which is nice. So anyway that was a bit of
a whirlwind tour of the theory. But I hope I could give you
a sense of what is there. Now, I’m going to get into
a lot more practical stuff. So we’ll talk about
this application of designing analyzing
perception systems. So the motivating example here is
you have an autonomous vehicle, you have a camera in
front of that vehicle. The output of the camera is
fed to a deep neural network that has to essentially
detect what’s in the scene. So what is really
this notion of a scene? This word is used quite informally. So for us, a scene is
a configuration of objects in 3D space along with the
attributes of those objects, and possibly if
those objects are dynamic, then attributes of the dynamic
objects like the velocity of the car heading at which it’s
heading at the current instant and then that over a period of time. As I mentioned, what people do a lot is drive around and collect data. That’s pretty expensive
but it’s also not going to produce a comprehensive data-set
especially of edge cases. So we’re looking at this case
of what’s simulations to run to generate diverse dataset. The challenge with
that is that this is a very large high dimensional space. So if you just think about I want
to generate images of a car, then there’s a lot left unspecified. Like what’s the model of the car? Where is the car in the frame? What’s the orientation? Are there other cars around it, and what’s the time of
day? What’s the weather? So there’s lots of
other implicit geometry constraints that come with each domain. Yes, I’m talking about cars here, but a lot of the stuff I’m
talking about in this section of the talk also applies
to other scenes. Then you might want
to specialize it and focus on a particular type
of scene like, I want to look at highway traffic
not city traffic. So it turns out that
this data generation problem is also another instance of
control improvisation. As I’ve mentioned before, you have these hard constraints which are saying that things
don’t intersect, for instance, then you have soft constraints which
are like similarity, and then you have
some randomness thing. I want to be able to generate images uniformly at random that
satisfy these constraints. So the soft constraint
could be something like, I want to generate bumper
to bumper traffic scenes of which most of them, 80 percent
of them should be daytime. You might say, oh, the gap between the car she follow
certain distribution. So how do we encode these? So we thought about
this and we could have gone with the hard-soft
and randomness constrain that we used in the previous case for
this robotic planning example. But instead what we found
is that it’s a lot easier to create a domain specific language to help people just write
these specifications, and in fact, because
the specification, some of them are probabilistic, a probabilistic programming
language seem to be the right fit.>>So this is also [inaudible].
This is non reactive.>>In this case, it’s not reactive. So in the case of reactivity, I’m just talking about
writing the specifications. So you could still write the
specification in this way. Then you would have to specify constraints on what the
environment can do. I suppose you could
also specify them here. What you’d have to do is extend
the specification language to be able to talk about
sequences of actions. Right now, we don’t have
that capability yet. It will, for example, write
temporal logic properties, something like that, in the language. You can do this in the
language currently by explicitly writing
down constraints over parameters that
encode a sequence. So the short answer is, yes, you can do it with
the current language but it’s not elegant. So
what the language is? The language that we’ve
created is called Scenic. What it does is it helps you define a distribution over possible scenes. Remember a scene is
configuration of objects in 3D space along with the
attributes of those objects. So for instance, if your scene
is bumper to bumper traffic, it turns out it’s
about 20 lines of Scenic code. Scenic is a DSL. So we have designed it
in a way that we can write concise short programs
that are also readable, that can capture
common geometric relationships. Furthermore, one of
the reasons to design a DSL is because the back-end
sampling techniques, some algorithms can be made much more efficient because of the ability
to exploit domain structure. Then we can write
your hard and soft constraints similar to other “Controller
Improvisation” settings. So one of the ways we envision the use of Scenic is to design
an answers, perceptions systems. So like neural networks that
are used to detect objects. So the way this works is you
start with a Scenic program. I’ll show you an example of it, but you already see what the syntax looks like which is down there. It’s like a cross between
English and Python. So it goes through the interpreter
which is this Scenic sampler. Each time the interpreter runs, it produces a scene. A scene as an actual configuration. So a Scenic Program defines
a distribution over scenes. The sampler, the interpreter,
each time it runs, it produces one scene, and that’s
like a layout that you see here. So it’s like a schematic layout
of where the car is, where something else is, etc. You take that and you feed this to a simulator or a renderer
and that produces a data. So a lot of simulators
of game engines have some kind of
format, input format. Basically, we translate the output
of Scenic into that format. Yes. Question.>>Where is the
improvisation scheme here?>>Yeah, good question. So
the improvisation scheme here is really in the generation
of the sampling strategy. I’ll have one slide about it,
but there’s this small area.>>So this one scene like
one clip or one series of clips like a video because
password change positions.>>Exactly. Yeah. So for this app, what I’ll talk about
different applications have different notions of
what a data item is. So in the case of
have a neural network that has to detect
an object in an image, a data item is one image. The use of Scenic, which I’ll
show at the end of the talk, where do you want to
find counterexamples for an autonomous vehicle controller but it shows that he
has a sequence of actions that takes
it into a bad state, there it is a sequence. So the Scenic can do both. So here, the application
we’ll talk about for the next five minutes is just images. So you can generate test data, you can generate
training data as well. You can use that to
augment real data. So one of the applications
that we use Scenic for is to debug things like neural networks
for object detection. So here, this is a concrete example
of an image we generated, and this is all generated using the Grand Theft Auto V game engine. So that’s a car with
a racing stripe on it. One of the best academic object
recognition neural networks, that is out of Berkeley
thought that there were three cars, three bounding boxes,
but there’s just one, and also with reasonably high
probabilities, or confidence levels. So we went back to the people
who created this and we said, “Okay, here’s a example
of a buggy input.” They thought maybe
it’s the racing stripe because data said it typically
doesn’t have cars like that. What we were able to do is
use the Scenic program that generates this and then do
Delta Debugging on that program. So it changed the model of the car,
the position of the car, etc., and do this efficiently and what
we found is actually it wasn’t the stripe at all and was
something really weird, like the distance between
the camera and that car. Anyway, so you can do that sort
of thing with Scenic. It’s a probablistic programming
language and there’s been a lot of work on probablistic
programming language, including here at Microsoft Research by Sriram and other colleagues. So I just want to situate
Scenic in that work. But before that, let
me take the question.>>Yeah. So one thing I
was quite curious about the previous example that
you mentioned is that typically was the picture
discovered first and then the Scenic program
written or was the Scenic program written first and then the
counterexample discovered?>>Yeah, good question. So
these two use cases for Scenic. So one is you can write
a Scenic program and you can use it to generate data and
then you can find misclassifications. So that’s one. Once you’ve found
a misclassification, then you can think about doing Delta changes to
the Scenic Program. The point is, once you have
a program that is generating data, it’s much easier to explore
the neighborhood as opposed to the typical
adversarial example thing where you’re like perturbing
pixels or whatever. So we want to be able to
find out what is going on? Why did the neural network come up
with a bad output in this case. Having the program, the Scenic
program in the first place, makes it a lot more useful.>>So should I think
of the Scenic sampler? [inaudible] like sampler?>>The Scenic sampler,
actually, you can use any of the techniques that have been produced and published
in the PPL community. In fact, our existing sampler, the first sampler which we already did pretty well is just
doing reduction sampling, but you could use MCMC,
in some certain cases, you could actually even use
the work that’s been done in random sampling from SAT problems.>>Just because it seems that this is quite interesting from
a computer graphics point of view. I think this can be used to generate several Siggraph papers
which came out. So what they were trying to do is do fancy stuff for number one
was about furniture layout, you want to layout the furniture.>>Correct.>>There was one about you have
some papers and you want to create a geometry in which
small tables are below and big tables are above so
the system is really unstable, but physically it
should not fall down.>>Right.>>Or you can put
papers into an arch.>>Yeah.>>They were all using MCMC to generate these systems
in which you have some hard constrained in physics, from soft constraints and
you wonder what I did.>>I see.>>Like a furniture layout
which should not intersect, and it seems that you can take these and write them as Scenic programs.>>Yeah.>>That’s really pretty
interesting from a graphics point.>>Okay. Great. We’ve had that
in mind also because we are not the first people to propose PPLs for this scene generation problem, but we feel that our syntax is a lot more concise than what
other people have proposed.>>Yeah, that’s what
I am saying that. I think graphics people might
be very interested in this.>>Right.>>That is, by the way, in
probabilistic programming language has been designed for the graphics.>>Picture.>>Vision.>>Probably.>>Picture, that’s the one with MIT and which people
I think probably.>>Yeah, I think so.>>Because [inaudible].>>That’s yeah.
There’s another person whose thesis came out of MIT. I forget the name now but anyway, Richie, it’s right there.
Daniel Richie, number two. So the Kulkarni et al is is
the one that you mentioned. So there are a few that I’ve
already be happier to hit on this. But the main differences here is, so first of all, our emphasis is
on generation, not inference. A lot of the PPLs for graphics actually even those were
on scene understanding, in vision scene understanding. So that was more on the inference
size as opposed to generation. The second is the domain specificity. So they use PPLs that are quite general and Scenic is not
even Turing-complete. So there’s a big gap and we
restrict Scenic in certain ways that makes sampling
much more efficient. There’s also work that is
not programming language based on generating data. The main differences with
Scenic is that having a program gives you a lot more control and it’s
also more interpretable. So let me walk you through, I’m probably overtime
but I hope I can go another 15 minutes and tell
you a bit more about Scenic. So consider the example of
a badly parked car and I’ll just walk you through the creation of
a Scenic program to model this. So what you’re seeing
on the left there is, so you have this is schematic, so the triangles correspond
to the objects and the pointy end of the triangle is showing which way
the object is facing. So on the left, you see this
triangle that’s facing this way. That’s what we call the ego object, that’s the object
from whose viewpoint you’re going to construct the scene. That’s going to be a car
at this intersection. So what we are, the first line
is basically saying from the Grand Theft Auto library that
we have interfaced to Scenic, we’re going to import
the notion of a car, a cab, and road direction. So the point of Scenic is not really
about autonomous cars per se. So if you interface it to a library,
a renderer that can do that, then you can use it
for that application. Then next, what you
say is the ego object is going to be a car itself. So if that car moves,
then the viewpoint moves, and then you’re going to say, well, look at this, a curb
region that’s visible, that’s in the view
con from that object and pick a point with
an orientation on that. So let’s zoom into that. So what’s happening there is
you look at the what’s visible, and then you look at the curb region, which is the part outlined in black and then you
pick a point on that. The point has an orientation which
is along the road direction. Let’s call that spot. Now, when I say, pick
a point on the curb. Implicitly, you’re picking a point uniformly at random
from the curb region. So even though there’s no use of the word uniform or
normal line distributions yet, there are implicit distributions
with all these objects. So the variable spot itself
is a random variable. Then you pick a bad angle to park the car at and so that’s going to, in this case is defined as
between 10 and 20 degrees, either left or right,
that’s 1 minus 1. Here, we are saying it has
to be uniformly at random. Then what you do is you place a car left of that spot offset by vector, this is the small
talk vector notation, so it’s 0.5 meters that
way and then it faces the bad angle relative
to the road direction. Now, in Scenic, every object has
its own local coordinate system. So this is why we need things like specifying that it’s
relative to something else. So that’s the Scenic program
for the badly parked car. The first is just importing these objects and then
the rest of it is the code. Then once we do that and we connect
it to the GTA-based generator, you get a sequence
of images like this. What’s happening is that
the other attributes of the scene like the model
of the car, time of day, and so on just being sampled
uniformly at random. Now, from a language perspective
what is new in Scenic, one of the main things that’s new
is this notion of specifiers. So I mean notion of
specify itself is not new, but the way in which we’re using its application is new
for scene generation. So we have these things
that are highlighted in yellow which is one object
facing towards something or a car at a location. These are really think of them
as ways to programmatically express geometric
dependencies between objects. We have nine possible
specifiers and they’re all written in a way that is
close to natural language. Then, one of the key points
actually this is something that Sriram helped us understand
when he visited Berkeley. So what we did is we designed
Scenic to be something, a language in which we can
write on dependencies in a very natural way,
dependency between objects. So what this translates
to is in the backend when you have random variables that
model the different objects, you have the dependencies between those random variables expressed
very naturally captured, and then when you do sampling, you use the dependency structure
to do that efficiently. Then you have things like this
relative to road directions. So you can think of that as
a function that tells you how to sample or produce the angle
in this particular case. So the domain specific
sampling techniques really correspond to ways in
which you can prune the space from which you’re
going to sample from. One of the ways we do
this is by you can think about the geometric regions
from which you want to sample and we basically dilate or change those regions in order
to prune away infeasible parts. So for instance, a concrete example
is here’s a map of the road network in the Berkeley
area and what we wanted is to be able to generate
a scene where there’s a ego car and then there’s a taxi and the distance to the taxi
is less than five meters and the relative heading of the taxi. So the angle between the
orientation of the taxi and orientation of
the ego vehicle should be between 15 degrees and 45 degrees. That’s a funny angle
for cars to be oriented if they are on the same road. But it’s possible if they
are at an intersection and one car is going that way and
the other car is going this way. So what you see here is that
we are able to automatically, in this road network, mark
these green regions which are all the things where places
where we can sample from. Then prune away all the red stuff which are parts of the road network where we don’t have to sample from. You can greatly reduce the space
for the backend sample. This is one example of the domain specific sampling techniques
that we can do. So very quick summary of
the applications of Scenic. So one application I
haven’t talked about yet is just to explore
road design space exploration. You can use this not just in
the autonomous driving application, but in fact, one of the other things
we looked at is in robotics, like if you have
this Mars rover that has to navigate to a location
which is marked by the flag, it can climb over rocks but
it can’t climb over pipes. So now you want to be able to generate test cases that are
really challenging for the rover. They can be things like this where there’s two pipes blocking the path, and there’s only a very narrow gap
which has a rock in it, and it has to climb over
the rock to get past, right? You can write a Scenic program, very short Scenic program
that generates a lot of these challenging things, and you can explore
how the system works. I already talked about this one. We can also apply Scenic to
generate better training data. In particular, training on cases that are hard for the neural network. For instance, for the same neural
network that had this issue, we found that it was not
able to detect cases where one car is blocking
another partially, it was missing the car in the back, occlusions is a challenging thing. What we did is we used a Scenic
program to generate more data and use that to augment
the training set by adding a small amount of
synthetically generated images, and we improved the precision
significantly on the hard case and we didn’t lose precision
on the original case. All right. Now, I want to conclude. That’s a very quick overview
of the work on Scenic. In conclusion, I think this idea of algorithmic improvisation
has really developed into a very interesting
setup direction over the last four years
since I last spoke about it. There’s lots of applications
that you see here. I think in particular, probably
during my own interests, we’ve been looking more at the
applications to safe autonomy, but I think there’s
applications much beyond that, like what Raul mentioned in graphics. More generally, I think
this is a new class of randomized formal methods
that I think can be quite useful in the design and verification of
various kinds of systems. Okay, what’s next? I think there’s a lot
more to explore in the theory of algorithmic
improvisation and maybe we just have scratched
the surface in terms of algorithms and complexity there, and I think there’s use this for data generation for
a variety of applications. Modeling dynamic agents, I think, is a very interesting application. This is something that
Sriram also talked about, and the current use of Scenic. We’ve used it in that context, but we think we need to improve
the language for that use case. One of the places where this need to model
dynamic agents comes up is in verifying Machine Learning
or AI-based systems, that is, especially autonomous
systems and we recently put together a toolkit that
appeared at the CAF Conference that we call the Verified
AI or Verify toolkit, and I want to give you a sense
of that and then show you a use case of Scenic in that case. So this toolkit, by the way, it’s open source, Python-based
and what you can do with it, if let’s focus on
the right-hand side, you can do what’s called falsification
which is property guided. So formal specification
guided bug finding. You can do fuzz testing, you can generate
counterexamples and then do some analysis on the counterexamples. Then you can do data augmentation
which is you take the output like counterexample that you generated and then use that to augment your dataset and
retrain your ML competence. You can also do synthesis
of hyper-parameters and model parameters
in your ML models. But you can do that in
a property guided way. So you can say, I want to synthesize
my hyper-parameters so that after training the resulting model in the system will
satisfy a property. [inaudible]. It’s a long thing
I said but the idea is you’re using a formal
specification to guide the synthesis. Now to use it, what you’d need is, this toolkit is based on simulation. So what you need is you
want to feed your modeling, in this case, I’m talking about CPS, you want to model the controller, the model of the objects, the plan, what is
called the plan model. Then the conception components
like the neural networks. So that’s the system description, you want to model
the environment, for example, in a Scenic program, and then you
want to specify the property, and then you can use
these different use cases. So an example of what
we did with this is to analyze the behavior of an autonomous vehicle that
is supposed to navigate around a stalled car or
some construction site. So what’s happening here, is that the maroon car down there is an autonomous vehicle, and initially, it’s doing lane-keeping and
the way it’s doing lane-keeping is using standard edge
detection on the lanes, so no Machine Learning there but
it’s a bit classic AI algorithm. Then it also has a camera that
feeds to a neural network that is looking out for these stall sites that are marked by orange cones. So if it detects one of those, it st-is to estimate
the distance to that site, and if the distance
is below a threshold, it executes a lane change
and tries to go around this. So there’s two things going
on, there’s lane-keeping and then there’s at some point,
neural network says, “Oh, there’s something in front, and you have to navigate around it”, and then it does a lane change. That’s the situation here. On the left is the Scenic
program that we wrote. In the Scenic program,
what we are trying to specify is what the
environment looks like. So where is the blockage site, right? It’s near a curb and it’s
a point with an orientation, and then where are the cones, and where is the disabled car, and what’s the angle
of the disabled car? So that’s the thing that’s
being specified there. Okay. We can also specify
if you’re talking about other environment objects and they have associated
velocities and so on. You can specify those as well, but I don’t have it in this example. Once you have that Scenic program, then we can generate lots and lots of initial
conditions for simulation. So you can think about this as
the analog of fuzz testing. So you’re seeing that
visualized here. It’s generating lots of cases
where there’s a stalled car, there’s cones around
the car, and then the red vehicle is
some distance away. It varies the position, it varies
the model, colors and so on. What you’re seeing at
the bottom is the camera view from the autonomous
vehicle. All right. Now, I’m going to show you next the application of
falsification, okay? Let me just pause this for a second and explain what
you’re going to see. So what you’re seeing is the visualization of
the falsification algorithm. The falsification algorithm
is an iterative algorithm. It starts out with
the correct behavior and then it tries to direct the search
towards unsafe behaviors. So it’s basically an iterative loop where the first simulation
you will see is just fine, and then iteratively, will show simulations that go
towards collisions. So initially it starts
over lane keeping, it detects the car,
it goes around it, everything seems to be fine, right? Now you’ll see the color of
the stalled car changes, the positions change, locations
of the cones changed, etc. There was the first crash
where it just grazed the rightmost cone
and now iteratively, it finds more and more
egregious crashes getting closer and closer to the car. So that’s what the falsification
capability is doing. So what Scenic does in
this whole setting is, it provides you a way
to randomly explore those configurations that you
want to run the simulator in. This last one was
particularly interesting. So here what we found
was, automatically, what we found was a case where the environment car was
the same color as the cone. So what happened here was that the autonomous
vehicle’s neural network. Okay, let’s see it here. So if you see down here, the stalled car looks orange. What happened was the neural network had basically trained itself based on the color of the cone and
so it saw the orange car, it thought that it was a cone and it misestimated the distance
and it executed the lane change way before it should have but it ended up
being a bad lane change, and it hit the car anyway. So that’s the kind of
thing that you can do with a language like Scenic. You can basically use it to do this systematic
simulation-based testing of these kinds of systems. That’s all I had to say. Both Verify and Scenic are
open source and they’re available off of that GitHub
site and my web page, and I’m happy to take
any further questions, and happy to discuss more. Thank you.>>Thank you.>>Thank you.

Leave a Reply

Your email address will not be published. Required fields are marked *