Widespread adoption of autonomous cars will require greater confidence in their safety than is currently possible. Certified control is a new safety architecture whose goal is two-fold: to achieve a very high level of safety, and to provide a framework for justifiable confidence in that safety. The key idea is a runtime monitor that acts, along with sensor hardware and low-level control and actuators, as a small trusted base, ensuring the safety of the system as a whole.
Unfortunately, in current systems complex perception makes the verification even of a runtime monitor challenging. Unlike traditional runtime monitoring, therefore, a certified control monitor does not perform perception and analysis itself. Instead, the main controller assembles evidence that the proposed action is safe into a certificate that is then checked independently by the monitor. This exploits the classic gap between the costs of finding and checking. The controller is assigned the task of finding the certificate, and can thus use the most sophisticated algorithms available (including learning-enabled software); the monitor is assigned only the task of checking, and can thus run quickly and be smaller and formally verifiable.
This paper explains the key ideas of certified control and illustrates them with a certificate for LiDAR data and its formal verification. It shows how the architecture dramatically reduces the amount of code to be verified, providing an end-to-end safety analysis that would likely not be achievable in a traditional architecture.
Barrier-Certified Adaptive Reinforcement Learning with Applications to Brushbot Navigation
School of Electrical Engineering, Royal Institute of Technology（皇家理工学院电气工程学院）；Georgia Institute of Technology（佐治亚理工学院）；RIKEN Center for Advanced Intelligence Project（日本理化学研究所高级智能研究中心）；School of Mechanical Engineering（机械工程学院）
University of Edinburgh（爱丁堡大学）；Five AI Ltd.（Five AI有限公司）
It is important for autonomous vehicles to have the ability to infer the goals of other vehicles (goal recognition), in order to safely interact with other vehicles and predict their future trajectories. This is a difficult problem, especially in urban environments with interactions between many vehicles. Goal recognition methods must be fast to run in real time and make accurate inferences. As autonomous driving is safety-critical, it is important to have methods which are human interpretable and for which safety can be formally verified. Existing goal recognition methods for autonomous vehic…
Department of Aeronautics and Astronautics（航空航天系）；Massachusetts Institute of Technology（麻省理工学院）
Deep Neural Network-based systems are now the state-of-the-art in many robotics tasks, but their application in safety-critical domains remains dangerous without formal guarantees on network robustness. Small perturbations to sensor inputs (from noise or adversarial examples) are often enough to change network-based decisions, which was already shown to cause an autonomous vehicle to swerve into oncoming traffic. In light of these dangers, numerous algorithms have been developed as defensive mechanisms from these adversarial inputs, some of which provide formal robustness guarantees or certifi…
CSymPlan: Certified Symbolic Planning and Control for High-DOF Manipulators
Mohamed bin Zayed University of Artificial Intelligence (MBZUAI)（穆罕默德·本·扎耶德人工智能大学（MBZUAI））；Technical University of Munich（慕尼黑工业大学）；Ludwig Maximilian University of Munich（慕尼黑大学）；New York University Abu Dhabi（纽约大学阿布扎比分校）
