PANews reported on May 28th that Vitalik Buterin shared the latest progress on his Autonomous Large Language Model (LLM) setup, noting the expanding intersection between Ethereum infrastructure and AI. He mentioned the release of Deepseek V4, whose 2-bit quantized version can run within 90GB of memory, achieving speeds of approximately 35 tokens/second on Apple hardware but only about 7 tokens/second on AMD. He emphasized that true support for multiple hardware vendors is key to distinguishing "decentralized AI" from "CROPS AI." Furthermore, Mistral's Leanstral model (focused on Lean code writing) can run within 70GB, achieving performance comparable to a 1TB parameter large model.

Vitalik further elaborated on the role of formal verification in enhancing code security, arguing that AI-assisted formal verification can achieve end-to-end security proofs for code, applicable to core components such as STARK, consensus algorithms, and EVM. He pointed out that blockchain and ZK-SNARK provide open verifiability and privacy scalability, while the combination of AI and formal verification can improve code writing efficiency while restoring accuracy, forming a complementary technology stack. Vitalik called on the Ethereum ecosystem to fine-tune models for Ethereum-related use cases and promote efficient support across multiple hardware platforms.