[發(fā)明專利]一種基于MSVL的BP神經(jīng)網(wǎng)絡的構建和訓練方法及系統(tǒng)

有效

• 申請?zhí)枺?/td>: 202110439442.6
• 申請日: 2021-04-23
• 公開（公告）號: CN113240075B
• 公開（公告）日: 2023-08-22
• 發(fā)明（設計）人: 趙亮;馮哲;段振華;王小兵;田聰;張南
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06N3/0499
• 分類號: G06N3/0499;G06N3/08;G06N3/084
• 代理公司: 西安長和專利代理有限公司 61227
• 代理人: 何畏

本發(fā)明屬于BP神經(jīng)網(wǎng)絡技術領域，公開了一種基于MSVL的BP神經(jīng)網(wǎng)絡的構建和訓練方法及系統(tǒng)，所述基于MSVL的BP神經(jīng)網(wǎng)絡的構建和訓練方法包括：根據(jù)BP神經(jīng)網(wǎng)絡基本的層次化結構和屬性行為特征，構建基于MSVL的BP神經(jīng)網(wǎng)絡的底層結構方法庫；根據(jù)用戶的定制需求，利用結構方法庫中的MSVL結構體，構建BP神經(jīng)網(wǎng)絡的初始架構；讀取樣本數(shù)據(jù)，利用結構方法庫中MSVL方法，對初始架構進行訓練，得到BP神經(jīng)網(wǎng)絡的形式化架構。本發(fā)明涵蓋了矩陣運算、反向傳播、權值更新等多種神經(jīng)網(wǎng)絡系統(tǒng)的基本行為，可直接用于模型檢測、插樁驗證等形式化驗證技術，并支持與這些行為相關的多方面性質(zhì)的驗證，從而系統(tǒng)的安全可信性能夠得到有效的保障。

技術領域

本發(fā)明屬于BP神經(jīng)網(wǎng)絡技術領域，尤其涉及一種基于MSVL的BP神經(jīng)網(wǎng)絡的構建和訓練方法及系統(tǒng)。

背景技術

目前，隨著神經(jīng)網(wǎng)絡系統(tǒng)的不斷發(fā)展和廣泛應用，這類系統(tǒng)是否安全可靠成為了一個人們越來越關注的問題。作為一種計算機系統(tǒng)，神經(jīng)網(wǎng)絡系統(tǒng)自身可能存在缺陷或漏洞，也可能遭到不同種類的惡意攻擊，且這樣的情形并不少見。尤其是許多系統(tǒng)應用在安全攸關的場景中，其細小的錯誤都可能導致嚴重的后果。2018年3月，美國亞利桑那州坦佩市一輛Uber無人駕駛汽車與行人發(fā)生碰撞，造成一名49歲女性重傷后救治無效死亡。2019年12月，一家名為Kneron的人工智能公司宣稱使用3D面具突破了支付寶、微信的人臉識別系統(tǒng)，還騙過了國內(nèi)某火車站的閘機，成功刷臉進站。

因此，檢驗并保障神經(jīng)網(wǎng)絡系統(tǒng)的安全性是非常必要的。目前，絕大多數(shù)神經(jīng)網(wǎng)絡系統(tǒng)采用測試的手段進行安全性檢驗。然而，測試不能確保系統(tǒng)不存在缺陷，而諸多的安全問題也說明了通過測試的系統(tǒng)仍不夠可靠。另一種檢驗手段是形式化驗證，采用模型檢測、定理證明等形式化方法對系統(tǒng)滿足預期性質(zhì)進行嚴格的邏輯推導，能夠保障系統(tǒng)的安全可信。

近年來，學術界對神經(jīng)網(wǎng)絡系統(tǒng)的形式化驗證開展研究，形成了一些初步的技術。現(xiàn)有技術一面向BP神經(jīng)網(wǎng)絡，通過定義一組操縱對標準樣本的鄰域空間離散化，由此建立一組邏輯約束，并使用可滿足性模理論邏輯求解方法來檢驗標準樣本鄰域空間中是否存在對抗樣本。現(xiàn)有技術二面向BP神經(jīng)網(wǎng)絡和卷積神經(jīng)網(wǎng)絡，借助于由浮點多面體和區(qū)間所組成的抽象域及其變換操作，推導和檢驗這些網(wǎng)絡的前條件、后條件和健壯性。現(xiàn)有技術三面向部署在云端的神經(jīng)網(wǎng)絡，通過一定的交互式證明協(xié)議實現(xiàn)了正確性的驗證，但是對神經(jīng)網(wǎng)絡的結構做了一些限制，例如僅采用二次激活函數(shù)等。

在現(xiàn)有的神經(jīng)網(wǎng)絡形式化驗證技術中，神經(jīng)網(wǎng)絡絕大多數(shù)是以Python、C等通用的程序設計語言所編寫。這些語言不具備形式化的語義理論基礎，不支持直接的數(shù)學邏輯推導，與形式化驗證存在一定的技術鴻溝。這使得不同的驗證技術不得不采用間接的方式，針對特定的神經(jīng)網(wǎng)絡和性質(zhì)進行數(shù)學建模，并做出不同程度的簡化限定。它們的技術內(nèi)容較分散，適用范圍偏小。

通過上述分析，現(xiàn)有技術存在的問題及缺陷為：待驗證的神經(jīng)網(wǎng)絡采用非形式化的程序設計語言編寫，缺乏數(shù)學邏輯基礎，無法直接用于形式化驗證，技術內(nèi)容較分散，適用范圍偏小，限定了各項神經(jīng)網(wǎng)絡驗證技術只能針對特定方面的問題進行建模和推導，難以形成一套有機的方法理論體系。

解決以上問題及缺陷的難度為：解決上述技術問題的途徑是采用形式化的方法來開發(fā)神經(jīng)網(wǎng)絡架構，包括網(wǎng)絡的構建和訓練。然而，神經(jīng)網(wǎng)絡的運行依賴于由機器學習而得到的各項參數(shù)，其行為被普遍認為是不透明、不可解釋的。如何為其建立形式化的框架是不小的挑戰(zhàn)。此外，神經(jīng)網(wǎng)絡的訓練樣本集和參數(shù)集往往規(guī)模龐大，這無疑增加了形式化的難度。

解決以上問題及缺陷的意義為：采用形式化的方法開發(fā)出的神經(jīng)網(wǎng)絡架構可直接用于形式化驗證，這避免了非形式化的程序設計與語言與形式化的邏輯推導之間的技術鴻溝。此外，采用形式化方法開發(fā)出的神經(jīng)網(wǎng)絡架構支持神經(jīng)網(wǎng)絡的矩陣運算、反向傳播、權值更新等多種行為，從而支持對神經(jīng)網(wǎng)絡多方面的性質(zhì)進行檢驗，有助于形成一套有機的方法理論體系。