Physical Address
304 North Cardinal St.
Dorchester Center, MA 02124
Non è più un esercizio teorico confinato ai paper accademici: la verifica formale tramite intelligenza artificiale dimostra di saper mettere le mani sul codice vero e stanare falle sfuggite per anni ai controlli umani. Mistral AI ha rilasciato oggi Leanstral 1.5, un modello open-source specializzato nel linguaggio Lean 4, capace di eccellere nelle competizioni matematiche più complesse e, parallelamente, di individuare vulnerabilità in software open-source ampiamente utilizzati.
Il salto di qualità è doppio: si passa dalla dimostrazione di teoremi alla caccia ai bug in produzione, il tutto con una licenza Apache 2.0 che ne agevola l’adozione senza vincoli.
Performance da record sui benchmark matematici
Leanstral 1.5 raggiunge il 100% sul benchmark miniF2F, che spazia da problemi di livello scolastico fino alle olimpiadi di matematica. Su PutnamBench, la prestigiosa competizione matematica universitaria, il modello risolve 587 dei 672 problemi totali.
Nel campo dell’algebra avanzata, i risultati restano da vertice assoluto tra i modelli open-source:
- FATE-H: 87%, benchmark che testa compiti di livello magistrale in teoria dei gruppi e degli anelli.
- FATE-X: 34%, dedicato a compiti di difficoltà dottorale.
Solo il modello closed-source Aleph Prover riesce a superare Leanstral 1.5 su PutnamBench, posizionandosi come unica alternativa proprietaria con performance superiori.
Dalla matematica al codice reale: 5 bug scovati in poche ore
L’impatto più concreto del modello riguarda la sicurezza informatica. Durante un test pratico di verifica del codice, Leanstral 1.5 ha scansionato 57 repository open-source e ha scovato 5 bug precedentemente sconosciuti.
Tra questi, è emerso un bug di overflow nella libreria Rust varinteger, un errore che era sfuggito al controllo della comunità di sviluppatori. La capacità di navigare il codice e applicare il rigore della verifica formale in un contesto reale, e non simulato, segna un punto di svolta per l’automazione della cybersecurity.
Architettura e disponibilità
L’architettura del modello bilancia potenza ed efficienza. Sebbene Leanstral 1.5 conti 119 miliardi di parametri totali, utilizza un design mixture-of-experts che ne attiva soltanto 6,5 miliardi durante l’inferenza. Questo consente di mantenere i costi computazionali relativamente bassi nonostante le elevate prestazioni.
Il processo di addestramento ha combinato mid-training, supervised fine-tuning e reinforcement learning. Il modello è immediatamente disponibile su Hugging Face e tramite un’API gratuita.
La combinazione tra licenza aperta e basso costo di inferenza cambia le carte in tavola per startup e aziende. Mentre i benchmark di algebra dottorale (FATE-X al 34%) mostrano che c’è ancora strada da fare ai confini della ricerca pura, la quota di problemi risolti su PutnamBench (87%) e il 100% su miniF2F rendono il modello già spendibile in contesti di automazione industriale. Con soli 6,5 miliardi di parametri attivi, la verifica formale di massa diventa economicamente accessibile senza dover ricorrere a cluster cloud proibitivi.
Il confine tra proof-of-concept accademico e utility di sicurezza operativa si è definitivamente assottigliato: la caccia ai bug non dipende più solo dall’occhio umano, ma dalla potenza combinatoria di un’intelligenza artificiale open-source che setaccia repository notte e giorno.
Fonti
