L'azienda Mistral AI ha presentato un ampio modello linguistico chiamato Devstral, concepito per lo 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 di non limitarsi a generare codice, ma anche di garantire che esso sia privo di errori.
Devstral è stato il primo modello open-source a supportare il linguaggio di programmazione Lean 4 e gli strumenti associati per la verifica delle dimostrazioni matematiche. Lean 4 offre funzionalità per la dimostrazione matematica della correttezza del codice e della sua conformità alle specifiche, permettendo nel contesto del vibe-coding di confermare che il codice generato dal modello AI faccia esattamente ciò che è stato progettato.
Il modello comprende 119 miliardi di parametri (6,5 miliardi di parametri attivabili per token), tiene conto di un contesto di 256.000 token ed è stato pubblicato con licenza Apache 2.0. L'archivio scaricabile di Leanstral occupa 121 GB ed è adatto per l'uso su sistemi locali. Si possono utilizzare le librerie vllm, transformers e SGLang per l'esecuzione locale.
Tra le altre cose, il modello può essere utilizzato per lo sviluppo vibe nell'agente open-source mistral-vibe, e integrarsi con gli strumenti Aeneas per la verifica del codice in Rust. I parametri di ingresso possono essere testo e immagini, mentre l'output è solo testuale. È supportata l'analisi del contenuto delle immagini.
È stato sviluppato un nuovo insieme di test chiamato FLTEval per valutare le capacità dei modelli AI in relazione alla qualità della verifica formale del codice e alla stesura di dimostrazioni matematiche. Nei test condotti, il modello Leanstral ha superato significativamente i modelli open-source esistenti Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B e GLM5 744B-A40B, mostrando risultati comparabili con i modelli Claude Haiku 4.5 e Claude Sonnet 4.6 di Anthropic, ma risultando inferiore al modello Claude Opus 4.6. In particolare, il modello Opus ha ottenuto 39,6 punti, mentre Leanstral ha totalizzato 21,9 in un singolo passaggio e 31,9 in 16 passaggi. Inoltre, i costi per l'uso di Opus ammontano a 1650 dollari, rispetto a $18 per Leanstral in un passaggio e $290 in 16 passaggi. Il modello Haiku ha ottenuto 23 punti con costi di $184, mentre il modello Sonnet ha totalizzato 23,7 con costi di $549.
Fonte: opennet.ru
