摘要

本文由斯坦福大学、耶路撒冷希伯来大学、哥本哈根信息技术大学、谷歌和GE航空研究等机构的专家共同撰写，探讨了深度强化学习（DRL）在航空航天控制系统中的应用及其安全性和可靠性问题。文章提出了一种新颖的设计-验证方法，通过k-归纳法和神经李亚普诺夫屏障证书来确保DRL控制器的正确性，并展示了这些方法在卫星控制模型中的应用。此外，文章还介绍了其他基于可达性的验证方法，并讨论了它们在实际应用中的局限性和潜在价值。

原理

文章提出的设计-验证方法的核心在于将验证过程融入到DRL训练过程中。具体来说，该方法通过修改训练循环使其更易于验证，并利用k-归纳法等正式验证技术来确保训练的正确性。神经李亚普诺夫屏障证书则是一种结合了李亚普诺夫函数和屏障函数的神经网络，能够在保证系统安全性的同时，确保系统最终达到目标状态。这些方法通过确保DRL系统在所有可能路径上的可达空间中不包含任何“坏”状态，并且始终保持在目标区域内，从而提供安全性和活性保证。

流程

文章首先定义了一个2D对接问题的基准问题，即训练一个DRL控制器来安全地将一个副航天器导航到主航天器。接着，介绍了使用k-归纳法来验证活性属性的方法，该方法通过找到一个排名函数（如航天器与目标的距离）来确保航天器最终会朝向目标移动。此外，文章还展示了如何使用神经李亚普诺夫屏障证书来生成不仅在大批量数据上表现良好，而且符合严格正确性标准的DRL代理。最后，文章描述了几种基于可达性的方法，这些方法虽然未能提供感兴趣的保证，但可能对其他DRL系统的验证有效。

应用

文章提出的方法不仅适用于航天器对接问题，还可以扩展到更复杂的控制系统和更广泛的航空航天应用中。随着技术的进一步发展和验证方法的改进，这些方法有望在确保系统安全性和可靠性的同时，推动DRL在航空航天领域的广泛应用。此外，这些研究成果也可能激发对神经网络验证、DRL安全及其在航空航天系统中作用的进一步研究。