arXiv:2410.15127v2 宣告类型: 替换-交叉 摘要：确保深度强化学习(DRL)的可验证和可解释的安全性对于其在实际应用中的部署至关重要。现有方法，如验证-在环训练，面临诸如部署难度大、训练效率低、缺乏可解释性以及在属性满足和奖励性能方面表现不佳等问题。在本文中，我们提出了一种名为Reintrainer的新颖的验证驱动的解释-在环框架，以开发可信赖的DRL模型，这些模型可以保证满足预期的约束属性。具体而言，在每次迭代中，该框架使用形式化验证来测量带内训练模型与预定义属性之间的差异，解释每个输入特征对模型输出的贡献，并根据即时测量结果生成训练策略，直到所有预定义属性得以证明。此外，现有验证器和解释器的低可重用性促使我们开发Reinfier，这是Reintrainer中的一个通用基础工具，用于DRL验证和解释。Reinfier具有断点搜索和验证驱动的解释功能，并与简洁的约束编码语言DRLP相关联。评估结果显示，Reintrainer在六个公共基准上的性能和属性保证方面均优于现有最新技术。我们的框架可以访问 https://github.com/Kurayuri/Reinfier。