以AI驗證AI：務實的進化還是危險的豪賭？

前言

     《Fighting AI with AI: Leveraging Foundation Models for Assuring AI-Enabled Safety-Critical Systems》探討了在航空航天和自動駕駛等安全關鍵系統中，使用深度神經網絡（DNNs）進行軟件保證所面臨的挑戰，並提出了一個名為“以AI治AI”的解決方案框架。該框架由兩個互補組件構成：REACT（利用大型語言模型/LLMs）專注於彌合非正式需求與形式化規約之間的語義鴻溝，以實現早期驗證和測試用例生成；而SemaLens（利用視覺語言模型/VLMs）則充當“分析透鏡”，用於測試、調試和監控DNN感知系統的行為，使其能被人類可理解的概念進行解釋。討論這一方法的前景與風險，肯定了其在解決傳統需求工程痛點和語義匹配方面的進步，同時也警示了這種“用一個黑箱驗證另一個黑箱”的策略對系統信任鏈的潛在脆弱性，尤其是在涉及複雜性、不確定性和行業認證的背景下。

正如在“論點交鋒”播客中一位工程師所言，將深度神經網絡（DNNs）集成到航空航天等安全關鍵系統中，“這絕對是一場噩夢”。傳統的驗證方法在AI面前幾乎完全失效，其核心挑戰主要有兩點：

1. 不透明性（黑箱問題）：我們無法完全理解AI做出某個決策的具體內部邏輯。

2. 語義鴻溝：工程師用自然語言提出的高層需求（例如，“車輛必須能識別行人”）與AI實際處理的底層像素數據之間存在巨大的脱節，難以建立可靠的驗證關聯。

為了應對這些挑戰，一個大膽的思路應運而生：以AI驗證AI。即利用能力更強的大型語言模型（LLM）和視覺語言模型（VLM）等基礎模型，來反向驗證、測試和監控系統中的AI組件。

這便引出了我們領域的核心問題：“以AI驗證AI”，究竟是引領我們走出困境的務實的進化，還是一場將不可預測性層層疊加、置生命於險境的危險的豪賭？本文將通過正反雙方的觀點交鋒，幫助您深入理解這場辯論的核心。

核心框架簡介：理解我們正在辯論什麼

在進入辯論之前，我們首先需要了解作為討論基礎的集成框架，它由REACT和SemaLens兩個互補的組件構成。

REACT：從模糊到精確的需求工程助手

• 目標： 利用大型語言模型（LLM），將工程師用自然語言編寫的、可能充滿模糊性的需求，系統地轉化為精確、可驗證的形式化規約（Formal Specifications），例如線性時序邏輯（LTLf）。

• 價值： 旨在實現早期錯誤檢測。通過在設計階段就對形式化的需求進行一致性分析，可以發現需求間的潛在矛盾，避免在開發後期才發現問題而導致災難性的返工成本。

SemaLens：跨越語義鴻溝的“智能鏡頭”

• 目標： 利用視覺語言模型（VLM），讓測試和監控系統能夠以人類可理解的概念（如“天氣狀況”、“行人”、“交通錐”）去分析和評估感知系統的行為。

• 價值： 旨在彌合高層需求與底層像素數據之間的語義鴻溝，從而實現從需求到實現的端到端驗證，確保AI“看懂”了世界並做出了正確反應。

儘管這個框架藍圖看起來很理想，但其核心理念“以AI驗證AI”卻引發了深刻的爭議。

第一輪交鋒：核心前提的對決

正方觀點：這是必要且務實的進化

作為支持這一方向的工程師，我認為這是我們唯一可行的前進方向。

• 傳統方法已力不從心：我們不能“用舊地圖找新大陸”。傳統的軟件驗證方法在面對DNNs的複雜性和不確定性時已經捉襟見肘，我們迫切需要新的工具和思路。

• 嚴謹性與效率的結合：這個框架並非憑空創造，而是將形式化方法的嚴謹性與AI的效率和規模化能力巧妙結合。它精準地瞄準了需求模糊和語義鴻溝這兩大業界最核心的痛點。

• 提供了一條可行的路徑：它構建了一個從非正式需求到經過驗證的實現的端到端解決方案。這為滿足DO-178C等嚴苛的行業標準，提供了一條“看得見、摸得着的路徑”。

反方觀點：這是用一個黑箱驗證另一個黑箱

我對此持嚴重保留態度，這本質上是用一種我們同樣無法完全理解的工具去驗證另一個。

• 脆弱的信任鏈：該策略的本質是“用一種複雜性去掩蓋另一種複雜性”。整個系統的信任鏈完全建立在同樣不透明、本質上是概率性的基礎模型（LLM和VLM）極其脆弱。

• 承認自身不可靠：REACT Author模塊在翻譯一句自然語言需求時，會生成多個候選項讓工程師挑選。這個設計本身就等於承認了LLM可能會誤解原始意圖，從而需要“人在迴路”進行最終裁決。這恰恰引入了新的、由驗證工具本身帶來的風險。

• 風險的疊加：這不僅沒有解決原有的黑箱問題，反而引入了新的、更隱蔽的複雜性。對於“人命關天”的安全關鍵系統來説，這種做法太過冒險。

這種在核心前提上的根本分歧，迫使我們審視更深層次的問題。如果我們暫時接受正方的觀點，那麼這種人機協同在實踐中究竟表現如何？這便將辯論從宏觀理念，帶入了微觀的現實考量之中。

