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

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

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.