Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an epsilon-approximate Hamilton-Jacobi Partial Differential Equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems.

翻译：近年来，利用深度学习计算连续时间动力系统可达集的方法相较于传统水平集方法日益受到青睐，因其克服了维数灾难问题。然而，与水平集方法类似，必须严格控制近似误差，尤其是在训练过程中无法保证所学可达集精度的现状下。为突破此局限，我们提出了一种ε近似Hamilton-Jacobi偏微分方程（HJ-PDE），该方程建立了训练损失与真实可达集精度之间的理论关联。为实现对该近似的形式化认证，我们借助可满足性模理论（SMT）求解器对HJ基损失函数在定义域内的残差误差进行严格界定。通过结合反例引导归纳合成（CEGIS）框架，我们构建了学习与验证的闭环系统：利用SMT求解器发现的反例对神经网络进行微调，从而持续提升所学可达集的精度。据我们所知，可认证近似可达性（CARe）是首个能为连续动力系统学习可达集提供可靠性保证的方法。