SHF: Small: Formal Symbolic Reasoning of Deep Reinforcement Learning Systems

深度强化学习（Deep reinforcement learning）是人工智能的一种，已经普及，并被部署在自动驾驶汽车等决策系统中。然而，深度强化学习模型在训练过程和运行时性能方面都存在不稳定性。尽管在对人工智能安全性的担忧日益加剧的情况下，在提高公众信任方面取得了很大进展，但在严格保证安全关键系统中深度强化学习的安全性方面仍存在重大挑战。该项目将一系列符号推理任务——严格的抽象和验证——通过形式方法技术集成到强化学习中，以确保公众对此类系统的信任。该项目的影响是建立新的范例，并为可证明安全的深度强化学习奠定基础，从而能够在复杂的现实环境中做出值得信赖的决策。该项目的新颖之处在于，通过一个形式验证模块来增强强化学习的训练循环，该模块可以推断系统级安全属性。首先，该项目研究了构建强化学习代理和环境的形式化和可微分抽象的技术。通过使用优化技术减少安全属性和可微分抽象之间的损失，强化学习现在可以在训练时提供正确性的正式保证。其次，该项目开发了环境建模和监测算法，以在运行时捕获环境条件。强化学习代理可以安全地适应由形式验证保证的环境变化。此外，该项目通过将每个高维视觉输入编码为适合形式验证的符号表示，为基于视觉的深度强化学习系统提供了安全保证。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Deep reinforcement learning, a type of artificial intelligence, has become pervasive and is being deployed in decision-making systems such as autonomous vehicles. Deep reinforcement learning models are, however, subject to instability in both their training process and their run-time performance. Despite much progress in boosting public trust amid rising concerns about the safety of artificial intelligence, there remain significant challenges to rigorously guarantee the safety of deep reinforcement learning in safety-critical systems. This project integrates a range of symbolic reasoning tasks – rigorous abstraction and verification – enabled by formal-methods technology into reinforcement learning to secure the public's trust in such systems. The project's impact is to establish new paradigms and lay foundations for provably safe deep reinforcement learning that is capable of making trustworthy decisions in complex real-world environments.The project's novelty is to augment the training loop of reinforcement learning with a formal-verification module that reasons about system-level safety properties. First, the project investigates techniques to construct formal and differentiable abstractions of reinforcement-learning agents and environments. By reducing the loss between safety properties and differentiable abstractions using optimization techniques, reinforcement learning can now provide formal assurances of correctness at training time. Second, the project develops environment-modeling and -monitoring algorithms to capture environment conditions at run-time. Reinforcement-learning agents are safely adapted to environment changes guaranteed by formal verification. Moreover, this project provides safety guarantees for vision-based deep-reinforcement-learning systems by encoding each high-dimensional visual input into a symbolic representation that is suitable for formal verification.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.