A empresa Mistral AI apresentou um grande modelo de linguagem chamado Devstral, voltado para o desenvolvimento de aplicativos (vibe-coding) e otimizado para verificação formal de código. Assume-se que o Devstral pode ser utilizado para criar assistentes de IA que não apenas geram código, mas também garantem a ausência de erros nele.
Devstral se tornou o primeiro modelo open-source a suportar a linguagem de programação Lean 4 e as ferramentas associadas para a verificação de provas matemáticas. O Lean 4 oferece capacidades de prova matemática de correção do código e sua conformidade com a especificação, o que, no contexto do vibe-coding, permite validar que o código gerado pelo modelo de IA faz exatamente o que foi planejado.
O modelo abrange 119 bilhões de parâmetros (6,5 bilhões de parâmetros ativáveis por token), considera um contexto de 256 mil tokens e é publicado sob a licença Apache 2.0. O arquivo compactado com Leanstral ocupa 121 GB e é adequado para uso em sistemas locais. Para execução local, podem ser utilizadas as bibliotecas vllm, transformers e SGLang.
Entre outras aplicações, o modelo pode ser utilizado para vibe-development no agente open-source mistral-vibe, além de se integrar com a ferramenta Aeneas para verificação de código na linguagem Rust. Os parâmetros de entrada aceitam texto e imagens, e a saída é apenas texto. A análise de conteúdo de imagens é suportada.
Foi desenvolvido um novo conjunto de testes, FLTEval, para avaliar as capacidades dos modelos de IA em relação à qualidade da verificação formal de código e redação de provas matemáticas. Nos testes realizados, o modelo Leanstral superou consideravelmente os modelos open-source existentes Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B e GLM5 744B-A40B, e apresentou resultados semelhantes aos modelos Claude Haiku 4.5 e Claude Sonnet 4.6 da Anthropic, mas ficou atrás do modelo Claude Opus 4.6. Em particular, o modelo Opus obteve 39,6 pontos, enquanto o Leanstral obteve 21,9 em uma só passagem e 31,9 em 16 passagens. Os custos associados ao uso do Opus foram de 1.650 dólares, enquanto os do Leanstral foram de 18 dólares em uma passagem e 290 dólares em 16 passagens. O modelo Haiku obteve 23 pontos com custos de 184 dólares, e o modelo Sonnet atingiu 23,7 pontos com custos de 549 dólares.
Fonte: opennet.ru
