利用形式化模型、安全防護和經過驗證的控制來驗證基於 AI 的列車系統

核心概念

本文介紹一種將形式化驗證技術與基於 AI 的感知系統和經過驗證的控制相結合的方法，以提高自主列車系統的安全性。

摘要

文章類型

這是一篇研究論文。

研究摘要

• 文獻資訊: Gruteser, J., Roßbach, J., Vu, F., & Leuschel, M. (2024). Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems. In Sixth International Workshop on Formal Methods for Autonomous Systems (FMAS 2024) (pp. 151–159). EPTCS. https://doi.org/10.4204/EPTCS.411.10
• 研究目標: 本研究旨在探索一種結合形式化方法、安全防護和經過驗證的控制來驗證基於 AI 的列車系統的方法，以解決 AI 組件在安全攸關應用中的安全問題。
• 方法: 研究人員使用 B 方法建立了一個包含環境、轉向系統和感知系統的列車控制系統的形式化模型。他們使用真實的 AI 組件（例如 YOLO）進行模擬，並使用經過驗證的控制來監控 AI 的輸出。此外，他們還設計了安全防護措施，以防止基於 AI 感知和已知環境的不安全操作。
• 主要發現: 研究結果表明，通過將形式化模型與真實的 AI 執行和經過驗證的控制相結合，可以有效地識別基於 AI 的感知系統和安全防護措施中的潛在弱點。例如，經過驗證的控制可以有效減少誤報，而安全防護可以處理誤報。
• 主要結論: 本研究強調了在基於 AI 的安全攸關系統中結合形式化方法、運行時監控和統計驗證的重要性。這種組合方法有助於在開發早期識別潛在問題，並提高系統的整體安全性。
• 意義: 這項研究對自主列車系統的開發具有重要意義，因為它提供了一種系統化且嚴謹的方法來驗證和確保此類系統中 AI 組件的安全性。
• 局限性和未來研究方向: 本研究的局限性包括需要一個更逼真的模擬環境，以及需要改進安全防護措施以處理經過驗證控制的誤報。未來的研究方向包括將該方法應用於更複雜的列車控制場景，並探索其他形式化驗證技術。

統計資料

使用 500 次模擬運行進行蒙地卡羅模擬。
列車在沒有安全防護和經過驗證的控制的情況下，在第一個錯誤檢測到的停車信號前總是提前停車。
經過驗證的控制幾乎消除了所有誤報。
經過驗證的控制導致正確檢測顯著減少。

引述

"This work deals with systems that employ an AI perception system, such as image recognition. Those systems include autonomous vehicles and autonomous railway systems."
"This work presents a real-time demonstrator linking the formal model, the AI, and certified control, extending an approach used to validate reinforcement learning agents [34]."
"The main benefit of our methodology is that we can link the execution of a real AI model to a formal model and check its behaviour using formal properties and statistical validation techniques."

從以下內容提煉的關鍵洞見

Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems

by Jan ... 於 arxiv.org 11-22-2024

https://arxiv.org/pdf/2411.14374.pdf

深入探究

該方法如何應用於其他類型的自主系統，例如自動駕駛汽車或無人機？

此方法的核心概念是將 形式化模型、AI 和 驗證過的控制 結合起來，並適用於任何依賴 AI 感知系統的安全攸關系統。以下說明如何將其應用於自動駕駛汽車和無人機：
自動駕駛汽車：

形式化模型： 建立自動駕駛汽車的行為模型，包括車輛動力學、交通規則、環境互動等。可以使用類似 B 方法的形式化語言進行建模。
AI 感知系統： 使用 AI 演算法，例如卷積神經網路 (CNN)，處理來自感測器（如相機、雷達、光達）的數據，以識別道路標誌、交通號誌、行人和其他車輛。
安全防護： 在形式化模型中設計安全防護，例如：

緊急煞車系統： 當 AI 感知系統未能及時識別障礙物時，啟動緊急煞車。
車道維持輔助： 當車輛偏離車道且 AI 感知系統未做出適當反應時，將車輛導回車道。

驗證過的控制： 使用經過驗證的演算法，例如基於模型的控制或經典控制理論，監控 AI 感知系統的輸出，並在必要時進行干預。
模擬和驗證： 使用模擬環境，例如 CARLA，模擬各種駕駛場景，並使用形式化驗證工具，例如 ProB 和 SimB，驗證系統的安全性。

無人機：

形式化模型： 建立無人機的飛行控制系統模型，包括飛行路徑規劃、避障策略、感測器數據融合等。
AI 感知系統： 使用 AI 演算法，例如 CNN 或強化學習 (RL)，處理來自感測器（如相機、慣性測量單元 (IMU)、全球導航衛星系統 (GNSS)）的數據，以識別障礙物、規劃飛行路徑、進行目標跟踪等。
安全防護： 在形式化模型中設計安全防護，例如：

