AI 寫程式的信任危機：Theorem 用數學證明解決

作者: @meow.coder
來源: Threads
觀看數: 1.3K
日期: 2026-03-03
標籤: #AI #形式化驗證 #FormalVerification #Theorem #程式碼安全 #軟體工程 #數學證明

---

TL;DR（極簡版）

• 🚨 問題：AI 每年生成數十億行程式碼，但誰來確認這些程式碼真的沒問題？
• 💰 新創：美國 Theorem 完成 600 萬美元融資
• 🔬 解法：用 AI 自動生成「數學證明」來驗證程式碼（形式化驗證 + AI）
• ⚡ 效率：原本需要博士級工程師耗費「數年」→ 縮短成「數週甚至數天」
• 🎯 核心技術：fractional proof decomposition（按比例分配驗證資源）
• 📊 實際案例：1,500 頁 PDF 規格書 → 16,000 行程式碼，無人工審查直接上線
• ⚠️ 創辦人警告：AI 超越人類軟體工程能力無法避免，需要更先進的驗證手段

---

核心問題：AI 寫程式的信任危機

問題規模

AI 每年生成數十億行程式碼，但誰來確認這些程式碼真的沒問題？

監管缺口：

• AI 寫程式的速度狂奔
• 驗證速度卻像牛步
• 如果有人叫你審查 6 萬行程式碼，根本無從下手

不只是工程問題：

• 金融系統
• 電網
• 等關鍵基礎設施的重大威脅

---

Theorem：用數學證明解決信任問題

公司資訊

• 名稱：Theorem
• 融資：600 萬美元（最新一輪）
• 創辦人：Jason Gross
• 總部：美國

核心技術

形式化驗證（Formal Verification）+ AI：

• 形式化驗證：一種數學技術，能證明軟體行為完全符合規範
• Theorem 用 AI 模型自動生成並檢查這些數學證明

效率提升：

原本需要博士級工程師耗費「數年」的工作，現在縮短成「數週甚至數天」。

---

形式化驗證的歷史與成本

傳統成本極高

成本比例：

• 每 1 行程式碼需要 8 行數學證明
• 只用在航空電子、核反應爐這種絕對不能出錯的領域

經典案例：

MIT 博士曾花 15 人年驗證 HTTPS 協議，可見傳統做法多昂貴。

應用限制：

• 成本太高，只用在最關鍵的領域
• 大部分軟體都無法負擔
• 需要博士級專家

---

Theorem 的核心技術：fractional proof decomposition

技術原理

簡單說：AI 不要全面測試每個行為，而是依據組件重要性，按比例分配驗證資源。

關鍵優勢：

1. 效率提升：不需要全面驗證每一行程式碼
2. 資源最佳化：重要組件分配更多驗證資源
3. 突破限制：能處理跨檔案的複雜程式碼（突破「上下文窗口」限制）

---

實際成果

1. 抓到傳統測試沒發現的 Bug

在大型 AI 系統中抓到傳統測試沒發現的 Bug

---

2. SFBench 展示

成果：

• 1,276 個數學問題從 Rocq 翻譯成 Lean 語言
• 自動證明等效
• 人類團隊至少需要 2.7 人年

意義：

• 自動化程度極高
• 人類需要 2.7 人年的工作 → Theorem 可能只需數週

---

3. 突破上下文窗口限制

Theorem 的架構能處理跨檔案的複雜程式碼，突破了「上下文窗口」限制——這是大多數 AI 程式碼工具的痛點。

為什麼重要？

• 傳統 AI 工具（Copilot、Cursor）受限於上下文窗口（128K、200K tokens）
• 大型專案往往跨越數百個檔案、數萬行程式碼
• Theorem 能處理這種規模的專案

---

實際案例：1,500 頁 PDF → 16,000 行程式碼

客戶需求

背景：

• 1,500 頁的 PDF 規格書
• 一套充滿記憶體洩漏、崩潰、隱性 Bug 的舊系統
• 目標：效能從 10 Mbps 提升到 1 Gbps（100 倍）
• 而且不能出錯

---

Theorem 的解決方案

成果：

• AI 生成了 16,000 行正式程式碼
• 客戶「完全沒有人工審查」就直接部署上線

為什麼敢這麼做？

因為透過數學驗證，新程式碼與規格書的目標行為完全一致。幾百行程式碼就概括了 1,500 頁的內容。

這就是數學證明的威力。

---

