Il nuovo modello gratuito di Mistral trova veri bug dimostrando che il codice è corretto
Mistral ha presentato Leanstral 1.5, un piccolo modello open source che scrive dimostrazioni matematiche formali e ha già trovato cinque veri bug nel codice open source.
Mistral AI ha appena presentato Leanstral 1.5, un modello gratuito che fa qualcosa di cui la maggior parte delle IA non è capace: dimostra con certezza matematica che un frammento di codice o un’affermazione matematica sia davvero corretto, non soltanto «probabilmente giusto in base agli schemi». Nel primo test reale ha già individuato cinque bug rimasti nascosti in piena vista.
Leanstral 1.5 è pensato per Lean 4, un «assistente alla dimostrazione»: immaginalo come un linguaggio di programmazione nel quale ogni affermazione deve essere logicamente inattaccabile prima che il computer la accetti. È molto diverso da un normale chatbot IA, che può sembrare sicuro pur sbagliando. Il modello è piccolo per gli standard odierni, con 6 miliardi di parametri attivi e licenza Apache 2.0, quindi chiunque può usarlo, modificarlo o eseguirlo localmente. Eppure è molto capace: «satura» miniF2F, un noto benchmark matematico, risolvendo correttamente ogni problema, e ha completato 587 dei 672 quesiti di PutnamBench, una raccolta di problemi matematici da gara notoriamente difficili.
La notizia più pratica è che Mistral ha applicato Leanstral 1.5 a 57 veri repository di codice open source e il modello ha segnalato cinque bug sconosciuti. In un esempio, varinteger, una piccola libreria per codificare numeri usata nel progetto datrs, conteneva un errore nella gestione del segno che con uno specifico valore limite provocava una corruzione silenziosa dei dati. Nessuna persona l’aveva rilevato. Il modello lo ha fatto dimostrando il comportamento del codice anziché dedurlo da esempi.
Cosa sta succedendo davvero: la maggior parte degli strumenti IA per programmare riconosce schemi. Ha letto molto codice e prevede cosa viene dopo; funziona bene quasi sempre, ma può ignorare sottili errori logici, soprattutto i casi limite come quello individuato da Leanstral. La verifica formale capovolge il metodo: non prevede, dimostra. Storicamente è stata un’attività lenta riservata agli esperti. Un modello gratuito, aperto e da 6 miliardi di parametri che la svolge abbastanza bene da trovare bug reali indica che questa nicchia sta diventando accessibile e non resterà confinata nei laboratori accademici.
Cosa significa per te: se sei soltanto curioso dell’IA, non devi usarlo: è uno strumento specialistico, come una chiave dinamometrica, non un martello. Se programmi professionalmente, soprattutto software critico per sicurezza o incolumità come librerie crittografiche, parser e sistemi integrati, merita attenzione: è gratuito, funziona senza inviare il codice a un’API cloud e ha già dimostrato di rilevare ciò che la revisione umana non ha visto. Per la programmazione quotidiana, i tuoi strumenti attuali restano adatti; questo serve quando «probabilmente corretto» non basta.
Fonti
È uscita la grande pagella annuale sull'IA di Stanford e il divario di fiducia aumenta
L'AI Index 2026 di Stanford HAI mostra rapidi progressi nelle capacità insieme all'aumento degli incidenti di sicurezza, al calo della trasparenza e a un crescente divario di fiducia tra esperti e pubblico.
