Diana Spears on the safety of adaptive agents

Luke Muehlhauser: In Spears (2006) and other publications, you’ve discussed the challenge of ensuring the safety of adaptive (learning) agents:

a designer cannot possibly foresee all circumstances that will be encountered by the agent. Therefore, in addition to supplying an agent with a plan, it is essential to also enable the agent to learn and modify its plan to adapt to unforeseen circumstances. The introduction of learning, however, often makes the agent’s behavior significantly harder to predict. The goal of this research is to verify the behavior of adaptive agents. In particular, our objective is to develop efficient methods for determining whether the behavior of learning agents remains within the bounds of prespecified constraints… after learning…

…Our results include proofs that… with respect to important classes of properties… if the [safety] property holds for the agent’s plan prior to learning, then it is guaranteed to still hold after learning. If an agent uses these “safe” learning operators, it will be guaranteed to preserve the properties with no reverification required. This is the best one could hope for in an online situation where rapid response time is critical. For other learning operators and property classes our a priori results are negative. However, for these cases we have developed incremental reverification algorithms that can save time over total reverification from scratch.

What do you mean by “incremental” reverification algorithms, as in the last sentence I quoted?

Diana Spears: Verification (model checking, in particular) consists of proving that a computer program satisfies a desirable property/constraint and, if it does not, a counterexample is provided. In my work, I assume that this program is a (multi)agent plan for action.  In most real-world applications, plans are typically enormous and therefore verification may be quite time-consuming. Suppose the safety property/constraint that agent A must always obey is that “agent A should always be at least M units away from agent B” (to prevent collisions). Let’s assume that initial verification proved that the entire plan (consisting of all action sequences that agent A could ever possibly take) is guaranteed to obey this property in all circumstances. Furthermore, let’s assume that adaptation is required after the agent has been fielded, where adaptation consists of applying a machine learning operator to modify the plan. For example, suppose a specific part of the plan states that agent A should “move from location 3 to location 4 if there is a clear path between 3 and 4, the ground is fairly level (e.g., nowhere higher than X or lower than Y between locations 3 and 4), and if the schedule permits such movement at this time.” Then an example machine learning operator might change the “4” to “6” based on new information about the task being performed.

Note that this learning operator only modifies one condition in one miniscule portion of the entire plan.Therefore, why re-verify that the entire plan still satisfies the desired property after learning? Why not re-verify only the specific portion of the plan that was modified, as well as any parts of the plan that depend on the modified portion?  That is what “incremental re-verification” does. It localizes post-adaptation verification to only those parts of the plan that are essential to re-verify.  In doing so, it improves the time complexity of re-verification. Time complexity is a very important and practical consideration for online systems – especially those that operate in real-time or in time-critical situations. In my research I ran numerous experiments comparing the CPU time of re-verifying an entire plan versus localized incremental re-verification of the plan after learning. My results showed as much as a 1/2-billion-fold speedup using incremental re-verification! And that’s using a plan that’s tiny compared to what agents would typically use in the real world.

Luke: With what kinds of agent programs have you explored this issue? What do the agents do, in what environment, and what kinds of safety properties do you prove about them?

Diana: Because of the strong relevance of the topic “safe adaptation” to aerospace applications, I chose to focus on NASA-related (multi-)agent programs. I depict a scenario in which a spacecraft has landed on another planet, such as Mars, and from which multiple mobile rovers emerge. The plans (programs) for the spacecraft  lander, as well as the planetary rovers, are for collecting, retrieving and transmitting/delivering data and/or samples from the surface of the planet. I prove “safety” and “liveness” properties. An example of “safety” is, “It is always the case that agent R is not delivering at the same time that agent L is transmitting.” Here, L is the lander and R is one of the rovers. This property/constraint prevents problems that may arise from the lander simultaneously receiving new data from R while transmitting older data to Earth. An example of “liveness” is, “If agent R executes the ‘deliver’ action, then eventually agent L will execute the ‘receive’ action.”

Luke: Have you or anyone else built on this specific line of work since 2006? What are some natural “next steps” for this particular line of research?