地理圍欄： 限制無人機的飛行區域，防止其進入禁飛區。
返航功能： 當無人機失去與操作員的連接或電池電量不足時，自動返回起飛點。

驗證過的控制： 使用經過驗證的演算法，例如比例-積分-微分 (PID) 控制或模型預測控制 (MPC)，監控 AI 感知系統的輸出，並確保無人機的穩定飛行。
模擬和驗證： 使用模擬環境，例如 Gazebo 或 AirSim，模擬各種飛行場景，並使用形式化驗證工具驗證系統的安全性。

總之，該方法可以通過調整形式化模型、AI 感知系統、安全防護和驗證過的控制等組件，應用於各種自主系統，以提高其安全性。

如果 AI 感知系統的準確性顯著提高，安全防護和經過驗證的控制是否仍然必要？

即使 AI 感知系統的準確性顯著提高，安全防護和經過驗證的控制仍然是必要的。原因如下：

未知情況和邊緣案例： AI 感知系統通常在大量數據上進行訓練，但仍然無法預測所有可能的情況，尤其是在複雜和動態的環境中。安全防護和經過驗證的控制可以作為一道額外的防線，處理 AI 感知系統無法處理的未知情況和邊緣案例。
感測器故障和數據錯誤： 感測器可能會出現故障，提供錯誤或不完整的數據。安全防護和經過驗證的控制可以檢測這些錯誤，並採取適當的措施，例如切換到備用感測器或啟動安全模式。
軟體錯誤和系統故障： 任何軟體系統都可能存在錯誤，自主系統也不例外。安全防護和經過驗證的控制可以幫助減輕軟體錯誤和系統故障帶來的風險。
安全認證和法規要求： 對於安全攸關的應用，例如自動駕駛汽車和無人機，安全認證和法規要求通常要求系統具備多層次的冗餘和安全機制。安全防護和經過驗證的控制是滿足這些要求的必要組成部分。

總之，即使 AI 感知系統的準確性很高，安全防護和經過驗證的控制仍然是確保自主系統安全的必要措施。它們可以處理 AI 感知系統無法處理的情況，提高系統的可靠性和安全性，並滿足安全認證和法規要求。

我們如何設計一個道德框架來指導基於 AI 的安全攸關系統的決策過程，尤其是在不可避免地發生事故的情況下？

設計一個道德框架來指導基於 AI 的安全攸關系統的決策過程，尤其是在不可避免地發生事故的情況下，是一個極具挑戰性的議題。以下是一些可以考慮的關鍵原則和步驟：
1. 明確價值觀和原則：

人類安全優先： 道德框架的首要原則應始终將人類安全置於首位，即使這意味著犧牲效率或其他目標。
透明度和可解釋性： AI 系統的決策過程應盡可能透明和可解釋，以便人類可以理解其背後的邏輯和推理。
公平和平等： AI 系統的決策不應基於任何形式的歧視，例如種族、性別、年齡或社會經濟地位。
責任和問責制： 應建立明確的責任和問責制機制，以確保在發生事故時可以追究相關人員的責任。
2. 建立決策模型：

基於規則的系統： 可以預先定義一組規則和約束條件，以指導 AI 系統的決策過程。例如，在自動駕駛汽車中，可以設定規則，要求車輛始终遵守交通法規和限速規定。
基於價值的學習： 可以訓練 AI 系統學習和理解人類的價值觀和道德原則，並將其納入決策過程中。例如，可以使用強化學習技術，訓練 AI 系統在模擬環境中進行決策，並根據其對人類安全的影響給予獎勵或懲罰。
混合方法： 可以結合基於規則的系統和基於價值的學習，以創建更強大和靈活的決策模型。
3. 處理不可避免的事故：

最小化損害： 在不可避免地發生事故的情況下，AI 系統應盡可能減少損害。例如，自動駕駛汽車可以選擇撞向障礙物，而不是撞向行人。
公開透明的調查： 在發生事故後，應進行公開透明的調查，以確定事故原因，並追究相關人員的責任。
持續改進： 應從事故中吸取教訓，並不斷改進 AI 系統的設計和訓練，以防止類似事故再次發生。
4. 社會共識和法規制定：

廣泛的社會討論： 設計道德框架需要廣泛的社會討論，以確保其反映社會的價值觀和期望。
制定相關法規： 政府應制定相關法規，以規範基於 AI 的安全攸關系統的開發和部署，並確保其符合道德標準。
設計一個道德框架來指導基於 AI 的安全攸關系統的決策過程是一個複雜且持續演進的過程。需要社會各界的共同努力，才能確保這些系統安全、可靠且符合人類的價值觀。