可认证鲁棒的神经Lyapunov-障碍证书的形式化综合

神经Lyapunov和障碍证书最近被用作验证深度强化学习（RL）控制器安全性和稳定性属性的强大工具。然而，现有方法仅在固定的理想无扰动动力学下提供保证，限制了它们在动力学可能因不确定性而偏离的现实世界应用中的可靠性。在这项工作中，我们研究了综合\emph{鲁棒神经Lyapunov障碍证书}的问题，该证书在系统动力学扰动下保持其保证。我们形式化定义了鲁棒Lyapunov障碍函数，并基于Lipschitz连续性指定了确保对有界扰动具有鲁棒性的充分条件。我们提出了实用的训练目标，通过对抗训练、Lipschitz邻域界和全局Lipschitz正则化来强制执行这些条件。我们在两个实际相关的环境（倒立摆和二维对接）中验证了我们的方法。前者是一个广泛研究的基准，后者是自主系统中的安全关键任务。我们表明，与基线相比，我们的方法显著提高了可认证的鲁棒性界（高达 $4.6$ 倍）和在强扰动下的经验成功率（高达 $2.4$ 倍）。我们的结果证明了在动力学扰动下训练用于安全RL的鲁棒神经证书的有效性。