Leanstral 1.5, il modello aperto di Mistral che dimostra teoremi e trova bug reali nel codice

Nel dibattito sull’intelligenza artificiale si parla in continuazione di modelli che scrivono testi, generano immagini o completano codice. Molto più raramente si parla di modelli capaci di dimostrare che qualcosa è corretto. Eppure è proprio qui che si decide una parte enorme dell’affidabilità del software e della matematica applicata. Il laboratorio francese Mistral ha rilasciato Leanstral 1.5, un modello aperto costruito per la verifica formale con Lean 4, il linguaggio con cui si scrivono dimostrazioni che una macchina può controllare riga per riga, senza margine di interpretazione.

Il dato che ha fatto discutere è duplice. Da un lato Leanstral 1.5 ha raggiunto il 100% su miniF2F, un benchmark di matematica formale che va dai problemi delle scuole superiori fino alle olimpiadi. Dall’altro, cosa forse più concreta, ha individuato cinque bug mai segnalati prima analizzando decine di repository open source reali.

Se sviluppi software, fai ricerca o semplicemente segui da vicino l’evoluzione dell’AI, ti conviene capire perché un modello del genere è diverso dai soliti assistenti di programmazione.

Che cosa è Leanstral 1.5 e perché la verifica formale conta

Per capire Leanstral 1.5 devi partire da Lean 4. Si tratta di un assistente di dimostrazione, cioè un ambiente in cui un teorema matematico, oppure la correttezza di un pezzo di codice, viene espresso in un linguaggio rigoroso e poi verificato in modo automatico. Se la dimostrazione contiene un errore, Lean la rifiuta. Non esistono zone grigie: o la prova regge, o non regge.

Questo approccio si chiama verifica formale ed è lo standard più alto di garanzia che l’informatica conosca. Viene usato dove un errore costa carissimo, ad esempio nei sistemi crittografici, nei protocolli di rete, nel software aeronautico e negli smart contract che gestiscono valore sulla blockchain. Il problema storico è che scrivere queste dimostrazioni a mano è lentissimo e richiede competenze molto specialistiche, quindi resta confinato a pochi progetti critici.

È qui che entra un modello come Leanstral 1.5. Il suo compito non è chiacchierare, ma generare dimostrazioni valide in Lean 4, proponendo i passaggi logici che portano dalla premessa alla conclusione e correggendosi quando il verificatore respinge un tentativo. In pratica trasforma un lavoro da specialisti in qualcosa di molto più accessibile.

Gli addetti ai lavori parlano di proof engineering, l’ingegneria delle dimostrazioni. È una disciplina giovane, e un modello capace di reggerne il peso la avvicina di colpo a un pubblico molto più ampio di ricercatori e sviluppatori.

La differenza rispetto a un normale assistente di codice

Un assistente generalista che scrive codice può sbagliare, e spesso lo fa in modo invisibile, perché il testo prodotto sembra corretto anche quando non lo è. Con la verifica formale il controllo diventa oggettivo: ogni passaggio viene validato dal sistema. Questo cambia la natura stessa dell’errore, che non resta nascosto ma emerge subito, nel momento in cui il verificatore boccia la prova.

Per questo l’unione tra grandi modelli linguistici e strumenti come Lean è considerata una delle strade più promettenti per ottenere un’AI davvero affidabile, e non soltanto convincente.

I numeri: 100% su miniF2F e 587 problemi Putnam risolti

Sul fronte dei benchmark i risultati dichiarati da Mistral sono notevoli. Leanstral 1.5 tocca il 100% su miniF2F, la raccolta di problemi che serve da riferimento per misurare la capacità di dimostrazione formale. Ancora più impegnativo è PutnamBench, costruito sui problemi della celebre competizione universitaria Putnam: qui il modello ha risolto 587 dei 672 problemi disponibili.

Il confronto sui costi è forse l’aspetto più interessante per chi ragiona in termini pratici. Secondo le stime di Mistral, ogni soluzione su PutnamBench costa circa 4 dollari con Leanstral 1.5, contro i circa 300 dollari di Seed-Prover 1.5 e i circa 60 dollari di Aleph Prover.

