一种针对安全可达动态系统的形式化学习方法.pdf

书书书收稿日期：；修回日期：基金项目：国家自然科学基金资助项目（）作者简介：鲁腾飞（），男，浙江湖州人，硕士研究生，主要研究方向为深度学习、形式化方法；娄攀登（），男，浙江杭州人，系统分析师，研究生企业导师，主要研究方向为软件分析与验证；王胜朴（），内蒙古满洲里人，硕士研究生，主要研究方向为系统可靠性研究和形式化方法；丁觅（），湖北咸宁人，硕士研究生，主要研究方向为形式化方法、软件分析与验证；林望（），男（通信作者），浙江温州人，副教授，硕导，博士，主要研究方向为形式化方法、软件分析与验证、信息物理融合系统（）一种针对安全可达动态系统的形式化学习方法鲁腾飞，娄攀登，王胜朴，丁觅，林望（浙江理工大学 计算机科学与技术学院，杭州 ；浙江唐彩智能信息科技有限公司，杭州 ）摘要：在动态系统建模问题中，深度学习为建模提供了更便捷和灵活的方法，但其难以解释的特点降低了模型的可靠性。针对具有安全性和可达性的动态系统，提出了一种形式化模型学习方法，将安全性和可达性引入到对目标系统的学习过程中，使模型满足这两个性质。为保证所学系统在定义域上严格满足这两个性质，该方法基于现代控制理论中的 方法和 函数设计了可验证的 函数（），通过将其与动态系统联合学习，使得 能够为所学系统提供安全性和可达性保障。最后通过求解混合整数线性规划问题验证了模型确实满足相关性质，与 的对比实验展示了这一方法的有效性。关键词：形式化方法；动态系统学习；安全性；可达性中图分类号：文献标志码：文章编号：（）：，（，；，）：，（），：；引言信息物理系统广泛应用于工业控制、自动驾驶和航空航天等涉及社会运作和人身安全的关键基础设施，这类系统关乎人身、财产和环境安全，因此建立可靠的系统模型至关重要。在这一情形下，基于严格数学基础的形式化方法被应用于系统可靠性研究中 。如今深度学习方法为动态系统建模提供了新的途径，但其难以解释的特点导致模型的可靠性难以保证，比如在动态系统中常见的两种性质 安全性和可达性，在通过深度学习的方法对系统进行建模后这两个性质的证明变得十分困难。其中，安全性是指对于给定动态系统的初始状态，系统在随时间演化的过程中不会进入不安全状态集；系统的可达性是指对于给定系统的初始状态，系统随着时间的推移总能进入目标状态集。由于 函数可以将系统的状态空间分割成两个子集，常被用来证明系统的安全性。理论是刻画动力系统稳定性的方法，求出系统的 函数可以保证系统的稳定性。这类函数能够为系统提供某些性质的保障，因此也被称为证书。为了在建模的同时保证系统的某些性质，诸多领域从不同的角度为此做了大量的研究工作，目前已存在许多针对不同种类系统的建模方法，但如何在学习动态系统的同时为模型提供安全性和可达性的保障仍是悬而未决的问题。比如文献 ，通过将系统投影到一个隐空间来保证系统的稳定性，在该隐空间中 函数严格满足定义，但是这种方法给系统施加了过强的限制，牺牲了神经网络的灵活性，而且该方法没有考虑系统的安全性。等人 迭代地收集数据并更新系统的控制器，使用控制 函数以减少模型的不确定性，最终实现系统的安全行为，但是该方法没有考虑系统的可达性。最近，等人 在控制器合成任务中通过 （）使控制系统满足安全性和可达性，但是未对该控制器和系统进行验证，实际上该方法建立的系统在状态空间中有稀疏的状态点违背了安全性和可达性。目前，在动态系统的学习任务中，同时保证安全性和可达性的研究几乎处于空白状态。受到 等人 的启发，本文提出了一个基于数据驱动的学习方法 （），该方法通过联合学习非线性动态系统和 函数（），为系统的安全性和可达性提供保障。既要满足安第 卷第 期 年 月计 算 机 应 用 研 究 全条件也要满足可达条件。但由于神经网络的引入导致模型具有不可解释性，这使得人们难以分析其行为。为了给系统的安全性和可达性提供一个形式化的保证，有必要验证所学的系统以及 。为此将系统和 的验证问题转换为混合整数线性规划（，）问题，并通过数值求解器 对该问题求解，以确保 的有效性。最后，将 和深度强化学习中常用的 方法进行对比，实验表明，对系统的长远预测准确度明显优于 方法，而且 有效地约束了神经网络形式的动态系统模型。本文主要贡献如下：）提出了一个学习框架，该框架同时考虑了系统的安全性和可达性，并且使用 作为系统具有安全性和可达性的通用证书，而不是像多数研究将各个性质分开考虑，简化了证书的表达；）提出了一个验证框架，通过以 为激活函数的神经网络表示证书，并将神经网络的验证问题转换为 优化问题，使用优化求解器 编码和求解；）在一组基准样例中成功合成了 ，证明了算法框架的有效性。相关工作 动态系统建模不同场景下的动态系统各自具有不同特点，也不存在一种统一的方法能够为所有系统建立模型。线性系统相比其他系统更易于处理，因此如何学习稳定线性动态系统 ，较早地受到了关注，近来有更多学者着手研究稳定非线性系统的学习问题 。等人 较早地探索了深度学习和 分析的交叉点，文献 ，以联合学习方式学习动态系统和 函数，并且在学习过程中通过 函数投影方法来限制系统的稳定性，其优点是无须验证即可保证所学系统的稳定性，但是对系统的限制可能过强，无法发挥出神经网络的灵活性。等人 提出的学习方法针对单调稳定系统，该方法认为系统的某一状态不仅依赖于上一个状态，之前的 个状态都对当前状态有贡献，因而训练了 个神经网络并将其输出取凸组合。等人 实现了一个名为 的工具，对给定了常微分方程（）形式的动态系统，用反例制导的方法合成 和 函数，以证明系统的安全性和稳定性，反例由可满足性模理论（）求解器解得。动态系统在数学上通常用微分方程表示，一些研究工作聚焦于如何建立系统的微分方程，该方法已广泛用于时间序列预测和常微分方程估计 ，。等人 提出了一类名为 的新型神经网络，该模型训练时间明显增加，但是空间复杂度为（），发表后被给予很高期望。等人 考虑到物理系统的部分行为通常可由微分方程或方程组给出，提出了一种将这些先验知识融入 的方法。基于 的方法现已被应用到概率分布变换 和图像识别 ，中，这些方法都非常新颖，但是关于这些系统具体性质的研究较少报道。等人 提出了另一种用于学习连续系统的方法，使用插值技术将离散轨迹连续化，在学习连续系统的同时求出 函数以保证系统的稳定性，该方法把吸引域作为先验信息引入学习过程。上述方法针对的系统各有特点，但考虑系统稳定性的研究较多，安全性和可达性相对较少被考虑到，后两个性质的研究主要集中在控制领域。要保证这些性质在神经网络上成立，必须依赖形式化技术。形式化技术在学习控制任务中的应用基于严格数学基础的形式化方法已经被公认为验证系统是否具有安全性的有效方法，在工业领域中得到越来越广泛的应用 。在这一背景下，形式化方法被引入到深度学习领域以训练满足条件的神经网络。和 函数主要应用于控制领域，这类函数也被称为证书（），因为它们为控制器或系统的行为提供了某种保障。通过学习基于神经网络的 或 函数以及相应的控制策略，使系统满足相应性质，如 等人 用这种方法得到了安全和可达的控制器，但是没有进一步验证。等人 对问题做了简化，他们对给定的 函数求稳定控制器，但实际上 函数很难事先给出；等人 提出了安全控制器的合成方法，其安全性由 函数保证，但是该方法针对连续系统，由于连续系统 函数定义与离散系统有所不同，验证方法也不一样。等人 采用神经网络表示标称控制器和 ，求得满足要求的 后，通过解一个特定的优化问题得到安全和稳定的控制器。这项工作受到 的启发，通过联合学习动态系统和对应的 保证了系统的安全性和可达性。通过深度学习方法合成 函数或 函数需要进一步验证，这涉及到神经网络的可信性分析 。为解决这一问题，、输入精化（）、线性逼近 、等方法被引入到神经网络的形式化验证中。等人 用 评估神经网络的鲁棒性；后来 等人 用这一技术验证屏障证书，其原理是将 函数替换为一系列线性约束和二值约束，从而用 计算神经网络在给定输入区域上的最大或最小输出。文献 处理的系统是连续的，而在本项工作中合成的是离散系统，验证过程中的编码方式有较大差异。基础知识 动态系统及其性质原系统的具体数学形式往往是不可知的，主要考虑通过深度学习建立离散动态系统模型，训练数据是从初始区域出发的状态序列。首先，引入离散动态系统的差分方程表示方法：（）（）（）其中：?表示时间，?表示系统状态，（）：表示定义在?上的 连续函数。同时系统还需要满足可达性和安全性。定义 可达性。给定紧集?和紧集?，如果对于任意初始状态?，都存在?，使得?，则称该系统是可达的，分别称?和?为初始集和目标集。定义 安全性。给定紧集?和紧集?，且?，如果对于任意?和任意?都有?，则称该系统是安全的，分别称?和?为初始集和不安全集。综合考虑这两个性质，即系统状态从初始区域?出发，存在有限时间?，经过 步后系统状态必能进入目标区域?，而且这期间不会进入不安全区域?。形式上，将从 出发，经过 步演化后形成的状态序列记为，简记为 ：。对目标区域的可达性可由稳定性扩展得到 ，通过证明动态系统存在一个与之匹配的 函数以确保系统具有可达性，而系统的安全性则是通过找到系统的 函数来保证，这两个函数的使用和推广在控制领域已经得到广泛研究和应用 。基于这两个函数，以保证所学动态系统的安全性和可达性。定义 函数。若有函数 ：?，：，使得下述条件：（）?（）（）?（）（）?（）计 算 机 应 用 研 究 第 卷（）?（）（）（）?（）成立，则称 为离散动态系统 的 函数。如果上述 存在，则系统是安全且可达的，因为 确定的水平集?是该系统的一个前向不变集，初始区域被包含在该不变集中，而不安全区域与该不变集没有交集，从而使得从?出发的任意轨迹都不可能进入?。类似地，由 确定的水平集?也是该系统的一个前向不变集，该不变集正是目标区域?，从状态空间中任意状态出发的轨迹随系统演化必将进入?，并且在无限时间内都不会离开?。基于以上理论，如果能够在学习系统的同时学习相应的 ，则最终学到的系统将具有安全性和可达性保障。但是仅通过神经网络学习动态系统及其 仍然不够，因为由神经网络表示的 本身就缺乏可解释性，所以必须对网络进行验证。为便于后续验证过程的描述，下面给出神经网络的形式化表示方法。神经网络验证方法用 表示神经网络 的输入，和 表示第 个隐藏层的输出和激活函数，和 分别表示第 个隐藏层的系数和偏置，表示的网络的最后输出，则神经网络的运算过程 （）可以形式化地描述为 （），（）为了便于验证系统 及其 ，使用 作为激活函数，基于 的神经网络的验证问题可以转换为 问题。关于神经网络输出求最大或最小值的问题，涉及到将网络的前向传播过程转换为 问题的约束 ，记为 （，），其具体形式如下：，（），（）（）其中：（）表示第 个隐藏层的输入 的维度；向量 维度与 相同，其每个元素都是属于 ，的二值变量，用于表示 函数的分段性质；是一个边界常数，可以直接设置为一个足够大的值，如 。形式化模型学习方法 联合学习动态系统和 是基于数据驱动的学习方法。假设从原系统获得的 个状态序列为（）：，（）：表示第 个状态序列，定义数据集为 ，其中，是两个时间上相邻的状态按时间顺序组成的状态对，在训练时作为特征和标签，表示总的数据量。的训练数据通过对各个区域网格化采样获取。用形式化模型（）（）表示使用神经网络学得的系统，其中 是一个神经网络，表示网络参数，这一形式受到了残差网络 的启发，经验表明该形式有利于学习离散系统和提高神经网络的精度。学习离散动态系统是通过降低损失函数（式（）实现的。?（）（）（）其中：表示 （）概率分布律，在实践中可以使用均方误差：?（）（）（）（）通过式（）训练得到的模型还不能确保具有稳定性和安全性。是系统具有安全性和稳定性的充分条件，若能够学得离散动态系统的 则证明系统满足这两个性质。使用参数为 的神经网络（）（）来表示，隐藏层数记为。根据定义 给出各个条件，相应的损失函数分别为?（?（）（）?（?（）（）?（?（）（）?（?（）（）?（?（）（）（）其中：（）和 （）分别表示上确界和下确界。式（）作为损失函数意味着要求（）在?上的上确界小于，即在输入区域?上处处小于；式（）要求（）在?上的下确界大于，即在输入区域?上处处大于；式（）和（）与前两者类似。式（）要求 每一步都沿着 输出值下降的方向演化，故（）（）的最大值应小于 。如果损失函数?的值降到 ，就说明 符合 的定义，意味着 在?边界任意一点上都精确地等于，神经网络可以逼近这一效果，但不可避免地会存在误差。换言之，由于?和?互为补集，两个集合在?的边界上相切，基于神经网络的方法很难将这两个集合分割开。为此可以对前两个条件做松弛处理，即要求轨迹进入?的任一子集，该子集在训练过程中自适应地确定，因此可将定义 中的第一个条件替换为（）?（）其中：?，那么必定存在 （）关于 的水平集?，且?，故?可以作为定义 中目标集。这样做的原因是：）如果轨迹能够进入目标区域的子集，那么必定能进入目标集，即系统满足可达性；）当?和?两个集合不相切时，神经网络 能够轻易地将两者分开，而?作为定义 中的目标集能够自然地被学习到。于是?和?可以修改为?（?（）（）?（）（）（）实际训练过程中的数据是有限的，因此训练时使用如下形式的损失函数：?（）()）?（）()）?（）()）?（）()）?（）（）()）（）其中：?表示在集合?中的采样数目，后面四项是类似的。为一给定正常数，其值接近 。式（）中的 项分别与?一一对应。现在考虑同时训练网络 和，将它们的损失函数相加得到?。由于采样点是有限的，即使?在经过一段时间训练后数值降到 ，在没被采样的状态上?仍有可能大于 ，这意味着 并没有在整个状态空间中满足 的定义，系统的安全性和可达性没有在整个状态空间内得到保障，因此还需要对候选、进行验证。基于 的形式化验证只有当所学的 在整个状态空间上满足定义 中的条第 期鲁腾飞，等：一种针对安全可达动态系统的形式化学习方法件，才能说 是离散动态系统 的 函数。因此需要根据定义 的条件对候选、进行验证。在初始区域上，定义 要求 在这一区域的值处处小于，即?（）（）如果上述条件得到满足，就称条件式（）通过验证。又由于神经网络中除激活函数以外都是线性运算，基于 激活函数的神经网络结构可以转换成 问题：（，）?（）这一优化问题可以通过优化问题求解器 求解，若有 ，则约束条件式（）通过验证。不安全区域的验证与在初始区域方法类似，检查 在不安全区域?上的最小值是否大于，验证如下约束条件：?（）（）为判断这一约束条件，需求解下述 问题：（，）?（）由 编码并求解优化问题式（）得到最优解，若 则约束条件式（）通过验证。目标区域的验证同样可以转换为 问题，在输入区域?上的输出值处处小于，在 上的值处处大于，形式上需要满足约束条件式（）和（）。?（）（）?（）（）这两个约束的验证过程与初始区域和不安全区域的验证相似，转换为 问题后可以求得 在?上的最大值 和在?上的最小值，若有 和，则这两个条件通过验证。式（）经过松弛后要求系统在?上的每一步都沿着 值下降的方向演化，即系统在该区域上的单步差分的上确界小于 ，故需验证约束条件式（）。?（）（）（）验证约束条件式（）是通过求解 问题式（）实现的。（）（，）（，），（，），（）关于 的约束在式（）中出现了两次，前者 的输入直接来自集合?，该约束等同于计算（）；后者 的输入来自 的输出，等同于计算（）。在求解此优化问题后，若有 ，则约束条件式（）通过验证。系统 和候选 通过以上所有验证，就称 满足定义，是离散动态系统 的 函数。实验及应用 实验设置 通过联合学习动态系统及其 函数，得到了可验证的安全可达动态系统，其中动态系统和 均用神经网络表示，基于 框架实现，验证过程采用 编码和求解。与强化学习中的深度确定性策略梯度（，）算法 在两个案例上进行对比实验，结果表明了 的有效性。是强化学习领域中广泛使用的算法，该算法由 和 两部分组成，两者都由深度神经网络表示，用于评估 动作的好坏程度，为了更准确地获得动作价值函数和策略函数，这两者还分别引入了目标函数。在本实验中 的输入为当前状态，输出为下一个状态和当前状态的差值，因此动作和状态具有相同维度。实验分别为目标区域和安全区域设置正值和负值作为奖励，为了使 具有拟合效果，本文在样本轨迹上采样，并根据 的预测状态到真实状态的距离设置奖励，以鼓励 的行为向训练轨迹靠近。在下面的案例中，使用科学计算软件包 中的数值积分工具获得轨迹，这些轨迹从随机初始点出发，取 条轨迹作为训练集。两个案例中除了时间步长的设置有所不同，其他设置都是一致的，第一个案例中时间步长为 ，第二个案例的时间步长为 ，总步数都是 步。系统的网络 设置为两个隐藏层，每个隐藏层 个神经元，表示 的网络 同样设置两个隐藏层，每个隐藏层 个神经元。令 ，的值在训练过程中自动确定，这可以通过网络框架中的自动微分工具实现，设置 。本工具使用 优化算法，经验表明相比于 等算法，其损失下降过程更加稳定。当?损失值下降到 即训练阶段结束，为了保证训练得到的网络符合如前面所述的稳定性和安全性，还需要进行验证。验证过程调用求解器 解决混合整数线性规划问题，若产生反例，则将反例添加到训练集中继续训练，直到没有反例通过验证。在原始系统形式未知的前提下，通过给定原系统的轨迹作为动态系统的训练数据，并从原系统的各个区域采样以训练 。实验表明 能成功合成满足安全性和稳定性的动态系统。范德波尔振荡器范德波尔振荡器方程描述了真空管放大器的极限环振荡现象，在一定条件下是一个局部渐近稳定模型。该模型具有一个极限环，在极限环内是以原点为平衡点的吸引域，在极限环外部则是不稳定的，其形式为：（）通过对该方程数值积分获得训练轨迹。本案例中，各个区域的范围设置为：?：，?：?：（）（）?：?：（）（）?：?：?：?：对这些区域进行网格化采样以供 训练，根据已有的样本轨迹和训练集便可训练得到一个既满足安全性又满足可达性的系统，该系统从初始区域?出发的轨迹不会进入不安全区域，且最终能到达目标区域?。和 分别学习 振荡器模型并用于预测系统状态的演化，图 直观地展示了两种方法在五个随机初始状态上的预测结果。的预测轨迹如图 （）所示，这些预测轨迹趋于目标集，而且与真实轨迹几乎完全重合，表明 学习到的系统误差非常小，而且预测误差并不随时间增长，这得益于系统的稳定性。虽然在一定程度上模拟了系统演化过程中状态变化的趋势，其预测轨迹与真实轨迹呈现出相似的曲线特征，但是误差显著大于 方法，而计 算 机 应 用 研 究 第 卷且这些轨迹没有进入目标集。两种方法的均方误差（）对比如图 所示，的预测误差比 小了几个数量级。图 和 在 模型上的对比结果 图 展示了 训练得到的 ，该 已经通过 验证。图中标注为 的封闭区域将状态空间分割为两个不相交的集合，被曲线包围的区域即为 函数关于 的一个水平集，水平集内皆为安全状态。实际上该水平集刻画了系统的一个前向不变集，即由初始区域出发的轨迹不会离开该水平集，从而确保了系统的安全性。并且 还能够保证合法初始状态必定能够在有限时间内进入由 确定的水平集，该水平集被包含于目标区域，从而为可达性提供保证。图 与 的均方误差 图 等高线图 倒立摆倒立摆是一个经典的非线性控制问题，该问题包含两个状态、和控制输入 ，其中 表示角度，表示角速度。该控制系统可以用如下方程表示：其中：非线性控制函数 （），其他常数分别设置为 ，和 。各个区域的范围为：?：，?：?：，?：?：?：?：?：?：在这一案例中，?的物理意义是明确的，系统状态进入该范围可能导致杆件故障，不同的物理装置有不同的设定。目标区域?描述了系统状态演化的目标，即杆件最终能够向上直立达到平衡状态。给定初始区域的五个随机初始状态作为测试样本，应用 方法合成的系统预测结果如图 （）所示，可以看到预测轨迹和真实轨迹基本吻合，误差保持在 以内，表明 对非多项式系统的预测误差依然很小，这是因为 是基于数据驱动的，对于原始系统的数学形式并不敏感。图（）展示了 对系统的预测结果，虽然在一定程度上满足了系统的安全性，但是没有在测试时间内到达目标区域，而且对系统的动态行为预测表现不佳。一个可能的解释是，该系统从初始状态出发到达目标区域的过程中，部分状态沿着远离目标区域的方向演化，这对于 而言相当于是一个多目标优化问题，而降低预测误差和到达目标区域是两个相互矛盾的目标。另外，尽管从预测图像上看，对系统的预测满足安全性，但是由于无法提供形式化保证，在训练集之外的状态上仍有可能违反安全性。图 和 在倒立摆系统上的结果 图 展示了两种方法的均方误差，虽然 在非多项式系统上的长远预测结果较上一案例有所增加，但是在数值上仍显著小于 。两者的预测误差在 后基本维持不变，这主要得益于系统的稳定性。值得注意的是，训练过程的损失函数只考虑单步预测误差，但在最后的轨迹预测时作出 步预测，的误差在长期预测中不会显著增长，这主要得益于系统的稳定性。成功地为倒立摆系统合成了 函数，该函数是从二维状态空间到一维实数值的映射，其等高线图如图 所示。关于 的水平集是系统的前向不变集，初始集?被包含在该不变集中，因此从初始状态出发的轨迹不会离开不变集进入不安全区域，从而保障了系统的安全性。另外，系统状态将沿着 值递减的方向演化，最终进入关于 的水平集?，?被包含于目标集中，从而保证了系统的可达性。图 与 的均方误差 图 等高线图 结束语动态系统常常具有安全性和可达性，建模过程中应保证这些性质成立，但是当深度学习方法被应用到动态系统的建模中时，这两个性质便很难得到保障。为了解决这个问题，本文提出了 方法，该方法引入 函数（），并通过数据驱动的方式联合学习未知形式的动态系第 期鲁腾飞，等：一种针对安全可达动态系统的形式化学习方法统和 ，建立了可达且安全的系统模型。神经网络表示的 带来了新的形式化问题，为此将其转换为一组混合整数线性规划问题，通过优化问题求解器 编码和求解。应当指出，目前还只能为低维度系统建模，在高维度复杂问题上难以合成有效的 ，即在系统的状态空间中存在反例而不能通过验证，而且验证时长大大增加。在后续工作中，将进一步探究高维度系统的可信学习方法和算力更节约的验证方法。参考文献：王淑灵，詹博华，盛欢欢，等可信系统性质的分类和形式化研究综述 软件学报，（）：（，（）：），：，：，：，：，：，：，（）：，：，：，（）：，：，：，：，：，（）：，：，（）：，：，：，：，：，：，：，：，：，：，：，：，（）：，：，：，：，（）：，（）：，（）：，：，：王莉，李晓娟，关永，等神经网络可信性的形式化验证方法综述 小型微型计算机系统，（）：（，（）：），：，：，：，：，：，（）：，：，：，：，：（）：，（）：计 算 机 应 用 研 究 第 卷