Diana: There were essentially three main offshoots of my research that I’m aware of – from NASA Ames, SRI, and USC. I’ll start with the NASA Ames offshoot. Around the year 2000 I gave a talk about “Asimovian Adaptive Agents” at NASA Ames. My instincts about the strong relevance of this work to NASA, and more generally aerospace, proved to be correct. (Furthermore, it appears to be highly relevant to any automated transportation, including automated cars/highways.) The researchers at NASA Ames rapidly and eagerly followed up on my talk with a flurry of related work, including research and publications. These researchers focused on “reference models,” which are used for online, run-time I/O checking. Instead of using temporal logic properties to verify, they used control theoretic properties such as “stability” and “performance.” Perkins and Barto also used Lyapunov stability as the property of interest when building adaptive learning agents¹. For examples of the NASA Ames research and other related work, see the papers that appeared in the NIPS’04 workshop on “Verification, validation, and testing of learning systems”². Dietterich gave a follow-up talk at NIPS’06 on this topic³. The NASA Ames offshoot has continued to be active post-2006, as exemplified by the many recent contributing papers in Schumann’s 2010 book⁴. Furthermore, Vahram Stepanyan and others at NASA Ames have been working on a project called “Integrated Resilient Aircraft Control” (IRAC), whose goal is to validate multidisciplinary integrated aircraft control design tools and techniques that will enable safe flight despite unexpected adverse conditions⁵.

Shortly after my Ames talk, a second offshoot was initiated by John Rushby at SRI International. The SRI follow-on research continued to focus on formal methods with model checking, which is what I had originally worked with. However more recently this work has moved in a more similar direction to that of Ames⁶. For example, in this paper Rushby introduces the idea of using a “safety case” that leads to an online performance monitor. And even more recently, Ashish Tiwari at SRI has worked on bounded verification of adaptive neural networks in the context of the IRAC project⁷.

Next, consider a third offshoot. This is the research at the University of Southern California (USC) by Milind Tambe and others. These USC researchers built on my specific line of work, but they decided to address the important issue of mixed-initiative situations (also called “adjustable autonomy”), where humans and artificial agents collaborate to achieve a goal. Their multiagent plans are in the form of Partially Observable Markov Decision Processes (POMDPs) and they check safety constraints in this context. The first paper of theirs that I’m aware of on the topic of Asimovian adaptive (multi)agents appeared in 2006⁸. In 2007, Nathan Schurr got his Ph.D. on this topic⁹. Milind Tambe continues to teach a very popular courses on “Artificial Intelligence and Science Fiction” in which he discusses his research on Asimovian multiagents.

Finally, I’ll mention miscellaneous post-2006 research that continues to build on my earlier line of work. For one, during 2006-2008 I was part of a DARPA Integrated Learning initiative that focused on methods for airspace deconfliction. Two of my graduate students, Antons Rebguns and Derek Green, along with Geoffrey Levine (U of Illinois) and Ugur Kuter (U of Maryland), applied safety constraints to planners¹⁰. Their work was inspired by my earlier research on Asimovian agents. There are also researchers currently building on the NASA Ames work: an international group¹¹, Zhang and other researchers at Michigan State University¹², and Italian researchers who are building on Zhang’s work¹³. Also, Musliner and Pelican (Honeywell Labs), along with Goldman (SIFT, LLC) started building on my incremental re-verification work in particular – back in 2005¹⁴, and apparently Musliner is still doing verification and validation (V&V) of adaptive systems.

Now I’ll respond to your second question about natural “next steps” for this particular line of research. I believe that all of the research mentioned above is exciting and shows promise. But I want to particularly emphasize the NASA/SRI direction as potentially fruitful for the future. This is based on my personal experiences with machine learning, formal methods, V&V, and AI in general. I have always found that formal methods and other logic-based approaches are, for computational reasons, difficult to scale up to complex real-world problems. Over the course of my career, I have leaned more towards stochastic methods for machine learning, and run-time checking for V&V. Therefore I hope that the aerospace researchers will continue in the directions they have adopted. However I also believe that they should widen their horizons. There are numerous techniques currently available for runtime monitoring and checking, e.g., see the online software self-checking, self-testing, and self-correcting methods of Ronitt Rubinfeld¹⁵, or the run-time monitoring and checking of Insup Lee and Oleg Sokolsky¹⁶. I believe it would be potentially very fruitful to explore how many of the available monitoring and checking techniques are applicable to the behavioral assurance of adaptive systems.

