Medical Devices Speaker Series 2023: How Formal Specifications Can Be a Game Changer

I would like to invite our next speaker as Professor Deshmukh. He's an assistant Professor in the Department of Computer Science at USC, and also the co-director for the Center of Autonomy and AI. So Dr. Deshmukh, again, pleasure to have you here, and I'll pass it over to you right now.

Oh, sorry. I forgot to introduce the topic. So we'll be talking about formal specifications, a game changer for learning safe controllers and for Dr. Deshmukh, the floor is all yours.

Hi, everyone. Fascinating talks this morning. I've been busily taking notes, and I just realized, I'm not a co-directory, I'm a co-director. That's what happens when you make slides late in the night.

Well, let me start by-- this is kind of preaching to the choir, but what do you think is common in all these applications? You are, of course, going to say that, well, there is some in the loop, and there's some medical stuff that's happening, but from my perspective, what is interesting and common in all these applications is the following.

So if I look at a heart, I see that people have heart conditions. And, in fact, these heart conditions manifest in our EKG data, right? For example, I have waveforms indicating this-- I'm not a medical person, so I have no idea what this means, but there's a left bundle branch block or right bundle branch block, right?

In the middle on the top, I have waveforms of EEG data where there is some fuzzy stuff happening, which indicates that a person is having a seizure. In the bottom, this is something you have already seen in two wonderful talks today. There's a waveform indicating the blood glucose levels versus time, and if the blood glucose drops below a certain critical level, person could be facing hypoglycemia, which can be a life threatening condition.

And then we had this very interesting talk on spinal surgery. If you have been kind of talking to doctors and KEPT medical school up in USC, and we have some experts who use surgical robots to perform prostate surgeries, and for them, it's very important to make sure that you don't cause tissue trauma when you are doing the surgery because tissue trauma is correlated with longer stays in the hospital, right? And you don't want anyone to have that.

Again, one of the ways you could measure whether you are doing the wrong motions is by looking at the kinematic data of the robot that's doing the very high precision surgery. So what's common in all these applications? From my perspective, it's that there are all instances of careful reasoning with time series or temporal data that's needed.

OK, so again just to summarize, in my view, all these applications present are temporal data with safety-critical shape information. And I'm going to elaborate on what I mean by shifting from information in the rest of the talk, but the other thing that's common all these applications-- and again, I'm preaching to the choir here, but these are safety critical applications.

Real human lives and human health are at the receiving end of whatever technologies that we develop here, so it's very important that we get our stuff right. Otherwise, we have implications on people's lives. What we mean by shape information here is that desirable or undesirable behavior in the physiological signals, or robot motions, or neural signals, all of this information can be often expressed by some shape information or time series data.

So for example, if you look at blood glucose versus time, blood insulin levels versus time, if you look at the PQRS complex in an EKG waveform, if you look at spiking or oscillations in EEG data, if you look at unsafe kinematic motions of a robot, all of these indicate shape information in time.

And with this nugget in mind, what I'm going to try and talk to you about the rest of the time is how I think that formal specifications can really help us capture some of this shape information in a way that it provides us a mathematically unambiguous and machine checkable expression of safety.

I'm not going to kind of wave my hands and say, oh, the person is not hypoglycemic, right? I'm going to give you a very precise definition of what it means for somebody to be hypoglycemic as a function of something that they can evaluate on a specific time series data of their blood glucose versus time, or even the other conditions that I mentioned.

In some cases, we can use formal logics to give precise definitions of what those specific conditions mean. Of course, the logic and core desirable behaviors of physiological signals. I think what is-- I mean, my talk had this loaded word, right?

Game changer. I think why formal specifications can be game changers is because they provide you an ecosystem of tools for doing various things that you would want in the process of getting certification for your medical device, or for doing simulations, for doing internal tests, even for running clinical trials. |

And what does ecosystem of tools look like? You can do things like testing. You can do verification. And here, again, verification, I mean in a very formal sense, which means that for all possible things that can happen with the patient or in the environment, I'm going to always do the right thing, the safe thing.

