Diana Spears on the safety of adaptive agents

卢克·穆尔豪瑟（Luke Muehlhauser）: InSpears (2006)and other publications, you’ve discussed the challenge of ensuring the safety of adaptive (learning) agents:

设计师不可能预见到代理商将遇到的所有情况。因此，除了为代理提供计划外，还必须使代理商能够学习和修改其计划以适应不可预见的情况。但是，学习的引入通常会使代理商的行为更加难以预测。这项研究的目的是验证自适应剂的行为亚博体育官网。特别是，我们的目标是开发有效的方法来确定学习剂的行为是否保持在预定约束的范围内……在学习之后……

…我们的结果包括……关于重要的财产类别的证据……如果[安全]财产在学习之前为代理商的计划保留，那么在学习后可以保证它仍然存在。如果代理使用这些“安全”的学习操作员，则可以保证不需要恢复资产即可保留属性。这是在迅速响应时间至关重要的在线情况下可以希望的最好的。对于其他学习运营商和财产类别，我们的先验结果为负。但是，在这些情况下，我们开发了增量的恢复算法，可以节省从头开始的总静止化时间。

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

Diana Spears：验证（尤其是模型检查）包括证明计算机程序满足理想的属性/约束，如果不提供反例。在我的工作中，我认为该程序是（多）行动计划。在大多数实际应用中，计划通常是巨大的，因此验证可能很耗时。假设必须始终服从代理A的安全性/约束是“代理A应该始终远离代理B的单位”（以防止碰撞）。假设最初的验证证明了整个计划（由代理A可能采取的所有动作序列组成）可以保证在所有情况下遵守该属性。此外，让我们假设在对代理进行派发后需要进行适应，在该适应器中包括应用机器学习操作员修改计划。例如，假设计划的特定部分指出，代理A应该“如果3和4之间有清晰的路径，则应从位置3移动到位置4，则地面是相当级别的（例如，没有任何地方高于x或低于y。在位置3和4）之间，如果时间表允许此时的运动。”然后，基于有关正在执行的任务的新信息，机器学习操作员可能会将“ 4”更改为“ 6”。

注意,这个学习算子只修改一个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:因为“强相关性的话题fe 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 toanyautomated 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在NIPS’06就此主题进行了后续演讲³。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 myincrementalre-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.

但是，最重要的是，有一个主题对于建立可信赖的自适应系统的未来至关重要，需要深入探索。亚博体育苹果app官方下载这就是自我恢复/维修的问题。自1998年至1999年以来，我和我的同事一直在群体机器人的背景下解决自我修复¹⁷¹⁸。我们的研亚博体育官网究主要集中于基于物理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.

机器学习是假定发生在两个阶段: 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.

我的“ Asimovian自适应代理商”论文的重点是，通过知道代理商所做的适应性，即将什么机器学习操作员应用于FSA，我们可以大量简化重新验证过程。

Luke：AI系统亚博体育苹果app官方下载在运行中变得越来越自主：self-driving cars，，，，robots thatnavigate disaster sites，，，，HFTprograms that trade stocks quickly enough to “flash crash” the market ornearly bankrupta large equities trader, etc.

How might current AI safety methods (formal verification and reverification, program synthesis, simplex architectures, hybrid systems control,分层体系结构，，，，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 thea prioriproblem/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 aAmerican Association for the Advancement of Artificial Intelligence (AAAI) Presidential Panelto 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 theUnited States President’s Council of Advisors on Science and Technologythe 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 arealreadyin a state where autonomy is outpacing safety and security, particularly in the commercial sector outside of the transportation industry.

Luke：鉴于“自主权超过了安全性和安全性”，您还为增加未来自治系统可靠良好结果的几率还有什么其他想法？亚博体育苹果app官方下载

顺便说一句，我只看过一个“临时”reportfrom 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 existingUL产品认证。

另一个想法是有监控,安全关闭，，，，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.

我不认为有可能在自主系统始终确保完全安全和安全性。亚博体育苹果app官方下载如上所述，我们能做的最好的是增加“可靠的好结果的几率”。尽管如此，我认为，如果在这个方向上有财务，技术，法律和程序化支持，可以取得实质性的进展。

Luke：谢谢，戴安娜！

1. 珀金斯（T.）和巴托（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. 舒曼，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. “一种用于认证自适应系统的安全案例方法。亚博体育苹果app官方下载” 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. “在知识破裂系统中，学习和验证计划者的安全限制。亚博体育苹果app官方下载” 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。和Spears，D。（编辑）”Physicomimetics: Physics-Based Swarm Intelligence.” Springer-Verlag, 2012.↩
19. Spears，W。和Spears，D。（编辑）2012。↩
20. DARPA-sponsored ISAT meeting on “Trustable Deployed Adaptive Systems” at SRI, 2006.↩