Mistral AI ha presentado Devstral, un modelo de lenguaje de gran tamaño diseñado para el desarrollo de aplicaciones (codificación Vibe) y optimizado para la verificación formal de código. Se espera que Devstral se utilice para crear asistentes de IA capaces no solo de generar código, sino también de garantizar que esté libre de errores.
Devstral se convirtió en el primer modelo de código abierto en admitir el lenguaje de programación Lean 4 y su conjunto de herramientas de verificación matemática. Lean 4 permite demostrar matemáticamente la corrección del código y su conformidad con las especificaciones, lo que, en el contexto de la codificación de vibraciones, permite confirmar que el código generado por un modelo de IA hace exactamente lo que se espera de él.
El modelo abarca 119 mil millones de parámetros (6.5 mil millones de parámetros activados por token), considera contextos de 256 000 tokens y se publica bajo la licencia Apache 2.0. El archivo descargable con Leanstral tiene un tamaño de 121 GB y es apto para su uso en sistemas locales. Las bibliotecas vllm, transformers y SGLang pueden utilizarse para la ejecución local.
Entre otras cosas, el modelo puede utilizarse para el desarrollo de la interfaz de usuario en el agente de código abierto mistral-vibe e integrarse con el kit de herramientas Aeneas para la verificación de código Rust. Acepta texto e imágenes como parámetros de entrada y produce únicamente texto como salida. Admite el análisis del contenido de las imágenes.
Para evaluar las capacidades de los modelos de IA, teniendo en cuenta la calidad de la verificación formal del código y la redacción de pruebas matemáticas, se desarrolló un nuevo conjunto de pruebas de referencia FLTEval. En las pruebas, el modelo Leanstral superó significativamente a los modelos de código abierto existentes Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B y GLM5 744B-A40B. Mostró resultados similares a los de Claude Haiku 4.5 y Claude Sonnet 4.6 de Anthropic, pero quedó por detrás del modelo Claude Opus 4.6. Específicamente, el modelo Opus obtuvo 39.6 puntos, mientras que Leanstral obtuvo 21.9 puntos en una sola pasada y 31.9 puntos en 16 pasadas. El costo de usar Opus fue de $1650, mientras que Leanstral costó $18 en una sola pasada y $290 en 16 pasadas. El Haiku obtuvo 23 puntos con un precio de 184 dólares, mientras que el Soneto obtuvo 23.7 puntos con un precio de 549 dólares.
Fuente: opennet.ru
