一種針對安全可達動態系統的形式化學習方法

摘 要：在動態系統建模問題中，深度學習為建模提供了更便捷和靈活的方法，但其難以解釋的特點降低了模型的可靠性。針對具有安全性和可達性的動態系統，提出了一種形式化模型學習方法，將安全性和可達性引入到對目標系統的學習過程中，使模型滿足這兩個性質。為保證所學系統在定義域上嚴格滿足這兩個性質，該方法基于現代控制理論中的Lyapunov方法和Barrier函數設計了可驗證的Lyapunov Barrier函數（LBF），通過將其與動態系統聯合學習，使得LBF能夠為所學系統提供安全性和可達性保障。最后通過求解混合整數線性規劃問題驗證了模型確實滿足相關性質，與DDPG的對比實驗展示了這一方法的有效性。

關鍵詞：形式化方法；動態系統學習；安全性；可達性

中圖分類號：TP301.2 文獻標志碼：A 文章編號：1001-3695（2023）08-026-2411-06

doi： 10.19734/j.issn.1001-3695.2022.12.0822

Formal learning approach for safe and reachable dynamical systems

Lu Tengfei Lou Pandeng Wang Shengpu Ding Mi Lin Wang

（1. School of Computer Science amp; Technology， Zhejiang Sci-Tech University， Hangzhou 310018， China; 2. Zhejiang TangClour AI Co.， Ltd.， Hangzhou 311121， China）

Abstract：In the problem of dynamic system modeling， deep learning based techniques make modeling more convenient and flexible， but it reduces the reliability of the learned model because of the difficulty in explanation. For dynamic systems with safety and reachability， this paper proposed a formal learning approach that introduced safety and reachability into the learning process of the target system， making the model satisfy these two properties. In order to ensure that the learned system strictly satisfies these two properties in the entire state space， this approach combined the Lyapunov method with Barrier function in modern control theory， and designed a verifiable Lyapunov Barrier function（LBF）， which was jointly learned with the dynamic system and guarantee security and reachability for the learned system. In addition， this paper employed the mixed integer linear programming in the verification about that the model satisfied the relevant properties. It makes a comparison with DDPG based method and the experimental results demonstrate the effectiveness and efficiency of the proposed approach.

Key words：formal method; dynamical system learning; security; reachability

0 引言

信息物理系統廣泛應用于工業控制、自動駕駛和航空航天等涉及社會運作和人身安全的關鍵基礎設施，這類系統關乎人身、財產和環境安全，因此建立可靠的系統模型至關重要。在這一情形下，基于嚴格數學基礎的形式化方法被應用于系統可靠性研究中［1］。如今深度學習方法為動態系統建模提供了新的途徑，但其難以解釋的特點導致模型的可靠性難以保證，比如在動態系統中常見的兩種性質——安全性和可達性，在通過深度學習的方法對系統進行建模后這兩個性質的證明變得十分困難。其中，安全性是指對于給定動態系統的初始狀態，系統在隨時間演化的過程中不會進入不安全狀態集；系統的可達性是指對于給定系統的初始狀態，系統隨著時間的推移總能進入目標狀態集。由于Barrier函數可以將系統的狀態空間分割成兩個子集，常被用來證明系統的安全性。Lyapunov理論是刻畫動力系統穩定性的方法，求出系統的Lyapunov函數可以保證系統的穩定性。這類函數能夠為系統提供某些性質的保障，因此也被稱為證書。

為了在建模的同時保證系統的某些性質，諸多領域從不同的角度為此做了大量的研究工作，目前已存在許多針對不同種類系統的建模方法，但如何在學習動態系統的同時為模型提供安全性和可達性的保障仍是懸而未決的問題。比如文獻［2，3］通過將系統投影到一個隱空間來保證系統的穩定性，在該隱空間中Lyapunov函數嚴格滿足定義，但是這種方法給系統施加了過強的限制，犧牲了神經網絡的靈活性，而且該方法沒有考慮系統的安全性。Taylor等人［4］迭代地收集數據并更新系統的控制器，使用控制Barrier函數以減少模型的不確定性，最終實現系統的安全行為，但是該方法沒有考慮系統的可達性。最近，Dawson等人［5］在控制器合成任務中通過CLBF（control Lyapunov Barrer function）使控制系統滿足安全性和可達性，但是未對該控制器和系統進行驗證，實際上該方法建立的系統在狀態空間中有稀疏的狀態點違背了安全性和可達性。

