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.