天天看點

MIT博士提出可驗證型控制器架構,為控制非線性系統提供解決方案

作者:DeepTech深科技

近年來,神經網絡控制技術在機器人領域展現出令人驚豔的表現。這項基于深度學習的技術,曾驅動各種先進機器人完成了一系列複雜任務。

對于美國麻省理工學院博士生楊麓潔來說,這些先進機器人的名字,她早已能夠脫口而出。

MIT博士提出可驗證型控制器架構,為控制非線性系統提供解決方案

圖 | 楊麓潔(來源:楊麓潔)

比如:

有既能泡咖啡、又會主動與人對話的 Figure 通用人形機器人;有會系鞋帶、會晾衣服的 ALOHA 操作機器人;還有能越過各種地形執行偵查任務的機器狗等。

所有這些智能機器人的背後,都運作着精心設計的神經網絡控制器。

盡管神經網絡控制展現出卓越的實用性,但是目前仍然缺乏對于安全關鍵應用的穩定性保證。

而在控制理論領域,已有學者通過規範優化和形式化方法,為線性控制器或多項式控制器提供了嚴格的穩定性證明。

然而,要想讓更加複雜的神經網絡控制器擁有同樣的穩定性保證,依然存在一些難題。

對于基于神經網絡的控制器來說,開展嚴格的李雅普諾夫穩定性驗證具有重要意義,主要原因如下:

其一,要確定系統的安全性和可靠性。

機器人、自動駕駛汽車、工業控制系統等都會涉及到複雜的動态過程,一旦控制系統失穩可能會導緻嚴重的安全事故。

通過李雅普諾夫穩定性驗證,可以形式化地證明系統在一定區域内的漸進穩定性,進而保證系統能夠安全可靠地運作。

其二,擴大神經網絡在關鍵領域的應用。

由于缺乏穩定性保證,目前的神經網絡控制器在安全關鍵領域的應用依舊受到很大限制。

而一旦可以對其穩定性進行嚴格驗證,神經網絡就能大規模用于機器人、航空航天、生命科學等領域,進而發揮強大的控制性能。

其三,彌補神經網絡的理論缺陷。

盡管神經網絡在實踐中表現卓越,但它本身缺乏堅實的理論基礎。

通過與李雅普諾夫穩定性理論相結合,可以為神經網絡控制器注入理論支撐,彌補其在可解釋性和可靠性方面的不足。

其四,促進控制理論與機器學習的融合。

神經網絡和李雅普諾夫理論分别代表着機器學習和控制理論兩大領域的最新進展。

針對神經網絡控制器進行李雅普諾夫驗證,正是将這兩個領域進行結合的有力嘗試,必将推動兩個領域的交叉融合,産生新的理論突破。

其五,應對複雜系統的挑戰。

随着控制對象的日益複雜,單一的經典控制方法已經難以完全滿足需求。

對于神經網絡控制器來說,它具有學習複雜映射的能力。如果其穩定性也能得到保證,将為控制複雜非線性系統提供全新的解決方案。

基于此,楊麓潔和所在團隊提出一種新型架構,該架構采用快速經驗反證和正則化技術等方法,旨在同時學習神經網絡控制器和李雅普諾夫穩定性證明,以便能夠适用于複雜的非線性動态系統。

MIT博士提出可驗證型控制器架構,為控制非線性系統提供解決方案

(來源:arXiv)

楊麓潔等人所提出的新公式化方法,不僅定義了現有研究中從未涉及的、更大的可穩定區域,而且改進了針對穩定導數的限制條件,讓其隻聚焦于可被證明的穩定區域範圍。

通過這種新穎的方法,課題組突破了現有神經網絡控制器在提供穩定性證明上的瓶頸,為更加複雜的神經網絡控制系統提供了更大的可驗證穩定區域。

對于李雅普諾夫穩定性條件的驗證,該團隊采用事後嚴格驗證的方式,利用可擴充的、基于線性邊界傳播的神經網絡驗證技術,并運用分支定界算法、以及目前最先進的 α,β-CROWN 神經網絡驗證器,進而讓驗證方法兼具高效性和靈活性。

整個訓練流程和驗證流程,都可以在 GPU(graphics processing unit,圖形處理器)上加速完成,無需依賴代價高昂的傳統求解器。

通過這種新型驗證方式,能夠避免使用代價高昂的傳統求解器,確定了李雅普諾夫穩定性條件的嚴格驗證。

同時,還能兼顧計算效率和靈活性,讓針對神經網絡控制器的穩定性驗證,變得更加高效和更加可行。