But, most importantly, there is a topic that is critical to the future of building trustworthy adaptive systems and needs to be explored in great depth. That’s the issue of self-recovery/repair. Since around 1998-1999, my colleagues and I have been addressing self-repair in the context of swarm robotics¹⁷¹⁸. Our research focuses primarily on physics-based approaches to controlling swarm robotic formations – because physics naturally obeys the “principle of least action,” i.e., if a formation is disturbed then it will automatically perform the minimal actions required to repair the disturbance. This repair is locally optimal but is not necessarily globally optimal. In other words, we have dropped the requirement of global optimality, focusing on “satisficing” behavior instead.  Organic and natural physical systems are not perfect, but their lack of perfection often makes them more robust. There are systems where we need precise guarantees of behavior (e.g., the dynamic control of an airplane wing, to ensure that the plane does not stall and crash). But for other tasks, perfection and optimality are not even relevant (e.g., the Internet). We have demonstrated the feasibility of our research both in simulation and on real robots on numerous tasks, including uniform coverage, chain formations, surveillance, the movement of formations through environments with obstacles, and chemical source localization¹⁹. Hopefully other researchers will also explore physics-based systems. I believe that an excellent “safe adaptive (multi)agent” architecture would consist of a physics-based controller at the lower level, with a monitor/checker at a higher level to provide strict behavioral guarantees when needed. In particular, a more sophisticated version of our original design in [17] would be quite promising.

In summary, I sincerely hope that the above-mentioned research will continue in the fruitful directions it has already taken, and I also hope that students and researchers will pursue additional, novel research along these lines. It seems to me that the topic of “safe adaptation” is “low-hanging fruit.” DARPA²⁰ and other funding agencies have expressed to me their desire to fund research on this topic – because it must be satisfactorily addressed if we are to have deployable, adaptive systems that we can trust.

Luke: In the lines of work you outlined above, what kinds of AI-like functionality are included in the parts of the code that are actually verified? E.g. does the verified code include classical planning algorithms, modern planning algorithms, logical agent architectures, or perhaps even machine learning algorithms in some cases?

Diana: The code that gets verified consists of reactive, “anytime” plans, which are plans that get continually executed in response to internal and external environmental conditions. Each agent’s plan is a finite-state automaton (FSA), which consists of states and state-to-state transitions. Each state in the FSA corresponds to a subtask of the overall task (which is represented by the entire FSA). And each transition corresponds to an action taken by the agent. In general, there are multiple transitions exiting each state, corresponding to the choice of action taken by the agent. For example, consider the scenario I described in one of my previous answers in this interview, i.e., that of a planetary lander along with rovers. Two possible states for a planetary lander L might be “TRANSMITTING DATA” and “RECEIVING DATA.” Suppose the lander is in the former state. If it takes the action “PAUSE” then it will stay in its current state, but if it takes the action “TRANSMIT” then after this action has completed the lander will transition to the latter state.  Furthermore, the conditions for transitioning from one state to the next depend not only on what action the agent takes, but also on what’s going on in the environment, including what this agent observes the other agents (e.g., the rovers) doing. For this reason, I call the plans “reactive.”

Every FSA has an initial state, but no final state. The philosophy is that the agents are indefinitely reactive to environmental conditions subsequent to task initiation, and their task is continually ongoing. FSAs are internally represented as finite graphs, with vertices (nodes) corresponding to behavioral states and directed edges corresponding to state-to-state transitions.