Falsification, which is trying to see is there some specific condition in the environment that can cause the patient, for example, to become hypoglycemic, or it can cause the patient to have a cardiac arrest, right? You could design controllers using these specifications.

So if you are in the job of making these safety critical control systems for maybe an automated insulin delivery or for designing a pacemaker, you could use these formal specifications to guide the process of how you are designing the controller. If you are in the business of trying to certify these things, you can use formal specifications to do safety assurance.

One of the interesting new topics that we have been looking at is how can we assess risk using formal specifications? So once you make the design decision on this is the controller I want to go with, how risky is your controller? What is the chance that this-- hopefully it's a very small chance, but what is-- is there a level of risk that we can quantify? Formal specifications allow that.

If you are in the domain of doing surgeries and robot assisted surgeries, you can use formal specifications to evaluate how skillfully is the surgery being done? Again, very different thing, but formal specifications allow you to do that. They allow you to do modeling decisions, they allow you to automatically mine the specifications from the data that you have.

So there is a bunch of tools that we have been working on in my group and other groups around the world where we have been building this ecosystem of tools. And here, I would like to give a shout out to MathWorks because many of the tools that we have been working on, starting with some tools related to falsification, have been squarely rooted in the Matlab simulation environment.

I mean, of course now in the age of AI, we also have to kind of look at Python based tools, so we kind of use a mixture of both Matlab Simulink based tools as well as Python scripts, so depending on what flavor of research you do, we have tools available in either environment.

So in the rest of the talk, I'm going to talk about-- I don't know whether I'll have time to talk about the second formal logic, which is shape expressions. I'll just leave a picture on my last slide for you guys as an advertisement, but I'm primarily going to talk about a logic called signal temporal logic, which has been kind of the bread and butter theme in my research group.

I'm going to talk very briefly at a very high level about how we can use signal temporal logic to learn controllers, and finally, this is the stuff that I think you will find most exciting from a certification perspective is, how can we derive probabilistic guarantees or risk quantification using signal temporal right? And by the way, please feel free to interrupt at any time to ask questions.

All right, so what is signal temporal logic? Signal temporal logic is nothing but a very formal way of describing shapes on logical relations on signals. So here's a very simple signal temporal logic formula. It says that all ways between time 0 and 100, the value of the signal, x, remains between 1 and 3.

Now this is a very simple specification of bounds on the signal, x. You can make signal temporal logic formulas more expressive and interesting, right? So for those of you who have a controls background will immediately recognize what this formula is saying.

It's saying that eventually between time 20 and 60, there is some time, t, such that from that time onwards forever, the absolute value of the signal, x, remains less than 0.1. So this is saying nothing but the settling time of the signal is between 20 and 60, right? It can be at the best case 20 seconds, the worst is 60 seconds, right? The settling region is defined as this region of width 0.1.

You can also, in the medical devices domain, you can express some interesting STL properties. For example, not hypoglycemic is the property that always in the next 24 hours, the blood glucose is about 70 milligrams per right? Here's a more interesting property that uses nested temporal operators about not being hypoglycemic. And again, shout out to the great talk from Tandem where you had those pictures showing that you don't want people with diabetes to have the spikes in the blood glucose, right?

So how can you write that you shouldn't be hypoglycemic for more than one hour? You say that always for the 24 hour period, it should be true that whenever the blood glucose level exceeds 150 mg per-- and again, 150 is just a number. It can be anything you want, 170, 180. Then it's the case that when this even happens, within one hour, your blood glucose drops below that level, right? It says that I should not have these large spikes.

Again, for spike in EEG or other applications. Here is a signal temporal logic formula that says that there is a spike of height at least h and duration at least d.

This is kind of a longish formula to me, but basically, what it's saying is eventually there is a time when the value of the signal, x, goes below c, and within a short amount of time, it exceeds c plus h, and within d, duration, it goes below c again, so that kind of indicates the spiky shape. And here, again, I'm just trying to give you a flavor of the kind of expressions over physiological or other kind of time cd signals you can write using STL.