第二輪交鋒：實踐中的效率與陷阱

正方觀點：這是高效的人機協同，將專家智慧用在刀刃上

反方對“人在迴路”的質疑，恰恰説明了這個框架設計的巧妙之處。

• 重新定義“人在迴路”：我們必須承認，讓工程師從零開始手寫幾百條LTLf規約是一項極其耗時且容易出錯的工作。現在，AI像“成百上千個初級工程師”一樣，在幾分鐘內就完成了繁瑣的初稿工作。

• 提升專家價值：這使得人類專家得以從“繁瑣的語法工作中解放出來”，轉而聚焦於最高層次的語義決策——判斷哪個形式化描述最符合真正的系統設計意圖。例如，當AI將模糊的“系統應具備魯棒性”需求細化為多個具體場景（如“在10%丟包率下保持功能”、“在傳感器延遲50毫秒內正常運行”）時，它實際上是在幫助設計者明確之前未定義的細節。

• 減少無效投入：這是一種高效的人機協同模式，它把人類最寶貴的領域知識用在了刀刃上，總體上減少了無效的人工投入。

反方觀點：這製造了新的瓶頸，且判斷標準十分脆弱

正方所謂的“高效協同”可能只是一個美好的幻想。

• 創造新的巨大瓶頸：對於一個複雜的系統，當AI生成五個“看似相似，但對系統行為影響巨大”的選項時，領域專家需要投入海量的精力去理解每個選項背後的深層含義，甚至需要仿真才能判斷。這個審核過程本身就可能成為一個新的巨大瓶頸，甚至比從頭寫更費勁。

• 判斷標準極其脆弱：SemaLens最脆弱的一環，是它依賴一個預設的**相似度得分閾值（如0.4）**來做判斷（這一閾值在源論文的示例中被明確提及，説明這並非一個假設性問題）。讓我們設想一個場景：

這場爭論的核心，最終還是回到了AI的“黑箱”問題。我們是否真的能通過一個AI去理解另一個AI呢？這引出了關於“可解釋性”的終極辯論。

第三輪交鋒：可解釋性的突破與幻覺

正方觀點：AI“看到”了什麼，我們終於可以一探究竟

我認為SemaLens在可解釋性上取得了真正的突破。

• 技術核心：其AED（分析、解釋與調試）模塊做了一件非常酷的事情。它將我們目標DNN的內部數學表示（即嵌入空間）與像CLIP這樣強大的視覺語言模型的嵌入空間進行了對齊。

• 突破性價值：通過這種“對齊”，我們終於可以提出一些以前無法回答的問題。例如，當系統將一個物體識別為“卡車”時，我們可以反向提問：它是基於“金屬光澤”、“巨大的輪子”還是“方形車廂”這些人類可以理解的概念做出這個判斷的？

• 量化可解釋性：這讓可解釋性不再是一句空話，而有了可以量化的依據。這是在“模型為何如此決策”這個終極問題上邁出的重要一步。

反方觀點：我們得到的可能不是真相，只是一個更令人信服的假象

這個想法聽起來很巧妙，但這也恰恰是讓我最擔憂的地方。

• 問題的轉移而非解決：我們如何確定作為“翻譯官”的VLM（如CLIP）本身是正確無誤的？這只是將“解釋一個黑箱的問題”巧妙地轉換成了“理解兩個黑箱之間映射關係”的另一個、可能更復雜的問題。

• 解釋的不可靠性：如果作為“鏡頭”的CLIP模型本身就存在偏見——比如因為其訓練數據裏大部分消防車都是紅色的，導致它將“紅色”和“消防車”這兩個概念強行關聯——那麼基於它得出的所有解釋和所謂的語義覆蓋率都將是不可靠的。

• 危險的幻覺：這種方法可能帶來的後果是極其危險的。

這場辯論從技術理念深入到實施細節，最終必然要面對現實世界的終極考驗：監管與認證。

深刻的權衡與未來的挑戰

觀點彙總：一場勢均力敵的辯論

在擁抱創新與堅守安全之間尋求平衡

這場辯論沒有簡單的贏家。它深刻地揭示了在安全關鍵領域應用前沿AI技術時所面臨的深刻權衡。一邊是解決現有工程難題（如需求模糊、語義鴻溝）的巨大潛力；另一邊則是引入一項我們自己都還沒完全吃透的新技術所帶來的內在風險。

這場辯論最終給我們留下了一個嚴峻的工程現實：我們面臨着一個兩難選擇——一邊是傳統驗證方法的已知侷限，這些方法正逐漸失效；另一邊則是概率性工具的未知風險，這些工具我們尚未能完全駕馭。未來的出路並非要在這場辯論中選出贏家，而在於如何構建新的系統架構，用形式化方法的嚴謹性去約束AI的概率性力量，確保即便我們“以AI驗證AI”，人類的監督和判斷力依然是安全最終的仲裁者。

如有想了解更多軟件設計與架構, 系統IT,企業信息化, 團隊管理 資訊，請關注我的微信訂閲號：

作者：Petter Liu
出處：http://www.cnblogs.com/wintersun/
本文版權歸作者和博客園共有，歡迎轉載，但未經作者同意必須保留此段聲明，且在文章頁面明顯位置給出原文連接，否則保留追究法律責任的權利。 該文章也同時發佈在我的獨立博客中-Petter Liu Blog。