论文标题
动态模型的神经屏障证书的自动合成和正式合成
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
论文作者
论文摘要
我们引入了一种自动化的，正式的，反例的方法，用于合成屏障证书（BC），以对连续和混合动力学模型进行安全验证。该方法的基础是电感框架的基础：该方法是在学习者之间作为一个顺序循环构造的，该学习者操纵候选人BC构成为神经网络，而声音验证者则可以证明候选人的有效性，或者生成反研究者以进一步指导学习者。我们将这种方法与多项式和非多项式动力学模型相比，将方法与最新的技术进行了比较：结果表明，我们可以更快地将声音BC综合到高达两个数量级，特别是在验证引擎上尤其是较小的较小的数据设置（较小的数据设置），以较小的数据设置（最多需要三个订单），以较小的学习（最多需要三个订单）。除了改进艺术状态外，我们还进一步挑战了混合动力学模型和更大维模型的新方法，并展示了我们算法和代码库的数值鲁棒性。
We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to five orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.
