驗證品質何時決定 AI 自動化能否奏效？

資料來源#

Antaeus: Hunting Repository-Level Logic Vulnerabilities via Context-Grounded LLM Reasoning

簡答#

當 AI 的輸出生成成本低廉，卻昂貴、危險，或根本不可能靠檢視來信任時，驗證品質就決定 AI 自動化能否奏效。在這種情況下，生成不是產品。經過驗證的產物才是產品。

這就是可驗證性論點的實務形式：傳統軟體自動化能被規格化的事物；LLM 系統自動化能被驗證的事物。驗證器越好，自主性就越能從「助理提出方案」移向「代理程式搜尋方案」。驗證器越差，系統就越容易退回人工審查、蓋章放行，或不安全的大量輸出。

驗證品質階梯#

1. 完美的機械式驗證器：自動化化為搜尋#

AI 驅動的形式化證明搜尋是最清楚的例子。代理程式產生 Lean 程式碼；Lean 會機械式檢查每個定義、定理和證明策略。只有在編譯器確認沒有待解目標、沒有 sorry，也沒有不允許的公理注入時，證明才會被接受。這將容易產生幻覺的數學文字，轉化為二元產物：接受或拒絕。

在這種情況下，驗證品質幾乎直接決定成敗：

驗證器夠可靠，能拒絕偽造的證明。
回饋夠局部，能引導下一次修改。
檢查成本夠低，能放進迴圈中執行。
接受的輸出夠有價值，值得送交人類做結構性審查，而不必逐行確認真偽。

驗證器不只是最後一道關卡。Lean 編譯器錯誤能為代理程式的下一輪提供依據。這就是代理程式迴圈超越客製化系統的意義：DeepMind 的基本獨立證明代理程式迴圈，在 9 道已解決的 Erdos 題目上，表現媲美繁複的演化式／AlphaProof 裝置，雖然在最難的題目上成本較高。這個迴圈之所以有效，是因為驗證器夠強，能讓簡單的搜尋產生效益。

重要的限制在於 Lean 自身的前沿：mathlib 的成熟度決定能觸及哪些範圍。完美的驗證器不會讓所有領域都準備就緒；它只會讓目標可形式化、且有支援函式庫的領域得以自動化。

2. 強大但不完整的驗證器：自動化可行，但基礎設施成為瓶頸#

軟體工程在階梯上低於 Lean。測試、CI、lint、型別檢查器、規格和程式碼審查都是真正的驗證器，但只涵蓋部分範圍。它們能抓出回歸、風格錯誤、型別違規、明顯錯誤和規格偏移；卻無法證明整個產品都正確。

因此，驗證成為新瓶頸正是可驗證性論點在組織層面的結果。一旦 Claude Code 讓寫程式變得便宜，稀缺資源就會變成對變更正確性的信心。瓶頸從撰寫程式碼轉移到驗證、審查和維護。

當驗證前移時，自動化就能奏效：

測試在程式碼之前或同步撰寫，讓 TDD 不再帶有過去那種「額外成本」。
規格放在儲存庫中，讓代理程式能檢查規格偏移。
CI／建置能力跟得上新增的工作量。
人工審查保留給法律、風險容忍度和信任邊界等決策。

失敗的原因不是「AI 不會寫程式」，而是程式碼產量超過驗證能力。如果 PR 週期沒有縮短，驗證成為新瓶頸建議拆解整個流程：問題可能是代理程式工作量壓垮 CI／建置基礎設施，而非 AI 採用率低。

3. 實證驗證器：只要現實能快速回饋，自動化就能奏效#

LLM 驅動的漏洞研究是更凌亂、但同樣重要的案例。代理程式並非在證明定理，而是在搜尋程式碼、提出漏洞假設、執行程式、除錯、產生 PoC，並提供重現步驟。其支架很簡單：隔離容器、專案原始碼、段落式提示、各自聚焦不同檔案的平行代理程式，以及負責篩選嚴重程度的最終驗證代理程式。

此處的驗證品質不是數學上的可靠性，而是實證確認：

代理程式能否重現當機、利用漏洞或控制流程劫持？
它能否產生 PoC 和其他審查者可執行的步驟？
驗證流程能否把重大發現和無用結果區分開來？
工作流程能否在人工被大量結果淹沒之前，先篩除小問題？

該文的證據支持兩方面的觀察。這套支架找到了重大漏洞，包括 RCE；Mythos Preview 更從發現漏洞進展到串接可行的攻擊利用。但檔案排序、重現、最終驗證、嚴重程度審查、防護措施和受控發布的必要性，本身就說明了核心問題：在高風險領域，驗證品質決定自動化究竟是防禦上的助力，還是無法審查的危險輸出。

與 Lean 相比，漏洞研究的驗證較弱，但比模糊的判斷任務更貼近可執行的現實。因此它位於中間：自動化可以奏效，但只有在支架強制產生可重新執行、可檢查的具體產物時才行。

3b. 完全沒有可執行驗證器：以結構和同儕比較作為替代方案（新增於 2026-09-23）#

第三階假設代理程式可以執行某些東西——重現當機、產生 PoC、重新執行產物。整類安全工作都做不到這些。Antaeus（Antaeus: Hunting Repository-Level Logic Vulnerabilities via Context-Grounded LLM Reasoning，empirical）在 C/C++ 儲存庫中搜尋存取控制和資訊暴露缺陷，並假設沒有攻擊輸入、沒有執行時追蹤，也沒有執行環境——漏洞是缺少防護，而缺少的東西無從重現。這是理解階梯的有趣案例，因為它展示了在第三階的實證檢查不可用、而第四階的「維持輔助」又不能接受時，系統會如何設計。