目前，在動態系統的學習任務中，同時保證安全性和可達性的研究幾乎處于空白狀態。受到Dawson等人［5］的啟發，本文提出了一個基于數據驅動的學習方法FLA-SR（a formal learning approach for safe and reachable dynamical systems），該方法通過聯合學習非線性動態系統和Lyapunov-Barrier函數（LBF），為系統的安全性和可達性提供保障。LBF既要滿足安全條件也要滿足可達條件。但由于神經網絡的引入導致模型具有不可解釋性，這使得人們難以分析其行為。為了給系統的安全性和可達性提供一個形式化的保證，有必要驗證所學的系統以及LBF。為此將系統和LBF的驗證問題轉換為混合整數線性規劃（mixed-integer linear programming， MILP）問題，并通過數值求解器 Gurobi 對該問題求解，以確保LBF的有效性。最后，將FLA-SR和深度強化學習中常用的DDPG方法進行對比，實驗表明，FLA-SR對系統的長遠預測準確度明顯優于DDPG方法，而且LBF有效地約束了神經網絡形式的動態系統模型。本文主要貢獻如下：a）提出了一個學習框架，該框架同時考慮了系統的安全性和可達性，并且使用LBF作為系統具有安全性和可達性的通用證書，而不是像多數研究將各個性質分開考慮，簡化了證書的表達；b）提出了一個驗證框架，通過以ReLU為激活函數的神經網絡表示證書，并將神經網絡的驗證問題轉換為MILP優化問題，使用優化求解器Gurobi編碼和求解；c）在一組基準樣例中成功合成了LBF，證明了算法框架的有效性。

1 相關工作

1.1 動態系統建模

不同場景下的動態系統各自具有不同特點，也不存在一種統一的方法能夠為所有系統建立模型。線性系統相比其他系統更易于處理，因此如何學習穩定線性動態系統［6，7］較早地受到了關注，近來有更多學者著手研究穩定非線性系統的學習問題［8～12］。Richards等人［13］較早地探索了深度學習和Lyapunov分析的交叉點，文獻［2，3］以聯合學習方式學習動態系統和Lyapunov函數，并且在學習過程中通過Lyapunov函數投影方法來限制系統的穩定性，其優點是無須驗證即可保證所學系統的穩定性，但是對系統的限制可能過強，無法發揮出神經網絡的靈活性。Wang等人［14］提出的學習方法針對單調穩定系統，該方法認為系統的某一狀態不僅依賴于上一個狀態，之前的n個狀態都對當前狀態有貢獻，因而訓練了n個神經網絡并將其輸出取凸組合。Abate 等人［15］實現了一個名為FOSSIL的工具，對給定了常微分方程（ODE）形式的動態系統，用反例制導的方法合成Barrier和Lyapunov函數，以證明系統的安全性和穩定性，反例由可滿足性模理論（SMT） 求解器解得。

動態系統在數學上通常用微分方程表示，一些研究工作聚焦于如何建立系統的微分方程，該方法已廣泛用于時間序列預測和常微分方程估計［16，17］。Chen等人［18］提出了一類名為Neural ODE的新型神經網絡，該模型訓練時間明顯增加，但是空間復雜度為O（1），發表后被給予很高期望。Mehta等人［19］考慮到物理系統的部分行為通?？捎晌⒎址匠袒蚍匠探M給出，提出了一種將這些先驗知識融入Neural ODE的方法?；贜eural ODE的方法現已被應用到概率分布變換［20］和圖像識別［21，22］中，這些方法都非常新穎，但是關于這些系統具體性質的研究較少報道。Mehrjou等人［23］提出了另一種用于學習連續系統的方法，使用插值技術將離散軌跡連續化，在學習連續系統的同時求出Lyapunov函數以保證系統的穩定性，該方法把吸引域作為先驗信息引入學習過程。

上述方法針對的系統各有特點，但考慮系統穩定性的研究較多，安全性和可達性相對較少被考慮到，后兩個性質的研究主要集中在控制領域。要保證這些性質在神經網絡上成立，必須依賴形式化技術。

