EAGER: Real-Time: Formal Reinforcement Learning Methods for the Design of Safety-critical Autonomous Systems

EARLY概念探索性研究资助（EAGER）项目通过整合形式化方法和数据强化学习，采用全新的第一原理方法来设计安全关键型自主系统。最近几起涉及半自动驾驶汽车的备受瞩目的交通事故引发了人们的质疑，即目前以人工智能（AI）为中心的方法是否能让我们实现4级或5级自动驾驶，即，实现在所有驾驶场景中性能与人类驾驶员相当的全自动驾驶车辆。另一方面，基于形式化方法的验证和综合方法可以提供安全保证，但难以有效地推理数据驱动模型的不确定性和正确性。这个项目将结合联合收割机这两个看似不兼容的设计自主系统的范例。它将使用无模型强化学习算法来学习半自动驾驶汽车的驾驶数据。它将采用基于模型的方法进行系统设计、验证和综合，以在高度不确定的情况下提供可证明的安全操作。将建立一个AutoDrive测试平台，利用来自缩放车辆模型的人类驾驶数据，使用模仿和反向强化学习算法来推断安全控制策略。该研究与智能自主交通系统科学相关，具有重大的社会影响。该实验测试平台将用于为本科生和K-12推广工作提供实践研究经验，特别是，该项目将开发一个用于以信号时序逻辑表示的安全和性能规范的最佳控制合成框架。然后，它将车辆和行人的运动学通过概率计算树逻辑指定的非确定性/概率过渡模型。最后，它将通过从安全人类驾驶员的痕迹中学习，为受安全规范和复杂时间目标约束的部分观察到的动态模型开发正式的强化学习方法。该项目的一个关键技术贡献将是开发新的正式强化学习方法，该方法可能在广泛的应用中有用，其中我们必须通过从数据中学习来合成满足某些安全规范的最佳控制器。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

This EArly-Concept Grant for Exploratory Research (EAGER) project takes a clean-slate first-principles approach to the design of safety-critical autonomous systems by integrating formal methods and reinforcement learning from data. Several recent high-profile traffic incidents involving semi-autonomous vehicles have raised questions about whether current artificial intelligence (AI)-centered methods can ever lead us to Level 4 or 5 autonomy, i.e., to the realization of fully-autonomous vehicles with performance equivalent to a human driver in all driving scenarios. On the other hand, approaches rooted in formal methods for verification and synthesis can provide safety guarantees but have difficulty in efficiently reasoning about uncertainty and the correctness of data-driven models. This project will combine these two, seemingly incompatible, paradigms for designing autonomous systems. It will use model-free reinforcement learning algorithms to learn from semi-autonomous vehicle driving data. It will adopt model-based methods for system design, verification, and synthesis to offer provably safe operation in highly uncertain scenarios. An AutoDrive testbed will be set up where human driving data from scaled vehicular models will be leveraged to infer safe control policies using imitation and inverse reinforcement learning algorithms. The research is relevant to the science of intelligent autonomous transportation systems with significant societal implications. The experimental testbed will be used to provide hands-on research experience to undergraduate students and for K-12 outreach efforts.In particular, the project will develop a framework for optimal control synthesis for safety and performance specification expressed in signal temporal logic. It will then incorporate vehicular and pedestrian kinematics in non-deterministic/probabilistic transition models specified via probabilistic computation tree logic. Finally, it will develop formal reinforcement learning methods for partially observed dynamic models subject to safety specifications and complex temporal goals by learning from traces of safe human drivers. One key technical contribution of the project will be development of new formal reinforcement learning methods that may be useful in a broad array of applications wherein we must synthesize optimal controllers that satisfy certain safety specifications by learning from data.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.