L'azienda Mistral AI ha presentato un grande modello linguistico chiamato Devstral, mirato all'uso nello sviluppo di applicazioni (vibe-coding) e ottimizzato per la verifica formale del codice. Si prevede che Devstral possa essere utilizzato per creare assistenti AI in grado non solo di generare codice, ma anche di garantire l'assenza di errori.
Devstral è diventato il primo modello open source a supportare il linguaggio di programmazione Lean 4 e il relativo insieme di strumenti per la verifica delle dimostrazioni matematiche. Lean 4 offre capacità per la dimostrazione matematica della correttezza del codice e la sua conformità alle specifiche, il che, nel contesto del vibe-coding, consente di confermare che il codice generato dal modello AI fa esattamente ciò che è previsto.
Il modello copre 119 miliardi di parametri (6,5 miliardi di parametri attivati per token), considera un contesto di 256 mila token ed è pubblicato sotto licenza Apache 2.0. L'archivio scaricabile di Leanstral occupa 121 GB ed è appropriato per l'uso su sistemi locali. Per l'esecuzione locale possono essere utilizzate le librerie vllm, transformers e SGLang.
Tra le altre cose, il modello può essere utilizzato per lo sviluppo vibe nell'agente open mistral-vibe e può anche essere integrato con gli strumenti Aeneas per la verifica del codice in Rust. I parametri di input accettano testo e immagini, mentre in output viene restituito solo testo. È supportata l'analisi del contenuto delle immagini.
Per valutare le capacità dei modelli AI in base alla qualità della verifica formale del codice e della scrittura di dimostrazioni matematiche, è stato sviluppato un nuovo insieme di test chiamato FLTEval. Nei test condotti, il modello Leanstral ha significativamente superato i modelli open source esistenti come Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B e GLM5 744B-A40B, mostrando risultati simili ai modelli Claude Haiku 4.5 e Claude Sonnet 4.6 della società Anthropic, ma è rimasto indietro rispetto al modello Claude Opus 4.6. In particolare, il modello Opus ha ottenuto 39,6 punti, mentre Leanstral ha ottenuto 21,9 in un passaggio e 31,9 in 16 passaggi. Le spese per l'uso di Opus ammontano a 1650 dollari, mentre Leanstral costa $18 per un passaggio e $290 per 16 passaggi. Il modello Haiku ha ottenuto 23 punti con spese di $184, e il modello Sonnet ha ottenuto 23,7 punti con spese di $549.
Fonte: opennet.ru