關鍵洞察

1. 信任來自數學證明，不是人工審查
2. 效率提升：1,500 頁 → 幾百行數學證明 → 16,000 行程式碼
3. 零風險部署：無人工審查直接上線
4. 性能提升 100 倍：10 Mbps → 1 Gbps

---

創辦人 Jason Gross 的警告

不對稱防禦

當 AI 讓駭客攻擊成本大幅下降，防禦者需要明白「不對稱防禦」——防禦能力擴展不需要同等比例資源。

什麼是不對稱防禦？

• 攻擊者：用 AI 生成大量攻擊
• 防禦者：用數學證明一次性確保安全
• 不需要對每個攻擊逐一防禦

---

AI 超越人類無法避免

他警告：如果 AI 以指數級速度進步，某天超越人類的軟體工程能力將「無法避免」。

如果人類沒準備好：

• ❌ 沒有更先進的驗證手段
• ❌ 沒有改變監管方式
• ❌ 最終只會打造出連自己都無法控制的系統

---

第一波 vs 第二波

第一波 AI 程式輔助：

• 帶來生產力提升（Copilot、Cursor、Claude Code）
• 但缺乏驗證機制

第二波（Theorem 押注）：

用數學證明確保速度提升不以犧牲安全為代價。

---

技術深度解析

形式化驗證 vs 傳統測試

項目	傳統測試	形式化驗證
方法	執行測試案例	數學證明
覆蓋率	部分路徑	所有可能路徑
保證	無法保證	數學保證
成本	低	極高（傳統）
適用	一般軟體	關鍵系統
AI 加速	有限	Theorem 突破

---

Rocq vs Lean

Rocq（前身為 Coq）：

• 法國開發的證明助手
• 用於形式化驗證

Lean：

• 微軟研究院開發
• 更現代、更易用的證明語言

SFBench 展示：

• 1,276 個數學問題從 Rocq 翻譯成 Lean
• 自動證明等效
• 證明 Theorem 的跨語言能力

---

上下文窗口問題

傳統 AI 工具限制：

• Claude：200K tokens
• GPT-4：128K tokens
• Gemini：1M tokens

大型專案挑戰：

• 數百個檔案
• 數萬行程式碼
• 複雜的依賴關係

Theorem 突破：

• fractional proof decomposition
• 能處理跨檔案的複雜程式碼
• 不受上下文窗口限制

---

網友質疑（技術討論）

mazdashie 的質疑

生成的證明有 1% 是錯的會產生連鎖效應，這 1% 的錯誤放大到程式上面至少變成 10% 錯誤。

這是合理的技術討論：

• 如果數學證明本身有錯
• 會導致程式碼錯誤被放大

Theorem 的回應可能包括：

• 多層驗證機制
• 證明的證明（meta-verification）
• 人類專家最終審查（對關鍵部分）

---

應用場景

適合 Theorem 的領域

1. 金融系統

   • 交易邏輯
   • 風控系統
   • 清算系統

2. 關鍵基礎設施

   • 電網控制
   • 交通管理
   • 通訊協議

3. 航空航天

   • 飛控系統
   • 導航系統
   • 安全關鍵軟體

4. 醫療設備

   • 植入式裝置
   • 手術機器人
   • 診斷系統

5. 加密貨幣 / 區塊鏈

   • 智能合約
   • 共識協議
   • 錢包安全

---

不適合的領域

1. 快速迭代的產品

   • 驗證成本 > 驗證價值
   • 更適合傳統測試

2. 非關鍵應用

   • 簡單的 CRUD 應用
   • 內部工具

3. 用戶體驗驅動

   • UI/UX 設計
   • 需要快速反饋

---

商業模式（推測）

可能的定價策略

1. 按專案收費

   • 類似案例：1,500 頁 PDF → 16,000 行程式碼
   • 可能收費：$100,000 - $500,000

2. 訂閱制

   • 企業年費：$50,000 - $200,000
   • 根據程式碼規模與複雜度

3. API 調用

   • 按驗證次數收費
   • 類似 AI API 定價模式

---

目標客戶

1. 大型企業

   • 金融機構（銀行、證券、保險）
   • 科技巨頭（Google、Microsoft、Amazon）
   • 航空航天（Boeing、Airbus、SpaceX）

2. 政府機構

   • 國防部門
   • 關鍵基礎設施營運商

3. 監管要求嚴格的產業

   • 醫療設備製造商
   • 核能營運商