Non è un dettaglio da poco. Un ordine di grandezza di differenza sul costo significa poter usare il modello su volumi molto più ampi, ad esempio per verificare intere basi di codice invece di affrontare singoli problemi isolati. Quando una capacità diventa economica, cambia il modo in cui la si usa.

Cinque bug scoperti nel software open source

I benchmark raccontano una parte della storia, ma il risultato che rende Leanstral 1.5 concreto è un altro. Analizzando 57 repository open source, il modello ha scovato cinque bug fino a quel momento sconosciuti. Non si tratta di errori teorici, ma di problemi reali dentro codice che qualcuno stava già usando.

Questo è il punto in cui la verifica formale smette di essere un esercizio da laboratorio e diventa uno strumento di lavoro. Un modello che dimostra teoremi può anche dimostrare che una funzione rispetta sempre le sue specifiche, oppure trovare il caso limite in cui quella garanzia salta.

Il parallelo con la sicurezza è immediato. Trovare un bug prima che finisca in produzione vale molto più che correggerlo dopo un incidente. Ed è la stessa logica che guida diversi strumenti recenti pensati per irrobustire il software prodotto con l’AI, dagli agenti di coding open source fino agli assistenti che scrivono codice dal terminale. La differenza è che Leanstral non si limita a produrre codice, ma ne certifica la correttezza.

Un modello aperto con licenza Apache 2.0

Uno degli aspetti più rilevanti di Leanstral 1.5 è il modo in cui viene distribuito. Il modello è a pesi aperti e rilasciato con licenza Apache 2.0, la stessa formula che consente di scaricarlo, modificarlo e usarlo anche in contesti commerciali senza i vincoli tipici dei modelli proprietari di frontiera.

Sul piano tecnico Leanstral 1.5 adotta un’architettura a esperti, con 119 miliardi di parametri complessivi ma soltanto 6,5 miliardi attivi per ogni token elaborato. In questo modo unisce la capacità di un modello grande a un costo di esecuzione più contenuto. La finestra di contesto arriva a 256.000 token, spazio sufficiente per ragionare su dimostrazioni lunghe e articolate senza perdere il filo.

La scelta dell’apertura non è casuale. Mistral ha seguito la stessa strada con Shieldstral, il suo classificatore di sicurezza distribuito in forma aperta, e più in generale l’ecosistema open sta diventando il terreno su cui laboratori diversi si sfidano. Per un laboratorio europeo, puntare sull’apertura è anche un modo per differenziarsi dai giganti americani che tengono chiusi i loro modelli migliori.

Per chi sviluppa, un modello aperto specializzato nella verifica formale significa poter integrare controlli di correttezza dentro i propri strumenti, senza dipendere da un’API esterna e senza esporre codice sensibile a terzi. È una differenza che pesa parecchio in tutti i settori in cui la riservatezza del software non è negoziabile.

Perché tenere d’occhio l’AI che dimostra

Leanstral 1.5 non è un assistente che userai per rispondere a un’email o riassumere un documento. È un tassello di una tendenza più profonda, quella che punta a rendere l’intelligenza artificiale non solo capace, ma verificabile. In un momento in cui si discute molto di allucinazioni e di output inaffidabili, un modello che produce dimostrazioni controllabili in automatico indica una direzione diversa e più solida.

La matematica e la verifica del software sono solo il primo campo di applicazione. La stessa idea, generare qualcosa e poi provarne la correttezza in modo rigoroso, può estendersi a molti altri ambiti in cui oggi ci fidiamo dell’AI senza avere garanzie reali.

Se vuoi capire dove sta andando l’intelligenza artificiale applicata al codice e alla ricerca, tieni d’occhio questa famiglia di strumenti e prova a immaginare come la verifica formale potrebbe entrare nei tuoi flussi di lavoro. Continua a seguirci per restare aggiornato sui prossimi modelli aperti e sulle loro applicazioni concrete.