The thing that excites me the most about STL, of course that it's a logic, and the logician part of my training gets excited that I see logic, right? But very few people in the world are excited by logic unfortunately. That might be my experience, so what's cool about logic?

Of course, with logical expressions or logical formulas, you can say things like, do I satisfy this formula or do I not satisfy this formula? But what is cool about STL is it also allows you to say how well do I satisfy my formula? And essentially, what this logic has is what are known as quantitative semantics.

A quantitative semantic for logic-- semantics for a logic is a way of saying-- you can think of it as a signed distance. So it's a signed distance from the set of that satisfy a violated department. So here, I have a formula that says always between time 50 and 100, the value of the signal, x, should be less than 3.

On the picture to your left, I have a signal that's just terrible, right? It never satisfies this formula ever within the time range 50 to 100. Here, the signed distance is going to tell you how bad is the violation? How much inside the bad set does my signal go? The signal to the right actually does satisfy the formula, and here the signed distance is going to tell me how far am I from the set of bad places, or how far from the unsafe region?

So one way of thinking about quantitative semantics is that it gives you a degree of robustness with which a specification is satisfied. Positive values indicate satisfaction. Negative values indicate a violation. 0 indicates that the property is marginally satisfied or violated any way you want to define it. It's your choice, but 0 is not the number that you want to see.

And you can, again, whenever you're trying to evaluate any system, you run your STL monitor on your signal, and you're going to get a value. That value tells you by how much can I my signal and still satisfy my specification, or by how much can I the signal so that my signal now satisfies the specification in case it's violated?

So robust semantics of STL actually opened many doors, so if you want to do traditional control design, you can use this robustness value as a cost function. If you are doing property driven testing, you can use it as a heuristic to guide search. If you are doing things like reinforcement learning, which is a very popular AI-based method to design controllers nowadays, you can use it to design reward functions.

If you are doing adversarial or robotic testing, I mean, this is related the question I was asking earlier. What if my patient has a habit of chugging a chocolate Oreo shake right before they take their insulin bolus? That kind of represents a very adversarial scenario. I mean, some people just have a death wish, right?

So in this case, you can use it as, again, as a reward function, or constraints, or priorities. Some people that are-- there may be different specifications you want to check. You can enforce priorities between those classifications. You can use it as basically treating the robustness value as a random value that you're trying to-- random variable whose distribution you are trying to estimate.

You can use it to do risk quantification to get probabilistic guarantees, and one interesting thing is you can also use these specifications to generate monitors. So actually, every STL formula comes in built with a monitoring algorithm which you can just put on your device, and you can monitor various things at your own time, and there is some work we have done on this aspect as well.

So let me now briefly talk about some work we have been doing on learning controllers from formal specifications. So Lane provided a very nice way of modeling these systems, so I'm not going to go into a lot of detail on how you model dynamical systems, but in contrast of the traditional view of viewing everything as a differential or differential equation, I'm going to instead say that our dynamics are stochastic.

So given a state and some action that the controller may take, there is a probability distribution on what next state my system may go in, so those are going to be my dynamics at a very high level. And our controller itself is going to be some control policy that is dependent on the current state, and any parameters that want to design the controller are going to be abstracted away to this variable theta.

OK, so this is very much the machine learning way of modeling controller design. You can think of theta as being PID gains for your controller, or if you are designing-- if you are risky enough to design a neural network based controller, you can think of theta as encoding the weights and biases upon neural net.

Basically, think about any control algorithm you want to use. All the design decisions in that algorithm are going to be kind of pushed into theta, OK? And what we are trying to do is learn the values of theta that keep our overall system safe, so we can define the system trajectory as basically a sequence of states that we obtain by applying the control action at each step, and the control problem we can think of as trying to maximize the probability of being safe.

And I know that in the medical devices industry, you don't want to ever hear of the word probability because of course we want to always keep our patients safe, but really, what we are doing is maximizing the probability, right? I mean, there are going to be very low probability events where somebody decides to take an additional bolus of insulin right before they go exercising, and that can lead to catastrophic situations, right?