Machine learning (ML) is applied to the FSA plans for the purposes of agent initialization and adaptation. Learning is done with evolutionary algorithms (EAs), using traditional generalization and specialization operators. These operators add, delete, move, or modify vertices and edges, as well as actions associated with the edges.  For example, suppose the lander’s transition from its “TRANSMITTING DATA” to its “RECEIVING DATA” state depends not only on its own “TRANSMIT” action, but it also requires that rover R1 successfully received the data transmitted by lander L before the lander can make this state-to-state transition in its FSA. This is a very reasonable requirement. Now suppose that R1’s communication apparatus has catastrophically failed. Then L will need to adapt its FSA by modifying the requirement of checking R1’s receipt of the transmission before it can transition to its “RECEIVING DATA” state. One possibility is that it replaces “R1” with “R2” in its FSA. Many other alternative learning operators are of course also possible, depending on the circumstances.

Machine learning is assumed to occur in two phases: offline then online. During the offline initialization phase, each agent starts with a randomly initialized population of candidate FSA plans, which is then evolved using evolutionary algorithms. The main loop of the EA consists of selecting parent plans from the population, applying ML operators to produce offspring, evaluating the fitness of the offspring, and then returning the offspring to the population if they are sufficiently “fit.” After evolving a good population of candidate plans, the agent then selects the “best” (according to its fitness criteria) plan from its population. Verification is then performed to this plan as well as repair, if required. During the online phase, the agents are fielded and plan execution is interleaved with learning (adaptation to environmental changes, such as agent hardware failures), re-verification, and plan repair as needed.

The main point of my “Asimovian adaptive agents” paper is that by knowing what adaptation was done by the agent, i.e., what machine learning operator was applied to the FSA, we can streamline the re-verification process enormously.

Luke: AI systems are becoming increasingly autonomous in operation: self-driving cars, robots that navigate disaster sites, HFT programs that trade stocks quickly enough to “flash crash” the market or nearly bankrupt a large equities trader, etc.

How might current AI safety methods (formal verification and reverification, program synthesis, simplex architectures, hybrid systems control, layered architectures, etc.) be extended to meet the safety challenges that will be raised by the future’s highly autonomous systems operating in unknown, continuous, dynamic environments? Do you think our capacity to make systems more autonomous and capable will outpace our capacity to achieve confident safety assurances for those systems?

Diana: My response to your first question is problem- and context-dependent. I know of many AI communities that are built around a single algorithm, and the researchers in those communities try to apply this algorithm to as many problems as possible. I believe that’s a misguided approach to research. Instead, I have always tried to adopt a problem-driven approach to research. The best way to scientifically solve a problem is to study it in great depth, and based on the a priori problem/task analysis select the most appropriate solution — including the planner or problem-solver, the properties/constraints to be verified, the adaptation method(s), etc. This will require a large suite of different AI safety/verification methods from which to choose. I cannot foresee the nature of this suite in advance; it’ll have to be constructed based on experience. As we tackle more complex autonomous systems, our repertoire of verification techniques will grow commensurately.

Your second question about whether autonomy will outpace safety is an extremely important one, Luke. Based on the applications you listed in your first paragraph, I see that your concerns extend to security. In fact, your security concerns also apply to “the internet of things,” which includes electronic, interconnected, remotely-accessible autonomous devices such as washing machines, ovens, and thermostats that will be installed in “smart homes” of the future. Businesses usually lack the motivation to install safety and security measures without some incentive. For example, leading software companies release beta versions of their programs with the expectation that the public will find and report the bugs. This is unacceptable as we transition to increasingly capable and potentially hazardous autonomous systems. I believe that the primary incentive will be government regulations. But we can’t wait until disasters arise before putting these regulations in place! Instead, we need to be proactive.

In 2008-2009 I was a member of a American Association for the Advancement of Artificial Intelligence (AAAI) Presidential Panel to study these issues. This was a fabulous panel, and it brought awareness to the AI community of researchers. Nevertheless it’s time raise awareness beyond the community of AI researchers. One suggestion I have is to assign a new or existing member of the United States President’s Council of Advisors on Science and Technology the task of studying and assessing the safety and security of autonomous systems.  This council member should consult the following people:

1. AI researchers who have extensive experience in developing autonomous systems
2. Engineers from aerospace, transportation, and other applications where safety is paramount
3. Lawyers and lawmakers who are cognizant of the legal issues that could arise
4. Cyber security experts.

