>>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.