戴安娜长矛on the safety of adaptive agents

Luke Muehlhauser: InSpears (2006)和其他出版物，您讨论了确保适应性（学习）代理人安全的挑战：

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?

戴安娜长矛: 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.

请注意，该学习操作员仅在整个计划的一个微小部分中修改一个条件。因此，为什么在学习后重新验证整个计划仍然满足所需的财产呢？为什么不仅重新验证已修改的计划的特定部分以及依赖于修改部分的计划的任何部分？这就是“增量重新验证”的作用。它本地将适应后验证定位为仅重新验证的计划的那些部分。这样一来，它改善了重新验证的时间复杂性。对于在线系统，时间复杂性是非常重要且实用的考虑因素，尤其是那些在实时或至关重要的情况下运行的系统。金宝博官方在我的研究中金宝博娱乐，我进行了许多实验，比较了CPU在学习后重新验证整个计划与计划的局部增量重新验证的时间。我的结果显示了使用增量重新验证的速度高达1/2亿倍的速度！与代理商在现实世界中通常使用的计划相比，这是一个很小的计划。

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：由于该主题“安全适应”与航空航天应用具有很强的相关性，因此我选择着重于NASA相关的（多）代理程序。我描绘了一种场景，其中一个航天器已降落在另一个星球上，例如火星，并从中出现了多个移动流浪者。航天器着陆器以及行星漫游者的计划（程序）用于收集，检索和传输/传输/传递/或从地球表面的样品和/或样品。我证明了“安全”和“ Livices”属性。“安全性”的一个例子是，“始终是代理R在代理L传输的同时交付的情况。”在这里，L是Lander，R是流浪者之一。该属性/约束可以防止登录器同时接收新数据时可能引起的问题，同时将旧数据传输到地球。“ Livices”的一个例子是，“如果代理R执行“交付”诉讼，那么最终代理L将执行“接收”诉讼。”

Luke：自2006年以来，您或其他任何人都建立在这一特定工作之上吗？对于这一特定的研究，有哪些自然的“下一步”是什么？金宝博娱乐

Diana：我知道我的研究的三个主要分支 - 来自NASA AMES，SRI和USC。金宝博娱乐我将从NASA Ames分支开始。在2000年，我在NASA Ames发表了关于“ Asimovian自适应代理商”的演讲。我对这项工作与NASA的强烈相关性以及更普遍的航空航天的直觉被证明是正确的。（此外，它似乎与任何自动运输，包括自动化汽车/高速公路。）NASA Ames的研究人员迅速而热切地跟进了我与一系列相关工作（包括研究和出版物）的演讲。金宝博娱乐这些研究人员金宝博娱乐专注于“参考模型”，这些模型用于在线运行时I/O检查。他们没有使用时间逻辑属性来验证，而是使用控制理论属性，例如“稳定”和“性能”。珀金斯和巴托还使用Lyapunov稳定性作为感兴趣的财产¹。有关NASA AMES研究和其他相关工作的示例，请参阅NIP金宝博娱乐S’04在“学习系统验证，验证和测试”研讨会中出现的论文。金宝博官方²。Dietterich gave a follow-up talk at NIPS’06 on this topic³。NASA AMES分支在2006年后继续活跃，这是舒曼2010年的许多撰稿论文的例证⁴。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）继续教授关于“人工智能和科幻小说”的非常受欢迎的课程，他在其中讨论了他对阿西莫维亚多人的研究。金宝博娱乐

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¹¹，张和密歇根州立大学的其他研究人员金宝博娱乐¹²，以及基于张的工作的意大利研金宝博娱乐究人员¹³。另外，Musliner和Pelican（Honeywell Labs）以及Goldman（Sift，LLC）开始在我的增加的特别是重新验证工作 - 2005年¹⁴, and apparently Musliner is still doing verification and validation (V&V) of adaptive systems.