---

競爭對手與市場定位

潛在競爭對手

1. 傳統形式化驗證公司

   • AdaCore（航空航天）
   • Galois（國防、安全）
   • TrustInSoft（C/C++ 驗證）

2. AI 程式碼工具

   • GitHub Copilot
   • Cursor
   • Claude Code
   • （但這些缺乏驗證機制）

3. 測試自動化工具

   • Selenium
   • Appium
   • （但無法提供數學保證）

---

Theorem 的獨特定位

交叉點：

• 形式化驗證的數學保證
• AI 的效率與可擴展性
• 實際商業應用（不只是研究）

護城河：

1. 技術難度極高（需要博士級專家）
2. fractional proof decomposition 專利技術（可能）
3. 實際案例累積（16,000 行無人工審查上線）

---

產業影響

軟體工程典範轉移

過去：

• 寫程式碼 → 測試 → 部署
• 依賴人工審查
• 無法保證正確性

未來（Theorem 願景）：

• 寫規格書 → AI 生成程式碼 + 數學證明 → 直接部署
• 無需人工審查
• 數學保證正確性

---

對開發者的影響

技能需求轉變：

1. 減少：手寫大量程式碼
2. 增加：撰寫精確的規格書
3. 新技能：理解形式化驗證、數學證明

工作流程改變：

• 從「寫程式碼」→「寫規格書」
• 從「測試」→「驗證」
• 從「人工審查」→「數學證明」

---

對監管的影響

Jason Gross 警告：

如果 AI 以指數級速度進步，某天超越人類的軟體工程能力將「無法避免」。人類如果沒準備好更先進的驗證手段，也沒改變監管方式，最終只會打造出連自己都無法控制的系統。

監管需要跟上：

1. 要求形式化驗證（對關鍵系統）
2. 建立驗證標準
3. 培養驗證專家

---

關鍵教訓

1. AI 生成程式碼的信任問題無法迴避

現狀：

• AI 每年生成數十億行程式碼
• 驗證速度遠遠跟不上

後果：

• 金融系統、電網等關鍵基礎設施的重大威脅

💡 教訓：監管缺口需要填補。

---

2. 數學證明 > 人工審查

Theorem 案例：

• 16,000 行程式碼無人工審查直接上線
• 因為數學證明提供絕對保證

💡 教訓：信任來自數學，不是人類。

---

3. 形式化驗證成本大幅降低

過去：

• MIT 博士 15 人年驗證 HTTPS
• 每 1 行程式碼需 8 行數學證明

現在（Theorem）：

• 數年 → 數週甚至數天
• AI 自動生成並檢查證明

💡 教訓：AI 讓形式化驗證從「奢侈品」變「必需品」。

---

4. 不對稱防禦是關鍵

攻防不對稱：

• 攻擊者：AI 生成大量攻擊（成本低）
• 防禦者：數學證明一次性確保安全（成本高，但有效）

💡 教訓：防禦能力擴展不需要同等比例資源。

---

5. AI 超越人類無法避免

Jason Gross 警告：

• AI 以指數級速度進步
• 某天超越人類軟體工程能力無法避免

人類需要準備：

• 更先進的驗證手段
• 改變監管方式
• 否則無法控制自己打造的系統

💡 教訓：技術進步需要配套的驗證與監管。

---

總結

核心問題：

AI 每年生成數十億行程式碼，但誰來確認這些程式碼真的沒問題？

Theorem 的解法：

• 形式化驗證 + AI
• fractional proof decomposition
• 數學證明取代人工審查

實際成果：

• 1,500 頁 PDF → 16,000 行程式碼，無人工審查直接上線
• 效能提升 100 倍（10 Mbps → 1 Gbps）
• 傳統需數年 → 現在數週甚至數天

創辦人警告：

• AI 超越人類軟體工程能力無法避免
• 需要更先進的驗證手段與監管方式
• 否則最終打造出無法控制的系統

第二波 AI 程式：

用數學證明確保速度提升不以犧牲安全為代價。

---

你覺得這個方向對嗎？ 🤔

---

下一步行動：

1. 關注 Theorem 的發展
2. 了解形式化驗證基礎知識
3. 思考自己的專案是否需要更嚴格的驗證
4. 準備迎接「寫規格書」時代

---

#AI #形式化驗證 #FormalVerification #Theorem #程式碼安全 #軟體工程 #數學證明 #JasonGross #不對稱防禦