1.2 形式化技術在學習控制任務中的應用

基于嚴格數學基礎的形式化方法已經被公認為驗證系統是否具有安全性的有效方法，在工業領域中得到越來越廣泛的應用［1］。在這一背景下，形式化方法被引入到深度學習領域以訓練滿足條件的神經網絡。Lyapunov和Barrier函數主要應用于控制領域，這類函數也被稱為證書（certificates），因為它們為控制器或系統的行為提供了某種保障。通過學習基于神經網絡的Lyapunov或Barrier函數以及相應的控制策略，使系統滿足相應性質，如Jin等人［24］用這種方法得到了安全和可達的控制器，但是沒有進一步驗證。Saha 等人［25］對問題做了簡化，他們對給定的Lyapunov函數求穩定控制器，但實際上Lyapunov函數很難事先給出；Zhao等人［26］提出了安全控制器的合成方法，其安全性由Barrier函數保證，但是該方法針對連續系統，由于連續系統Barrier函數定義與離散系統有所不同，驗證方法也不一樣。Dawson等人［5］采用神經網絡表示標稱控制器和CLBF，求得滿足要求的CLBF后，通過解一個特定的優化問題得到安全和穩定的控制器。這項工作受到CLBF的啟發，通過聯合學習動態系統和對應的LBF保證了系統的安全性和可達性。

通過深度學習方法合成Lyapunov函數或Barrier函數需要進一步驗證，這涉及到神經網絡的可信性分析［27］。為解決這一問題，SMT［28］、輸入精化（input refinement）［29］、線性逼近［30］、MILP［31］等方法被引入到神經網絡的形式化驗證中。Tjeng等人［31］用MILP評估神經網絡的魯棒性；后來Zhao等人［32］用這一技術驗證屏障證書，其原理是將ReLU函數替換為一系列線性約束和二值約束，從而用MILP計算神經網絡在給定輸入區域上的最大或最小輸出。文獻［32］處理的系統是連續的，而在本項工作中合成的是離散系統，驗證過程中的編碼方式有較大差異。

2 基礎知識

2.1 動態系統及其性質

2.2 神經網絡驗證方法

3 形式化模型學習方法 FLA-SR

3.1 聯合學習動態系統和LBF

3.2 基于MILP的形式化驗證

4 實驗及應用

4.1 實驗設置

4.2 范德波爾振蕩器

4.3 倒立擺

給定初始區域的五個隨機初始狀態作為測試樣本，應用FLA-SR方法合成的系統預測結果如圖4（a）所示，可以看到預測軌跡和真實軌跡基本吻合，誤差保持在10－4以內，表明FLA-SR對非多項式系統的預測誤差依然很小，這是因為FLA-SR是基于數據驅動的，對于原始系統的數學形式并不敏感。圖4（b）展示了DDPG對系統的預測結果，雖然在一定程度上滿足了系統的安全性，但是沒有在測試時間內到達目標區域，而且對系統的動態行為預測表現不佳。一個可能的解釋是，該系統從初始狀態出發到達目標區域的過程中，部分狀態沿著遠離目標區域的方向演化，這對于DDPG而言相當于是一個多目標優化問題，而降低預測誤差和到達目標區域是兩個相互矛盾的目標。另外，盡管從預測圖像上看，DDPG對系統的預測滿足安全性，但是由于無法提供形式化保證，在訓練集之外的狀態上仍有可能違反安全性。

圖5展示了兩種方法的均方誤差，雖然FLA-SR在非多項式系統上的長遠預測結果較上一案例有所增加，但是在數值上仍顯著小于DDPG。兩者的預測誤差在0.7 s后基本維持不變，這主要得益于系統的穩定性。值得注意的是，訓練過程的損失函數只考慮單步預測誤差，但在最后的軌跡預測時作出200步預測，FLA-SR 的誤差在長期預測中不會顯著增長，這主要得益于系統的穩定性。

5 結束語