现在，我将回答有关此特定研究线的第二个关于自然“下一步”的问题。金宝博娱乐我相信上述所有研究都是令人兴奋的，并表现出了希望。金宝博娱乐但是我要特别强调NASA/SRI方向对未来有可能富有成果。这是基于我在机器学习，正式方法，V＆V和AI的个人经历的基础上。我一直发现，出于计算原因，正式的方法和其他基于逻辑的方法很难扩展到复杂的现实世界问题。在整个职业生涯中，我更倾向于用于机器学习的随机方法，并检查V＆V的运行时间。因此，我希望航空航天研究人员将继续朝着他们采用的方向发展。金宝博娱乐但是，我也相信他们应该扩大视野。目前有许多用于运行时监视和检查的技术¹⁵, or the run-time monitoring and checking of Insup Lee and Oleg Sokolsky¹⁶。我相信，探索多少可用的监控和检查技术适用于自适应系统的行为保证，这可能是非常有成果的。金宝博官方

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¹⁷¹⁸。我们的研金宝博娱乐究主要集中于基于物理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¹⁹。希望其他研究人员还将探索基于物理金宝博娱乐的系统。金宝博官方我认为，出色的“安全自适应（多）代理”体系结构将由较低级别的基于物理的控制器组成，并在更高层的层中使用监视器/检查器，以便在需要时提供严格的行为保证。特别是，我们在[[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²⁰其他资金机构也向我表示，他们希望为该主题提供研究的愿望 - 因为如果我们要拥有可以信任的可部署的自适应系统，则必须令人满意地解决。金宝博娱乐金宝博官方

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.

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，机器人navigate disaster sites,hftprograms that trade stocks quickly enough to “flash crash” the market or几乎破产大型股票交易者等

当前的AI安全方法如何（正式验证和恢复，程序合成，单纯形架构，混合系统控制，金宝博官方分层体系结构, 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：我对您的第一个问题的回答是问题和上下文依赖性的。我知道许多围绕单个算法建立的AI社区，这些社区的研究人员试图将该算法应用于尽可能多的问题。金宝博娱乐我相信这是一种误导研究的方法。金宝博娱乐相反，我一直试图采用问题驱动的方法进行研究。金宝博娱乐科学解决问题的最佳方法是深入研究它，并基于先验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.

卢克（Luke），关于自主权是否会超过安全空间的第二个问题。根据您在第一段中列出的应用程序，我看到您的担忧扩展到安全性。实际上，您的安全问题也适用于“物联网，”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.

在2008年至2009年，我成为美国人工智能促进协会（AAAI）总统小组研究这些问题。这是一个神话般的小组，它为AI研究人员社区带来了认识。金宝博娱乐然而，现在是时候提高AI研究人员社区的意识了。金宝博娱乐我有一个建议是分配新的或现有成员United 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研究人员金宝博官方
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已经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”报告从那个AAAI面板。是否应该在某个时候有一份后续报告？

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 product certification。

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

我不相信这是可能的,以确保完整的年代afety 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和Fresnedo（联合主席）。关于“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. “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。等。“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。等。“Learning and verifying safety constraints for planners in a knowledge-impoverished system.” Computational Intelligence 28 (3), 2012.↩
11. Tamura，G。等。“实现自适应软件系统的实际运行时验证和验证。金宝博官方” Self-Adaptive Systems, LNCS 7475, Springer-Verlag, 2013.↩
12. 张等。“动态自适应系统的模块化验证。金宝博官方” AOSD’09.↩
13. Sharifloo，A。和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。等。“即时控制器合成的增量验证。” MoChArt’05.↩
15. Rubinfeld, R.Checking。↩
16. Sokolsky, O.Selected Recent Publications by Subject↩
17. Gordon，D。al。“Distributed spatial control, global monitoring and steering of mobile physical agents.” ICIIS’99。↩
18. Spears, W. and Spears, D. (Eds.) “物理学：基于物理的群智能。” Springer-Verlag，2012年。↩
19. Spears, W. and Spears, D. (Eds.) 2012.↩
20. DARPA-sponsored ISAT meeting on “Trustable Deployed Adaptive Systems” at SRI, 2006.↩