So I think the scientifically correct thing to say is all we can do is maximize the probability of being safe. In terms of the robustness guided control, we can think of it as maximizing the probability of being safe by at least some margin, and this is the problem that we are trying to solve.

Some of the challenges-- and again, big shoutout to Lane and someone-- Alex--

Alex.

Yeah, Alex, so for the talk. One of the big challenges is whenever we do control design, we usually assume we have some model that's kind of well behaved, right? In our setting, we have a model, but that model may be a very coarse approximation of reality.

So one way to look at it is, well, we have a model that's just unknown, and all we know is data about specific situations. So for example, each patient, or each organ, or each human phenomenon that we are trying to model is potentially unknown, and all we can do is try to learn from data.

The dependence on whether our particular system trajectory is safe on the control parameters in our algorithm could also be highly non-linear. So basically, what we are talking about here is we want to design controllers for a system where we don't know a model, or have a very vague idea of what the model looks like.

And if you want to set up an optimization problem that's highly non-linear, potentially time intensive to compute an optimal strategy that almost seems like I'm setting it up to be an impossible to solve problem, right? But again, thankfully, there are new techniques emerging from the AI machine learning domain which exactly try to address this situation where we are trying to design controls for highly uncertain systems.

So here, think about self-driving cars. I mean, it's not a great example given all the accidents that we keep hearing about in the news, but that's a good analogy. Like we are operating in a highly uncertain environment. What are the best effort guarantees that we can give, right? So highly nonlinear optimization, high uncertainty.

So one of the approaches-- and again, I'm not going to go into a whole lot of depth into the techniques. I just want to give you a flavor of the kind of approaches you have been looking at. So one approach we call neuro-symbolic controller synthesis-- so it has three main ideas.

Try to build a data driven model from the data that you see. So for example, if we have medical data of the patient on this action in this state led to this state, just build a neural network model, and then try to argue that this model is a good fit for the data.

The second step is to train a parameter controller to maximize the robust satisfaction, and then we have a few ways to make the problem slightly easier. So instead of having this highly nonlinear function to optimize, we try to make it smooth. We try to use stochastic gradient descent and other kind of black box optimization techniques.

And finally, the challenge is, how can we give deterministic or probabilistic guarantees on the synthesized system? And then, again, we have some techniques that are to formally reason about neural network based control systems, and I'll be happy to chat offline about what these techniques look like.

Here's another way, which is this brave new paradigm of model-free methods that is used in the modern work on the reinforcement learning. Here, again, the setting is you don't really have a model. All you have is access to a simulator, which is great because most of you seem to be building nice simulators, so your simulator allows you to query what's the next state given I'm in this state?

And using these model-free methods, you can try to learn controllers that maximize the probability of satisfying a given specification. So on the left, you have an of the very first paper that came out of this model-free and this, after some 730 iterations, is still kind of the card-- this is the classical card for control problem when you want to make sure that the pool stays balanced. What the system is doing is it keeps trying to jump off the table, OK? Even after 730 iterations.

And the picture of the on the right is something that we synthesized after about a 350 iterations of running the simulator, which looks quite stable. The difference is we used STL specifications to specify the desired behavior of the system, whereas on the left, they used this handcrafted kind of reward function.

Again, I'm happy to talk about this offline. We also have some results using-- for some diabetes applications using some RL based-- some simulators based on the model that people have done, and we have some preliminary results on this as well.

What I found interesting in our use of reinforcement learning is it also enables you to do robust testing, and here, the problem is how do you find whether your system violates that human specification? And this is what is known as the falsification problem, where you can model your environment, your patient, as an adversary, and try to model the spec that you want the system to satisfy using, for example, STL, and then you're trying to find what are adversarial inputs that lead the system to specification, right?

The issue here is the adversary can do anything. Finding bugs is like finding hay in a haystack, right? It's not like finding a needle in a haystack. Imagine the person who is just continuously insulin. I mean, if that's their adversary, they are going to be dead, right? In the simulation.