動態系統常常具有安全性和可達性，建模過程中應保證這些性質成立，但是當深度學習方法被應用到動態系統的建模中時，這兩個性質便很難得到保障。為了解決這個問題，本文提出了FLA-SR方法，該方法引入Lyapunov Barrier函數（LBF），并通過數據驅動的方式聯合學習未知形式的動態系統和LBF，建立了可達且安全的系統模型。神經網絡表示的LBF帶來了新的形式化問題，為此將其轉換為一組混合整數線性規劃問題，通過優化問題求解器 Gurobi 編碼和求解。應當指出，FLA-SR目前還只能為低維度系統建模，在高維度復雜問題上難以合成有效的LBF，即在系統的狀態空間中存在反例而不能通過驗證，而且驗證時長大大增加。在后續工作中，將進一步探究高維度系統的可信學習方法和算力更節約的驗證方法。

參考文獻：

［1］王淑靈，詹博華，盛歡歡，等. 可信系統性質的分類和形式化研究綜述 ［J］. 軟件學報，2022，33（7）： 2367-2410. （Wang Shuling，Zhan Bohua，Sheng Huanhuan，et al. Survey on requirements classification and formalization of trustworthy systems ［J］. Journal of Software，2022，33（7）： 2367-2410.）

［2］Manek G，Kolter J Z. Learning stable deep dynamics models ［C］// Proc of the 33rd International Conference on Neural Information Processing Systems. Red Hook，NY： Curran Associates Inc.，2019： 11128-11136.

［3］Takeishi N，Kawahara Y. Learning dynamics models with stable inva-riant sets ［C］// Proc of the 35th AAAI Conference on Artificial Intelligence. Palo Alto，CA： AAAI Press，2021： 9782-9790.

［4］Taylor A，Singletary A，Yue Yisong，et al. Learning for safety-critical control with control barrier functions ［C］// Proc of the 2nd Confe-rence on Learning for Dynamics and Control. 2020： 708-717.

［5］Dawson C，Qin Zengyi，Gao Sicun，et al. Safe nonlinear control using robust neural Lyapunov-Barrier functions ［C］// Proc of the 5th Conference on Robot Learning. 2022： 1724-1735.

［6］Lacy S L，Bernstein D S. Subspace identification with guaranteed stability using constrained optimization ［J］. IEEE Trans on Automatic Control，2003，48（7）： 1259-1263.

［7］Siddiqi S M，Boots B，Gordon G J. A constraint generation approach to learning stable linear dynamical systems ［C］// Proc of the 20th International Conference on Neural Information Processing Systems.Red Hook，NY： Curran Associates Inc.，2007： 1329-1336.

［8］Khansari-Zadeh S M，Billard A. Learning stable nonlinear dynamical systems with Gaussian mixture models ［J］. IEEE Trans on Robo-tics，2011，27（5）： 943-957.

［9］Neumann K，Lemme A，Steil J J. Neural learning of stable dynamical systems based on data-driven Lyapunov candidates ［C］// Proc of IEEE/RSJ International Conference on Intelligent Robots and Systems. Piscataway，NJ： IEEE Press，2013： 1216-1222.

［10］Umlauft J，Hirche S. Learning stable stochastic nonlinear dynamical systems ［C］// Proc of the 34th International Conference on Machine Learning. 2017： 3502-3510.

［11］Duncker L，Bohner G，Boussard J，et al. Learning interpretable continuous-time models of latent stochastic dynamical systems ［C］// Proc of the 36th International Conference on Machine Learning. 2019： 1726-1734.

［12］Massaroli S，Poli M，Bin M，et al. Stable neural flows ［EB/OL］. （2020-03-18）. https：//arxiv.org/pdf/2003.08063.pdf.

［13］Richards S M，Berkenkamp F，Krause A. The Lyapunov neural network： adaptive stability certification for safe learning of dynamical systems ［C］// Proc of the 2nd Conference on Robot Learning. 2018： 466-476.

［14］Wang Yu，Gao Qitong，Pajic M. Deep learning for stable monotone dynamical systems ［EB/OL］. （2020-06-22）. https：//arxiv.org/pdf/2006.06417v1.pdf.

［15］Abate A，Ahmed D，Edwards A，et al. FOSSIL： a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks ［C］// Proc of the 24th International Conference on Hybrid Systems： Computation and Control. New York： ACM Press，2021： article No.24.

［16］Schlkopf B，Smola A J. Learning with kernels： support vector machines，regularization，optimization，and beyond ［M］. Cambridge，MA： MIT Press，2002.

［17］Michalak M. Time series prediction with periodic kernels ［C］// Computer Recognition Systems 4. Berlin： Springer，2011： 137-146.

