PANews 5月28日消息，Vitalik Buterin發文分享其自主大語言模型（LLM）設置的最新進展，並指出以太坊基礎設施與AI的交集正不斷擴大。他提到Deepseek V4已發布，其2-bit量化版本可在90GB內存內運行，在蘋果硬體上速度約35 token/秒，但在AMD上僅約7 token/秒，強調真正支持多硬體廠商是區分「去中心化AI」與「CROPS AI」的關鍵。此外，Mistral推出的Leanstral模型(專注Lean程式碼編寫)在70GB內可運行，效能媲美1T參數大模型。

Vitalik也詳細闡述了正式驗證在提升程式碼安全性中的作用，認為AI輔助的正式驗證可實現程式碼的「端到端」安全證明，適用於STARK、共識演算法、EVM等核心元件。他指出，區塊鏈與ZK-SNARK提供開放可驗證性和隱私可擴展性，而AI與正式驗證的結合能在提升程式碼編寫效率的同時重建準確性，形成互補技術堆疊。 Vitalik呼籲以太坊生態應針對以太坊相關用例進行模型微調，並推動多個硬體平台的高效支援。