通過此,課題組為複雜非線性系統的穩定控制,提供了新的解決方案,在工業、交通、航空航天等領域都具備潛在應用前景。

其一,可用于機器人控制系統。

即本次方法能用于機器人的運動控制。特别是對于具有複雜非線性動力學的機器人系統來說,利用本次所提出的神經網絡控制器和李雅普諾夫證明,能夠保證機器人運動的穩定性和收斂性。

其二,可用于自動駕駛和無人機的控制。

自動駕駛汽車和無人機等系統,往往具有非線性和高次元的動力學方程。

而通過本次方法可以設計具有穩定性保證的神經網絡控制器,提高自動駕駛和無人機的安全性和可靠性。

其三,可用于航天器和航空器的控制。

航天器和航空器通常具有複雜的非線性動力學模型,而本次方法可以為其提供穩定性保證的神經網絡控制解決方案。

其四,可用于工業過程的控制。

許多化工、冶金等工業過程,都涉及到複雜的非線性動态系統。本次方法可用于設計具有穩定性保證的神經網絡控制器,優化生産過程的控制性能。

其五,可用于生物醫學系統模組化與控制。

對于一些生物醫學系統比如基因調控網絡來說,可以使用非線性動力學模型來描述它。是以,本次方法有望用于這些系統的模組化和控制。

MIT博士提出可驗證型控制器架構,為控制非線性系統提供解決方案

(來源:arXiv)

另據悉,在相關論文截稿的前兩周,該團隊重新審視了論文中的數學公式。

在這次讨論之中,他們不僅針對公式加以深度優化,還發現了領域内已有研究中存在的錯誤和遺漏。

盡管本次研究的初步實驗結果已經遠遠超越目前該領域的最先進成果。但是,上述發現也讓他們決定采取一個大膽的舉措:推翻所有已有的實驗資料,基于優化後的公式全面設計實驗。

“這是一個充滿挑戰的決定,因為重新進行實驗意味着巨大的風險和額外的工作量,但我們堅持確定研究成果的嚴謹性與準确性。”楊麓潔表示。

經過連續奮戰,他們終于在論文截稿前 4 小時,完成了所有實驗和論文最後修改,確定了本次成果的高品質和創新性。

最終,相關論文以《用于狀态和輸出回報的 Lyapunov 穩定神經控制:一種用于高效合成和驗證的新形式》(Lyapunov-stable Neural Control for State and Output Feedback:A Novel Formulation for Efficient Synthesis and Verification)為題發在國際機器學習大會(ICML,International Conference on Machine Learning)[1]。

楊麓潔和豐田研究院戴泓楷博士是共同一作。

MIT博士提出可驗證型控制器架構,為控制非線性系統提供解決方案

圖 | 相關論文(來源:arXiv)

下一步,課題組将開展以下幾方面探索。

首先,提高模型的普适性與适應性。

即開發基于神經網絡的方法,來估計或優化系統的可靠性,以及調試和優化價值函數和控制障礙函數等其他控制名額,進而提高處理複雜動态系統時的可擴充性和靈活性。

其次,将理論與實踐加以進一步結合。

目前,課題組已經在無人機、以及一些标準控制基準上取得進展。

未來,可以将本次架構用于更多、更複雜的控制系統,比如用于工業機器人和自動駕駛汽車等,以驗證和提高其在複雜實際場景下的穩定性和可靠性。

再次,将開展跨學科的合作。

鑒于所研究問題的複雜性和跨學科特質,他們計劃與機器學習領域的專家合作,力争發展更好的解決方案。

如前所述,為了合成通用非線性動态系統的、具有李雅普諾夫穩定性的神經網絡控制器的目标,課題組還利用了神經網絡驗證領域的最新的驗證工具 α,β-CROWN(https://abcrown.org)。

α,β-CROWN 由楊麓潔的兩位合作者——美國伊利諾伊大學張歡教授、以及美國加州大學博士生施舟行共同研發。

在大規模計算機視覺神經網絡穩健性驗證和神經網絡控制器安全性驗證上,α,β-CROWN 展現出出色的擴充能力。

它利用了驗證問題的網絡結構,通過在神經網絡中傳播線性邊界進而加速運算。

同時,α,β-CROWN 的邊界傳播過程具有較好的“GPU 友好度”,支援大型網絡的高效驗證,并能借助分支定界技術來快速評估多個子問題。

是以,楊麓潔也希望能進一步利用 α,β-CROWN 的能力,來解決更多的神經網絡控制系統驗證問題。

參考資料:

1.https://arxiv.org/pdf/2404.07956

排版:朵克斯

繼續閱讀