［18］Chen R T Q，Rubanova Y，Bettencourt J，et al. Neural ordinary diffe-rential equations ［C］// Proc of the 32nd International Conference on Neural Information Processing Systems. Red Hook，NY： Curran Associates Inc.，2018： 6572-6583.

［19］Mehta V，Char I，Neiswanger W，et al. Neural dynamical systems： balancing structure and flexibility in physical prediction ［C］// Proc of the 60th IEEE Conference on Decision and Control. Piscataway，NJ： IEEE Press，2021： 3735-3742.

［20］Papamakarios G，Nalisnick E T，Rezende D J，et al. Normalizing flows for probabilistic modeling and inference ［J］.Journal of Machine Learning Research，2021，22（57）： 1-64.

［21］Rodriguez I D J，Ames A，Yue Y. LyaNet： a Lyapunov framework for training neural ODEs ［C］// Proc of the 39th International Conference on Machine Learning. 2022： 18687-18703.

［22］Dupont E，Doucet A，Teh Y W. Augmented neural odes ［C］// Proc of the 33rd International Conference on Neural Information Processing Systems. Piscataway，NJ： IEEE Press，2019： 3140-3150.

［23］Mehrjou A，Iannelli A，Schlkopf B. Learning dynamical systems using local stability priors ［EB/OL］. （2020-08-23）. https：//arxiv.org/pdf/2008.10053.pdf.

［24］Jin Wanxin，Wang Zhaoran，Yang Zhuoran，et al. Neural certificates for safe control policies ［EB/OL］. （2020-06-15）. https：//arxiv.org/pdf/2006.08465.pdf.

［25］Saha P，Egerstedt M，Mukhopadhyay S. Neural identification for control ［J］. IEEE Robotics and Automation Letters，2021，6（3）： 4648-4655.

［26］Zhao Qingye，Chen Xin，Zhao Zhuoyu，et al. Verifying neural network controlled systems using neural networks ［C］// Proc of the 25th ACM International Conference on Hybrid Systems： Computation and Control. New York： ACM Press，2022： article No.3.

［27］王莉，李曉娟，關永，等. 神經網絡可信性的形式化驗證方法綜述 ［J］. 小型微型計算機系統，2022，43（9）： 1830-1837. （Wang Li，Li Xiaojuan，Guan Yong，et al. Review of formal verification methods for credibility of neural networks ［J］. Journal of Chinese Compu-ter Systems，2022，43（9）： 1830-1837.）

［28］Huang Xiaowei，Kwiatkowska M，Wang Sen，et al. Safety verification of deep neural networks ［C］// Proc of the 29th International Confe-rence on Computer Aided Verification. Cham： Springer，2017： 3-29.

［29］Katz G，Barrett C，Dill D L，et al. Reluplex： an efficient SMT solver for verifying deep neural networks ［C］// Proc of the 29th Internatio-nal Conference on Computer Aided Verification. Cham： Springer，2017： 97-117.

［30］Wong E，Kolter Z. Provable defenses against adversarial examples via the convex outer adversarial polytope ［C］// Proc of the 35th International Conference on Machine Learning. 2018： 5286-5295.

［31］Tjeng V，Xiao Kai，Tedrake R. Evaluating robustness of neural networks with mixed integer programming ［EB/OL］. （2019-02-18）. https：//arxiv.org/pdf/1711.07356.pdf.

［32］Zhao Qingye，Chen Xin，Zhang Yifan，et al. Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ［C］// Proc of the 24th International Conference on Hybrid Systems： Computation and Control. New York： ACM Press，2021： 1-11.

［33］He Kaiming，Zhang Xiangyu，Ren Shaoqing，et al. Deep residual learning for image recognition ［C］// Proc of IEEE Conference on Computer Vision and Pattern Recognition. Washington DC： IEEE Computer Society，2016： 770-778.

［34］Gurobi Optimization L L C. Gurobi optimizer reference manual［EB/OL］.（2019-12-27）.http：//www.gurobi.cn/download/GuNum.pdf.

［35］Lillicrap T P，Hunt J J，Pritzel A，et al. Continuous control with deep reinforcement learning ［EB/OL］. （2019-07-05）. https：//arxiv.org/pdf/1509.02971.pdf.