So what we want to do is we want to place reasonable constraints on what the adversary can do, and what's interesting is you can also express this constraints using STL. So we have some applications in the self-driving domain where we say that, well, we want the blue cars to merge in front of the red car, but if the blue car decides to just side on collide with the red car, there's nothing we can do, so we place some constraints on what the blue car can do.

And under those constraints is our red car meant to be safe, and we tried doing this adversarial testing approach for planners that people have developed, and we found that even under constraints on the blue car, the red car can still be unsafe. So these kind of results would be very interesting in the medical device domain where you say that, OK, I have a model that encodes what are typical things that the users do, and under these models, I'm safe.

If somebody does something that's a far departure from these models, then I can't really guarantee anything because my system only works conditioned on these assumptions. And in fact, one of the things I gave a shout out to Matlab that works is we have been looking to integrating the other Toolbox from to do some of this robust testing approaches for various models, including some from the medical devices domain.

All right, so in the last part of the talk, I want to go into some work we have been doing on statistical verification and risk estimation, and the main idea here is to model the system as basically a joint distribution between inputs and outputs. So you have inputs that come from some distribution, and these inputs could be initial states, exogenous disturbances, parameters, whatever, and it produces outputs over some distribution.

So the analysis question is, can we analyze this output distribution, right? And can we use this distribution to give probabilistic safety guarantees and to analyze this? So one of the ideas we have in doing this is a very exciting new method from the machine learning community called conformal inference.

The main idea is you have a bunch of data that you have gathered from your system trying to learn a surrogate model that predicts how the system is going to react, or what is the system behavior going to be in a previously unseen setup, OK? And for example, you could use your favorite regression method to kind of fit a model to your data.

Then you use conformal inference to what is known as-- to calculate what is known as a confidence interval. So basically, you have a training set with which you train your model. Then you use a calibration set to compute the 1 minus epsilon quantile of the empirical distribution of the error in prediction, OK?

And what the formal inference does is it tells you that once you compute the weight or the residual error of the 1 minus epsilon quantile, you can give the guarantee that's on the bottom line. It says that the probability that I'm safe-- that my safety score is between the predicted score plus minus c is going to be greater than 1 minus epsilon. So it kind of gives you a probabilistic guarantee on how unsafe I can be.

What's cool about conformal inference is it's not a very data hungry method. You can do this with very few samples compared to other methods to be probabilistic It's a versatile tool. You can use it to identify safe reasons in your control scheme.

So here, we had an F 16 control model, where, of course, we have ground collision avoidance. This kind of green red heatmap shows which regions are regions where the controller works safely, red regions are regions where the controller does not work safely. You can use conformal inference to do runtime monitoring and prediction, which is something we have also done using some neural network models.

And finally, you can use this robustness value of STL to do risk estimation, so you can compute the empirical distribution and compute risk measures that are used in the finance industry, such as value at risk or traditional value at risk. You can think of these risk measures as giving you some estimation of how risky is it to use controller.

Again, you can use a risk estimation with any kind of control theoretic method. What's cool about using STL specifications is now you are actually quantifying safety risk, not just an arbitrary control risk. I'll be happy to go into the details of these matters offline.

So to conclude, hopefully what I conveyed is that logical specifications can encode safety arguments or safety critical systems. We have an ecosystem of tools around specifications that can help with various tasks, and we would love to work with the medical devices industry to explore applications of our tools. Many of our tools are available in Python and Matlab code, so if you have interesting applications where you would like to try this, please feel free to send me an email.

Finally, a big thanks to my collaborators, my students on the left, and some of the faculty with whom I have collaborated on these topics, and I also want to leave a plot of what are shape expressions. I think this is a very cool idea which allows us to encode shape information in a less clunky way than STL.

I mean, my wife thinks that I'm not to her, but I also occasionally cheat with respect to formal logics, and that's the work we have been doing with shape expressions, where we try to express more interesting shape information in a less clunky way than STL. So I'll just leave that picture here. I'll be happy to check offline about this design. All right, thanks.