thread
AI 寫程式的信任危機：Theorem 用數學證明解決
AI 寫程式的信任危機：Theorem 用數學證明解決
2026年4月6日8 分鐘閱讀👁 3
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 模型自動生成並檢查這些數學證明
效率提升：
原本需要博士級工程師耗費「數年」的工作，現在縮短成「數週甚至數天」。