有兩種替代方案，但兩者都不是第三階意義上的驗證器：

把結構化輸出結構當成主張依據工具。 模型不能只給出判定；它必須指出對安全性敏感的接收點、列舉該接收點所需的安全條件、將每項條件標記為 locally_satisfied 是 true 或 false，並附上以程式碼為依據的說明。只有判斷及其支持證據都正確，發現才會被接受，因此理由不一致的正確標籤會被丟棄。這是在沒有可靠性的情況下，換得可採取行動性和審查篩選：沒有人驗證該條件是否成立，但審查者會獲知該檢查哪個述詞，不必從頭推導二元判決。
在同一語料庫內進行同儕比較，替代真值。 只有當被標記的條件相較於同一儲存庫中結構相似的接收點具有獨特性時，才會保留；若同一未滿足條件普遍重現，則予以刪除——其依據是普遍性代表專案慣例，而非錯誤。接收點識別碼以 UniXcoder 嵌入，條件文字則以 sentence-transformer 嵌入，門檻值按儲存庫校準。它不增加模型成本，就能移除 25–27% 的誤報，同時不漏掉任何真陽性。

結果正如階梯對沒有可靠拒絕機制的一階所預測：自動化能奏效，而且靠的是產量而非信任。 在 1,732 項發現中，偵測並說明 35 個已知 CVE 中的 20 個——約每 87 項發現才有一個確認的錯誤。對比第一階：Lean 不會接受任何錯誤證明。此處則完全沒有根據真偽來拒絕，只根據典型性篩選，因此人類審查者仍要全程參與，系統的貢獻在於將 186,859 個函式縮減到 6,112 個，並為每個標記附上論證。

因此這一階的規則是：驗證器無法存在時，就改以可採取行動性和篩選能力取代可靠性，並明確計算剩餘的人力注意力成本。 這種設計不會提高自主性，而是降低自主性原本仍得仰賴的審查成本；在第三階以下，這是唯一可行的做法。

4. 嘈雜的驗證器：自動化仍應維持輔助角色#

可驗證性論點承認，幾乎任何事物多少都能被驗證，甚至可透過 LLM 評審團驗證軟性領域。但「多少」還不足以支撐完全委派。嘈雜的驗證器或許能改善排序、分類或草擬，卻無法承擔 Lean 所能承擔的自主性負荷。

分界就在這裡：驗證器無法可靠地拒絕不良輸出時，自動化就必須更接近人類判斷，否則系統只會大量擴增看似合理的錯誤。

驗證品質何時是決定因素#

有四個條件成立時，驗證品質就會成為決定因素：

生成充足。 代理程式能以低成本產生許多候選修補、證明、漏洞利用、報告或計畫。驗證成為新瓶頸、AI 驅動的形式化證明搜尋和LLM 驅動的漏洞研究都符合這項條件。
輸出有外部正確性標準。 證明要麼通過型別檢查，測試要麼通過，漏洞利用要麼能重現，修補要麼能維持行為。目標不是品味。
不良輸出代價高昂。 錯誤證明會浪費專家注意力；不良程式碼會增加維護成本；未經驗證的漏洞輸出會帶來安全風險或揭露工作超載。
回饋能進入迴圈。 驗證器必須提供代理程式能採取行動的訊號，而不能只給出延遲的人類判決。

四項條件全部成立時，改善驗證器通常比改善提示更重要。代理程式迴圈會變成：生成、檢查、從檢查中學習、重複。檢查可靠時，迴圈會逐步累積效益；檢查薄弱時，迴圈只會不斷累積雜訊。

驗證品質的構成#

來源指出五個面向：

可靠性： 接受是否代表產物確實有效？Lean是此處的最高標準。
涵蓋範圍： 驗證器是否檢查了任務中真正重要的部分？測試和 CI 有用但不完整；mathlib 的成熟度也會限制形式化證明搜尋。
可採取行動性： 失敗訊號是否能引導下一次嘗試？Lean 編譯器錯誤能做到；含糊的人類審查往往不能。
延遲和成本： 驗證能否在代理程式迴圈中執行？若速度太慢或成本太高，就會變成最後稽核，而非搜尋的基本工具。
審查篩選： 驗證器是否能將人工工作縮減到值得審查的輸出？AI 驅動的形式化證明搜尋明確將形式化驗證視為篩選工具，用來判斷哪些證明值得人工審查；LLM 驅動的漏洞研究則透過驗證來篩選發現。

結論#

當驗證器夠好，能將模型輸出轉化為可可靠拒絕錯誤的搜尋空間時，AI 自動化就能奏效。Lean 展現理想情況：驗證器可靠、局部、低成本且可放進迴圈，因此簡單的代理程式迴圈就能超越客製化機制。軟體工程展現實務上的中間地帶：測試、CI、規格和審查能讓自動化派上用場，但程式碼產量增加時，驗證基礎設施便成為瓶頸。漏洞研究展現危險的中間地帶：實證重現和驗證能讓自動化產生效益，但驗證薄弱時，規模擴大也會帶來風險。

規則很簡單：自主程度只提升到驗證器所能支援的層級。 低於這條界線，就把模型當作助理；到達這條界線，就把它當作搜尋流程；高於這條界線，系統承重的核心便是驗證器，而非模型。