1.8 億行數學證明：當 AI 開始檢查 AI 寫的程式

前言：一個 QA gate 的日常

我每天的工作裡有一個固執的習慣：任何 pipeline 產出的 artifact，都必須帶著自己的驗證證據。文件解析出來的欄位，要有溯源紀錄。轉換過的資料，要附比對報告。任何一個數字被質疑的時候，證據要能自己說話。

同事問過我為什麼這麼麻煩。我的回答是：因為我選擇相信的東西很少。

所以當我看到 Anthropic 那則新聞的時候，反應不是驚訝，而是一種奇怪的親切感。好像有人把我的小習慣，推到了一個極端規模。

1.8 億行證明，潛伏十年的 bug

Anthropic 跟 Theorem 公司合作，讓 Claude 對 123 個開源函式庫做了一件工程界很少認真做的事：形式化驗證。

他們產出了約 1.8 億行 Rocq 證明代碼。Rocq 就是 Coq 改名之後的形式驗證語言，跟 Lean 4 是同一個賽道的競品。驗證目標很具體：在 RISC-V、Linux 這些執行環境下，用數學證明「小於 64 MB 的輸入，不會觸發特定的崩潰或記憶體安全錯誤」。

過程中挖出了數百個 bug。有些潛伏超過十年。

十年。一個 bug 在 production 裡活了十年，度過了無數次 code review、無數輪的回歸測試、無數個自信滿滿的「這個功能很穩」。

傳統測試是抽樣。你丟一千個輸入進去，沒爆，你說它穩。形式化驗證是全量：在定義好的條件範圍內，數學上證明不存在會讓它崩潰的輸入。

一句話是「目前還沒發現問題」。另一句話是「問題在數學上不存在」。這兩句話之間的距離，就是測試與證明的距離。

程式碼與證明

為什麼這件事現在才發生

形式化驗證不是新東西。Coq 快四十歲了。Thales 用它驗證過航空軟體，AWS 用 TLA+ 驗證過 S3 的核心服務。

變的不是技術，是成本結構。

以前寫一個形式化證明，貴到只有航天、晶片、密碼學這種「錯一次就死」的產業用得起。因為人類寫證明太慢：一行的程式碼，可能需要十行的證明，還要專家反覆調整。手工藝的產能，撐不起軟體的需求。

AI 把這個成本砍掉了。Claude 一口氣生成 1.8 億行證明，這件事在兩年前是幻想。人類寫證明是手工藝，AI 寫證明是製造業。製造業的單位成本，決定了誰能用得起這個技術。

Lean 4：數學家的賭桌

同一波浪潮，純數學那邊玩的是 Lean 4。

Terence Tao，當代最有影響力的數學家之一，把 Lean 形式化當成日常工具在推。DeepMind 的 AlphaProof 用 Lean 拿到了 IMO 銀牌等級的成績。Mathlib 社群函式庫累積超過一百五十萬行，由全球數學家共同維護，規模還在加速。

數學家在做的事情，本質上跟 Anthropic 一樣：把「我相信這個定理是對的」，換成「這個定理的證明通過了編譯器」。

數學證明

數學界幾百年的 peer review 信任機制，正在被機器可驗證的證明補充。不是取代。人類數學家負責直覺與方向，證明助手負責一步一步的嚴謹。這個分工，跟我們軟體工程的分工演化，方向是一樣的。

瓶頸的轉移

哈佛有一個研究，數據很扎心。

AI coding 普及之後，開源專案的 PR 數量增加了 23%，代碼行數增加了 30%，但真正 merge 出街的 feature 沒有顯著增加。更扎心的是，PR 的平均處理時間增加了 49%。

翻譯成白話：AI 讓寫代碼變快了，同時讓「檢查代碼」變成新的瓶頸。人類 reviewer 成了整條生產線上最慢的那台機器，而且這台機器還在積壓。

這就是形式化驗證的時代意義。當生成的成本趨近於零，驗證的成本決定一切。誰能把驗證自動化，誰就把整條產線的最大瓶頸拆掉了。

我不是形式化驗證專家

先把這一點說清楚。我的正職工作裡沒有一行 Lean，也沒有一行 Rocq。

但我做的東西，是同一個哲學的微縮版。我管的那條 AI 文件管線，每天處理兩百多份表單。每一份的解析結果都帶著自己的驗證證據：欄位有溯源，轉換有比對，任何一個輸出被質疑的時候，證據要能自己說話，而不是靠我口頭保證。

這不是形式化驗證。這是一個工程師被現實教育之後的信仰：驗證證據，優先於任何人的保證。

形式化驗證把這個信仰推到了數學的極端。而它突然變得便宜，意味著這個信仰可以從個人習慣，升級成團隊標準。

更難的問題還在後面

形式化驗證驗證的是程式行為。但 AI 帶來的問題，不只程式行為。

我前陣子做完一份 AI 安全研究，主題是多個 AI agent 在缺乏人類監督時，如何發展出人類難以察覺的協調模式。研究裡最讓我在意的發現是：AI 之間的合謀不需要它們有合謀的意圖，行為模式本身就能形成人類無法有效審查的協調。

程式可以形式化，因為程式有明確的語義。但一個 AI agent 在十萬次決策中形成的隱性行為模式，要怎麼證明它沒問題？

這是我目前為止覺得最有趣、也最困難的問題。Anthropic 在證明程式不崩潰，而整個 AI 安全社群在試圖證明一個更模糊的命題：AI 的行為是可控的、可解釋的、可信任的。前者已經有 1.8 億行的示範，後者連數學語言都還在發明。

寫在最後

工程師的技能清單正在改寫。

以前的核心技能是寫出能用的代碼。後來變成寫出能維護的代碼。我看這波浪潮之後，下一個核心技能會是：寫出能被驗證的代碼，以及，寫出難以被欺騙的驗證。

測試告訴你問題在哪裡，證明告訴你問題不在哪裡。前者靠人力維持，後者靠數學保證。

當寫代碼的成本歸零，信任就會成為最貴的資產。而數學，是這個世界上唯一能量產信任的工廠。

如果你也在思考 AI 時代的工程實踐，或在做類似的 AI 安全研究，歡迎寫信交流：partner@calpa.me。也可以到我的 GitHub 看看最近的開源實驗。