Según PANews, el 28 de mayo, Vitalik Buterin compartió actualizaciones sobre la configuración de su modelo de lenguaje autónomo (LLM), destacando la creciente intersección entre la infraestructura de Ethereum y la inteligencia artificial. Señaló que la versión cuantizada de 2 bits de Deepseek V4 funciona con 90GB de memoria aproximadamente a 35 tokens por segundo en hardware de Apple, pero solo a 7 tokens por segundo en AMD, subrayando que el soporte para múltiples proveedores de hardware es clave para diferenciar la “IA descentralizada” de “CROPS AI”. El modelo Leanstral de Mistral, centrado en la escritura de código Lean, también se ejecuta en 70GB con un rendimiento comparable al de modelos de 1 billón de parámetros.
Vitalik profundizó en el papel de la verificación formal para mejorar la seguridad del código, proponiendo que la verificación formal asistida por IA habilita pruebas de seguridad “de extremo a extremo” aplicables a STARKs, algoritmos de consenso y componentes de EVM. Destacó que blockchain y los ZK-SNARKs aportan verificabilidad abierta y escalabilidad de la privacidad, mientras que la IA combinada con verificación formal mejora la eficiencia del código a la vez que restaura la precisión, formando un stack tecnológico complementario.