I assume this council member would research the topic, consult others, conduct meetings, and conclude with a report and recommendations. Furthermore, I strongly believe that such a task should be assigned as soon as possible. We are already in a state where autonomy is outpacing safety and security, particularly in the commercial sector outside of the transportation industry.

Luke: Given that “autonomy is outpacing safety and security,” what are some other ideas you have for increasing the odds of reliably good outcomes from future autonomous systems?

By the way, I’ve only ever seen an “interim” report from that AAAI panel. Is there supposed to be a follow-up report at some point?

Diana: I haven’t heard about any follow-up or final report for the AAAI panel, unfortunately.

One idea is that we should have extensive safety and security testing prior to product release, based on established industry/government standards. We may not be able to enforce 100% compliance, but the presence of something like a “Safe and Secure Autonomous Product” certification could motivate consumers to favor purchasing tested and certified products over others lacking compliance. This would be like the existing UL product certification.

Another idea is to have monitoring, safety shutoff, self-recovery, and self-repair capabilities associated with autonomous devices. Furthermore, for security reasons these mechanisms should be decoupled from the autonomous system’s control, and they should also be detached from communications (e.g., not connected to the Internet) so as to avoid malicious tampering.

I don’t believe it’s possible to ensure complete safety and security at all times with autonomous systems. As you stated above, the best we can do is to increase “the odds of reliably good outcomes.” Nevertheless, I believe that substantial progress can be made if there is financial, technical, legal and programmatic support in this direction.

Luke: Thanks, Diana!

1. Perkins, T. and Barto, A. “Lyapunov design for safe reinforcement learning control.” Proceedings of AAAI’02. ↩
2. Margineantu, Schumann, Gupta, Drumheller, and Fresnedo (co-chairs). Workshop on “Verification, validation, and testing of learning systems.” NIPS’04.  ↩
3. Dietterich, T. “Research issues in deployed adaptive systems.” NIPS’06. ↩
4. Schumann, J. “Applications of Neural Networks in High Assurance Systems.” Springer-Verlag, 2010. ↩
5. Stepanyan, V. et al., “Stability and performance metrics for adaptive flight control.” AIAA’09. ↩
6. Rushby, J. “A safety-case approach for certifying adaptive systems.” AIAA’09. ↩
7. Tiwari, A. “Bounded verification of adaptive flight control systems.” AIAA’10. ↩
8. Schurr, N. et al. “Asimovian multiagents: Laws of robotics to teams of humans and agents.” 2006. ↩
9. Schurr, N. “Toward human-multiagent teams.” USC Ph.D. dissertation, 2007. ↩
10. Levine, G. et al. “Learning and verifying safety constraints for planners in a knowledge-impoverished system.” Computational Intelligence 28 (3), 2012. ↩
11. Tamura, G. et al. “Towards practical runtime verification and validation of self-adaptive software systems.” Self-Adaptive Systems, LNCS 7475, Springer-Verlag, 2013. ↩
12. Zhang et al. “Modular verification of dynamically adaptive systems.” AOSD’09. ↩
13. Sharifloo, A. and Spoletini, P. “LOVER: Light-weight formal verification of adaptive systems at run time.” Formal Aspects of Component Software. Lecture Notes in Computer Science Volume 7684, pp. 170-187, 2013. ↩
14. Musliner , D. et al. “Incremental verification for on-the-fly controller synthesis.” MoChArt’05. ↩
15. Rubinfeld, R. Checking. ↩
16. Sokolsky, O. Selected Recent Publications by Subject ↩
17. Gordon, D. et. al. “Distributed spatial control, global monitoring and steering of mobile physical agents.” ICIIS’99. ↩
18. Spears, W. and Spears, D. (Eds.) “Physicomimetics: Physics-Based Swarm Intelligence.” Springer-Verlag, 2012. ↩
19. Spears, W. and Spears, D. (Eds.) 2012. ↩
20. DARPA-sponsored ISAT meeting on “Trustable Deployed Adaptive Systems” at SRI, 2006. ↩