--- title: "Vitalik Buterin 表示，人工智能形式驗證可能有助於防止在以太坊生態系統中發生數百萬美元的加密貨幣黑客攻擊" type: "News" locale: "zh-HK" url: "https://longbridge.com/zh-HK/news/287031704.md" description: "以太坊聯合創始人維塔利克·布特林提倡使用人工智能輔助的形式驗證，以增強加密生態系統的安全性，認為這可以幫助開發者在發佈前證明軟件的安全性。在網絡攻擊日益增加的背景下，包括最近的一起 7600 萬美元的黑客事件，布特林強調人工智能可以消除編碼缺陷。他承認形式驗證的侷限性，但相信它可以顯著提高安全性，尤其是在複雜系統中。多個以太坊項目已經在測試這種方法，旨在實現一個未來，代碼能夠附帶機器可檢查的正確性證明" datetime: "2026-05-20T08:30:40.000Z" locales: - [zh-CN](https://longbridge.com/zh-CN/news/287031704.md) - [en](https://longbridge.com/en/news/287031704.md) - [zh-HK](https://longbridge.com/zh-HK/news/287031704.md) --- # Vitalik Buterin 表示，人工智能形式驗證可能有助於防止在以太坊生態系統中發生數百萬美元的加密貨幣黑客攻擊 以太坊聯合創始人維塔利克·布特林認為，雖然人們擔心人工智能系統會加速網絡攻擊，但這些系統最終可能成為加密貨幣最強大的安全工具之一。 隨着黑客不斷從脆弱的區塊鏈平台中竊取數百萬美元，布特林正在推動一個未來，在這個未來中，人工智能幫助開發者在軟件上線之前數學證明其安全性。 他的論點是在加密行業面臨越來越大的壓力之際，最近包括從 Echo Protocol 的跨鏈橋中盜取超過 7600 萬美元，以及針對 THORChain 和 Verus-Ethereum Bridge 的攻擊。 ## 人工智能能否阻止下一個加密攻擊 布特林認為，與其將人工智能視為威脅，不如將其視為消除持續困擾加密基礎設施的許多編碼缺陷的工具。 他的重點是 “形式驗證”，這是一種將軟件與數學證明相結合的方法，以確認代碼的行為完全符合預期。  維塔利克·布特林認為，人工智能可能成為加密貨幣最大的安全升級之一。   根據他的説法，人工智能輔助的形式驗證可能幫助以太坊和其他區塊鏈基礎設施在黑客能夠利用漏洞之前檢測到這些漏洞。   隨着行業的發展，越來越智能…… pic.twitter.com/sSAWRnpaig   — 𝗔𝗹𝗶𝗸𝗼-𝗱𝗮𝗻𝗴𝗼𝘁𝗲 (@alikodangote9) 2026 年 5 月 19 日 雖然這一概念已經存在了幾十年，但對於大多數開發者來説，使用它仍然過於困難和耗時。 根據布特林的説法，人工智能最終可能使這一過程變得切實可行。 開發者不再需要手動逐行編寫證明，而是可以越來越多地依賴人工智能系統來生成軟件及其伴隨的數學檢查。 然後，人類將驗證最終的證明是否確實反映了系統的預期行為。  許多人聲稱，藉助人工智能輔助的漏洞發現，安全代碼（因此無信任的任何東西）將變得不可能。   我持有更樂觀的看法，人工智能輔助的形式驗證是原因之一：https://t.co/0ceMBZ6uqj   — vitalik.eth (@VitalikButerin) 2026 年 5 月 18 日 布特林寫道， “如果你進行端到端的形式驗證，那麼你不僅是在理論上證明某個協議的描述是安全的，而是在實踐中證明用户運行的特定代碼是安全的。” 他補充説，用户將不再需要自己審計大量代碼，並表示， “你只需檢查關於它的證明聲明。” ## 以太坊項目已在測試人工智能驗證 布特林指出，幾個與以太坊相關的項目已經在嘗試這種方法。 一個例子是 Arklib，它試圖創建一個完全形式驗證的 STARK 實現。 另一個是 evm-asm，一個在低級 RISC-V 彙編中構建以太坊虛擬機的項目，同時對其進行數學檢查，以確保其與可讀的參考版本一致。 他還表示，更新的人工智能系統在證明生成方面已經證明了其價值。 根據布特林的説法，Claude 和 DeepSeek 4 Pro 在編寫 Lean 證明時表現良好，而 Leanstral，一個較小的專用模型，可以在本地運行，並在形式驗證任務上超越更大的通用人工智能系統。 這位以太坊聯合創始人將該模型描述為可能的 “軟件開發最終形態”，在這種形態中，高度優化的代碼與可機器檢查的正確性證明一起交付。 ## 為什麼布特林仍然不完全信任人工智能 儘管他持樂觀態度，布特林反覆警告説，形式驗證並不是解決網絡安全問題的完整答案。 他強調了之前涉及經過驗證的編譯器、不完整證明的失敗，以及開發者數學證明錯誤的情況，因為規範本身未能反映預期行為。 他寫道， “形式驗證並不是靈丹妙藥。” 他認為，當所需結果比所構建軟件的複雜性更簡單時，該方法效果最佳。  人們説人工智能使安全代碼變得不可能   維塔利克不同意，我也不同意。   這是我從他關於形式驗證的新帖子中學到的：   \\ 人工智能編寫代碼（甚至是原始彙編）   \\Lean 編寫代碼正確的證明   \\ 計算機自動驗證證明   … https://t.co/nw0T2id727pic.twitter.com/uP6U3kHFHn   — Rohit Purkait (@codeswithroh) 2026 年 5 月 18 日 他特別指出，量子抗性簽名、STARKs、共識算法和 ZK-EVMs 是形式驗證可能特別有價值的領域。 布特林表示， “價值增加的一個重要部分是證明確實是端到端的。通常，最棘手的錯誤是交互錯誤，發生在兩個被單獨考慮的子系統的邊緣。” 他還拒絕了對日益先進的人工智能網絡攻擊可能最終使開源系統無法安全的擔憂。 他寫道， “整個密碼朋克精神基本上是基於這樣一個理念：在互聯網上，防禦者具有優勢。” ## 加密黑客對以太坊安全施加壓力 這一討論出現在行業網絡安全最困難的時期之一。 Echo Protocol 最近在攻擊者突破其跨鏈橋基礎設施後損失超過 7600 萬美元。 早期的攻擊針對 THORChain，損失超過 1000 萬美元，而 Verus-Ethereum Bridge 的攻擊導致又有 1158 萬美元的資金被盜，因為黑客利用了缺失的驗證檢查。 布特林建議，這些失敗中的一些可能通過更強的基於證明的驗證系統來避免。 隨着人工智能模型在發現軟件漏洞方面的能力提高，整體威脅環境也變得更加嚴峻。 據報道，Anthropic 限制了其以網絡安全為重點的 Claude Mythos 模型的訪問權限，因為內部測試顯示該系統能夠自主識別並利用漏洞，其能力遠超早期的公共 AI 系統。 研究人員還聲稱，該模型在測試中識別出了 Mozilla Firefox 的 271 個漏洞，而其他報告則將 AI 輔助研究與涉及 Apple M5 芯片保護的漏洞聯繫在一起。 與此同時，英國 AI 安全研究所的安全研究人員據報道發現，OpenAI 的 GPT-5.5 展現出越來越先進的攻擊性網絡能力。 Buterin 寫道， > “計算機代碼中的漏洞令人恐懼。” ## Buterin 的私人 AI 設置內部 在對 AI 安全風險的警告之外，Buterin 還透露了他完全在自己硬件上運行的個人 AI 系統的細節。 他通過 llama-server 在一台配備 Nvidia 5090 GPU 的筆記本電腦上運行一個開源的 Qwen3.5:35B 模型。 根據 Buterin 的説法，該系統每秒生成大約 90 個標記，足夠快速以供日常使用，而無需過多依賴雲服務。 > 更新：我切換到了 llama-swap，現在 35B 的運行速度為每秒 90 個標記。 > > — vitalik.eth (@VitalikButerin) 2026 年 3 月 9 日 他的設置包括本地存儲的維基百科和技術文檔副本，以減少互聯網搜索，他認為這是一種隱私風險，因為它們暴露了用户行為。 Buterin 還將 AI 系統連接到他的以太坊錢包和消息賬户，但設定了嚴格的限制。 他開發了一種工具，允許 AI 閲讀 Signal 消息和電子郵件，但任何外發消息或高風險操作都需要手動批准。 > Vitalik Buterin 表示，AI 應該在個人設備上本地運行，而不是在雲端。 > > • 雲 AI 創建了單點故障和監控 > > • 本地模型保護隱私和用户主權 > > • 加密 + 本地 AI = 可驗證的、抗審查的計算 > > 當… pic.twitter.com/no1QMVvXZA > > — THE BLOCKOPEDIA (@theblockopedia\_) 2026 年 4 月 3 日 他説，同樣的邏輯也應該適用於連接到 AI 系統的加密錢包。 任何自主 AI 支出應限制在每天 100 美元，而較大交易應要求人工確認。 這種方法與他保護自己加密貨幣資產的方式相似。 據報道，他約 90% 的資金存儲在一個多簽名安全錢包中，由多個受信方控制訪問，而不是單個個人。 > Vitalik Buterin 不使用冷錢包來保護自己的個人加密貨幣。 > > 這是他保持加密貨幣安全的方法： > > 以太坊創始人 Vitalik Buterin 揭示他將 90% 的加密資金存儲在一個多簽名安全錢包中。 > > "M-of-N，一些密鑰由你持有（但不足以… pic.twitter.com/CTx5tuP87k > > — Talha (@talhaasiiif) 2024 年 5 月 7 日 在研究人員發現與 OpenClaw 相關的約 15% 的第三方工具 allegedly 包含隱藏的惡意指令，悄悄將用户數據傳輸到外部服務器後，Buterin 的擔憂加劇。 Buterin 警告説，儘管端到端加密和本地運行的軟件終於開始獲得主流採用，但基於雲的 AI 服務有可能逆轉這一進展。 ### 相關股票 - [COIN.US](https://longbridge.com/zh-HK/quote/COIN.US.md) - [ETHE.US](https://longbridge.com/zh-HK/quote/ETHE.US.md) - [GBTC.US](https://longbridge.com/zh-HK/quote/GBTC.US.md) - [BLCN.US](https://longbridge.com/zh-HK/quote/BLCN.US.md) - [ARKB.US](https://longbridge.com/zh-HK/quote/ARKB.US.md) - [BTCO.US](https://longbridge.com/zh-HK/quote/BTCO.US.md) - [BRRR.US](https://longbridge.com/zh-HK/quote/BRRR.US.md) - [ETHHKD.VAHK](https://longbridge.com/zh-HK/quote/ETHHKD.VAHK.md) - [ETHUSD.VAHK](https://longbridge.com/zh-HK/quote/ETHUSD.VAHK.md) ## 相關資訊與研究 - [MaiCoin 集團攜手必勝客歡慶比特幣比薩日 線上線下同步送好康](https://longbridge.com/zh-HK/news/287023156.md) - [通膨疑慮、殖利率上升壓抑風險資產 比特幣挫](https://longbridge.com/zh-HK/news/286860469.md) - [ETH 研發團隊集體跑路，華爾街瘋狂砍倉 ETH](https://longbridge.com/zh-HK/news/286863776.md) - [明日加密市場 所有人都將迎來全新格局](https://longbridge.com/zh-HK/news/287031763.md) - [DeFi 協議成最大贏家 ！渣打：2028 年「代幣化資產」規模將達 4 兆美元](https://longbridge.com/zh-HK/news/286875291.md)