Verifiable Autonomy

自主性无疑是21世纪世纪技术的核心主题。在20年内，我们预计将看到完全自动驾驶的车辆、飞机、机器人、设备、蜂群和软件，所有这些都将（而且必须）能够在没有人类直接干预的情况下做出自己的决定。经济影响是巨大的：例如，全球民用无人机（UAV）市场估计在未来10年内将达到60亿英镑，而机器人系统的全球市场预计到2025年将超过500亿美元。令人兴奋的是，这项技术可以让我们开发系统并解决远远超出当前可能性的任务。令人恐惧的是，这些系统的控制权现在从我们手中被夺走了。我们怎么知道他们会工作吗？我们怎么知道他们是安全的？我们怎么能相信他们呢？所有这些都是目前技术无法解决的问题。我们不能说这样的系统是安全的，不会故意伤害人类，总是尽最大努力保证人类的安全。如果没有这样的保证，这些新技术既不会被监管机构允许，也不会被公众接受。想象一下，我们有一个自治系统的通用架构，这样系统做出的选择就可以得到保证？这些保证都有强有力的数学证明吗？如果我们有这样一个架构，我们的自主系统（无论是机器人、车辆还是软件）都可以基于这个架构，那么我们确实可以保证我们的系统永远不会故意做出危险的行为，将努力做到安全，并将尽可能以道德和值得信赖的方式行事。重要的是要注意，这与系统如何准确地理解其环境的问题是分开的。由于对真实的世界建模的不准确性，我们不能说一个系统绝对安全或一定会实现某些目标;相反，我们可以说它试图做到安全，并决定尽最大努力执行任务。这一区别至关重要：我们只能证明这个制度从来没有决定做错事，我们不能保证永远不会发生意外。因此，我们还需要让一个自治系统判断其理解的质量，并要求它考虑到这一点采取行动。我们还应该通过我们的方法来验证系统的选择不会加剧任何潜在的安全问题。我们的假设是，通过识别和分离自治系统中的高层决策组件，并为此提供全面的形式化验证技术，我们确实可以直接解决安全、道德、合法性和可靠性问题。在这个项目中，我们建立在国际领先的工作代理验证（费舍尔），控制和学习（Veres），安全和道德（温菲尔德），和实用的自治系统（Veres，温菲尔德），以推进底层的验证技术，从而开发一个框架，使我们能够解决上述问题。在为复杂和未知的环境开发自主系统时，能够回答这些问题至关重要。

Autonomy is surely a core theme of technology in the 21st century. Within 20 years, we expect to see fully autonomous vehicles, aircraft, robots, devices, swarms, and software, all of which will (and must) be able to make their own decisions without direct human intervention. The economic implications are enormous: for example, the global civil unmanned air- vehicle (UAV) market has been estimated to be £6B over the next 10 years, while the world-wide market for robotic systems is expected to exceed $50B by 2025.This potential is both exciting and frightening. Exciting, in that this technology can allow us to develop systems and tackle tasks well beyond current possibilities. Frightening in that the control of these systems is now taken away from us. How do we know that they will work? How do we know that they are safe? And how can we trust them? All of these are impossible questions for current technology. We cannot say that such systems are safe, will not deliberately try to injure humans, and will always try their best to keep humans safe. Without such guarantees, these new technologies will neither be allowed by regulators nor accepted by the public.Imagine that we have a generic architecture for autonomous systems such that the choices the system makes can be guaranteed? And these guarantees are backed by strong mathematical proof? If we have such an architecture, upon which our autonomous systems (be they robots, vehicles, or software) can be based, then we can indeed guarantee that our systems never intentionally act dangerously, will endeavour to be safe, and will - as far as possible - act in an ethical and trustworthy way. It is important to note that this is separate from the problem of how accurately the system understands its environment. Due to inaccuracy in modelling the real world, we cannot say that a system will be absolutely safe or will definitely achieve something; instead we can say that it tries to be safe and decides to carry out a task to its best ability. This distinction is crucial: we can only prove that the system never decides to do the wrong thing, we cannot guarantee that accidents will never happen. Consequently, we also need to make an autonomous system judge the quality of its understanding and require it to act taking this into account. We should also verify, by our methods, that the system's choices do not exacerbate any potential safety problems.Our hypothesis is that by identifying and separating out the high-level decision-making component within autonomous systems, and providing comprehensive formal verification techniques for this, we can indeed directly tackle questions of safety, ethics, legality and reliability. In this project, we build on internationally leading work on agent verification (Fisher), control and learning (Veres), safety and ethics (Winfield), and practical autonomous systems (Veres, Winfield) to advance the underlying verification techniques and so develop a framework allowing us to tackle questions such as the above. In developing autonomous systems for complex and unknown environments, being able to answer such questions is crucial.