La empresa Mistral AI ha presentado un gran modelo de lenguaje Devstral, diseñado para su uso en el desarrollo de aplicaciones (codificación de vibras) y optimizado para la verificación formal de código. Se espera que Devstral pueda ser utilizado para crear asistentes de IA que no solo generen código, sino que también garanticen que esté libre de errores.
Devstral se ha convertido en el primer modelo abierto que soporta el lenguaje de programación Lean 4 y su conjunto de herramientas asociado para verificar pruebas matemáticas. Lean 4 ofrece capacidades para la prueba matemática de la corrección del código y su conformidad con la especificación, lo que en el contexto de la codificación de vibras permite confirmar que el código generado por el modelo de IA cumple con lo previsto.
El modelo abarca 119 mil millones de parámetros (6.5 mil millones de parámetros activados por token), considera un contexto de 256 mil tokens y se publica bajo la licencia Apache 2.0. El archivo descargable de Leanstral ocupa 121 GB y es adecuado para su uso en sistemas locales. Para la ejecución local, se pueden utilizar bibliotecas como vllm, transformers y SGLang.
Entre otras cosas, el modelo puede ser utilizado para el desarrollo de vibras en el agente abierto mistral-vibe, así como integrarse con el conjunto de herramientas Aeneas para la verificación de código en el lenguaje Rust. Se aceptan texto e imágenes como parámetros de entrada y se genera solo texto como salida. Se admite el análisis del contenido de imágenes.
Para evaluar las capacidades de los modelos de IA en términos de calidad de la verificación formal de código y redacción de pruebas matemáticas, se ha desarrollado un nuevo conjunto de pruebas llamado FLTEval. En las pruebas realizadas, el modelo Leanstral superó notablemente a los modelos abiertos existentes Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B y GLM5 744B-A40B, mostrando resultados similares a los modelos Claude Haiku 4.5 y Claude Sonnet 4.6 de la empresa Anthropic, pero quedando atrás del modelo Claude Opus 4.6. En particular, el modelo Opus alcanzó 39.6 puntos, mientras que Leanstral logró 21.9 en una pasada y 31.9 en 16 pasadas. Además, los costos de uso de Opus fueron de 1650 dólares, mientras que Leanstral costó $18 en una pasada y $290 en 16 pasadas. El modelo Haiku obtuvo 23 puntos con un gasto de $184, y el modelo Sonnet obtuvo 23.7 con un gasto de $549.
Fuente: opennet.ru
