CAREER: A Framework for Logic-based Requirements to guide Safe Deep Learning for Autonomous Mobile Systems

人类驾驶的汽车等非自动驾驶系统被自动驾驶的无人驾驶汽车取代的未来已经触手可及。这种减少人类工作的代价是：在现有系统中，人类操作员通过他们的行动隐含地定义了高层次的系统目标;自治系统缺乏这种指导。 流行的自主设计技术，如基于深度强化学习的技术，从用户指定的、基于状态的奖励函数或用户提供的演示中获得指导。不幸的是，这样的技术通常不提供对训练的控制器的安全行为的保证。该项目主张采用一种不同的方法，其中使用时序逻辑表达的数学上明确的系统级行为规范来指导深度强化学习算法来训练基于神经网络的控制器。它允许推理的安全性，基于学习的控制，通过可扩展的方法，正式验证训练的控制器对给定的规格。 为了解决神经控制器缺乏可解释性的问题，该项目设计了新的技术，将神经网络控制的自治系统提取为人类可解释的符号自动机。该项目融合了统计学习、控制理论、优化和形式化方法，为自治系统的安全行为提供确定性或概率性保证。它通过可验证的强化学习的新研究生课程整合了教育和研究。 研究人员将通过向工业合作伙伴转让技术以及在顶级研究会议和期刊上发表文章，广泛传播该项目的科学成果。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The future where non-autonomous systems like human-driven cars are replaced by autonomous, driverless cars is now within reach. This reduction in human effort comes at a cost: in existing systems, human operators implicitly define high-level system objectives through their actions; autonomous systems lack this guidance. Popular design techniques for autonomy such as those based on deep reinforcement learning obtain such guidance from user-specified, state-based reward functions or user-provided demonstrations. Unfortunately, such techniques generally do not provide guarantees on the safe behavior of the trained controllers. This project argues for a different approach where mathematically unambiguous, system-level behavioral specifications expressed in temporal logic are used to guide deep reinforcement learning algorithms to train neural network-based controllers. It allows reasoning about the safety of learning-based control through scalable methods for formal verification of the trained controllers against the given specifications. To address lack of explainability of neural controllers, this project devises new techniques to distill the neural-network-controlled autonomous system into human-interpretable symbolic automata. The project blends methods from statistical learning, control theory, optimization, and formal methods to give deterministic or probabilistic guarantees on the safe behavior of autonomous systems. It integrates education and research through new graduate courses on verifiable reinforcement learning. The investigator will broadly disseminate the scientific outcomes of the project through technology transfer to industrial partners and through publications at top research conferences and journals. The expected societal impact is improved safety and explainable control for future autonomous cyber-physical systems in various application domains.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.