Mistral AI ha rilasciato Leanstral 1.5, un modello open source specializzato nella produzione e nella verifica di dimostrazioni formali in Lean 4, il proof assistant utilizzato per rappresentare teoremi matematici e proprietà logiche del software in una forma controllabile automaticamente dal compilatore. Il modello è pensato quindi per un tipo di lavoro molto diverso dalla generazione tradizionale di codice: non deve soltanto proporre una soluzione plausibile, ma costruire prove che possano essere accettate da un sistema formale e trasformate in garanzie verificabili.
Leanstral 1.5 è basato sulla famiglia Mistral Small 4 e utilizza un’architettura Mixture of Experts con 119 miliardi di parametri complessivi. Per ogni token vengono attivati solo alcuni esperti, portando il numero di parametri effettivamente utilizzati a circa 6,5 miliardi. Questa struttura consente di mantenere una capacità elevata sul ragionamento formale senza sostenere il costo computazionale di un modello denso di pari dimensioni. Supporta inoltre un contesto fino a 256.000 token, con input testuali e visivi e output testuale.
L’addestramento combina mid-training, supervised fine-tuning e reinforcement learning basato su CISPO. La parte più rilevante riguarda gli ambienti di apprendimento: nel primo il modello riceve l’enunciato di un teorema, genera una prova, riceve il feedback del compilatore Lean e modifica la strategia finché non ottiene una verifica valida oppure esaurisce il budget disponibile. Nel secondo lavora come un agente di sviluppo all’interno di un file system, modifica file, esegue comandi Bash e consulta il Lean Language Server per leggere errori, obiettivi intermedi e informazioni sui tipi. In questo modo può intervenire su dimostrazioni incomplete, creare lemmi ausiliari e mantenere una traiettoria di lavoro più lunga rispetto alla semplice generazione one-shot.
Nei benchmark formali il modello ha raggiunto il 100% su miniF2F, ha risolto 587 dei 672 problemi di PutnamBench e ha ottenuto nuovi risultati di riferimento su FATE-H, con l’87%, e FATE-X, con il 34%. Sul benchmark FLTEval, costruito a partire da pull request del repository relativo al Teorema di Fermat, Leanstral 1.5 ha migliorato il Pass@1 dal 21,9% al 28,9% e il Pass@8 dal 31,9% al 43,2%.
Uno degli aspetti più interessanti riguarda il test-time scaling. Quando aumenta il budget di token assegnato al ragionamento, cresce anche il numero di problemi risolti: su PutnamBench il modello passa da 44 soluzioni con 50.000 token a 244 con 200.000 token, 493 con un milione e 587 con quattro milioni di token. Il tempo di inferenza non viene quindi usato soltanto per produrre risposte più lunghe, ma per eseguire cicli ripetuti di tentativo, compilazione, correzione e verifica.
Leanstral 1.5 è stato impiegato anche nella verifica di codice Rust attraverso l’integrazione con Aeneas, strumento che traduce componenti Rust in rappresentazioni utilizzabili in Lean. Su 57 repository open source il sistema ha individuato 47 violazioni di proprietà, delle quali 11 confermate come bug reali. Cinque non risultavano precedentemente segnalate su GitHub. Tra i casi emersi c’è un problema di overflow nella funzione di decodifica Zigzag della libreria datrs/varinteger: per valori interi a 64 bit, l’operazione value + 1 poteva superare il limite numerico, causando l’interruzione del programma in debug oppure possibili alterazioni dei dati in release.
Il modello viene distribuito con licenza Apache 2.0, disponibile su Hugging Face e tramite API gratuita di Mistral. L’obiettivo non è sostituire il lavoro del matematico o del software engineer, ma rendere più accessibile una verifica formale che fino a oggi richiedeva competenze specialistiche e tempi elevati. In ambiti dove un errore logico può propagarsi in sistemi critici, contratti software, protocolli o librerie di base, un agente capace di trasformare requisiti in proprietà verificabili può diventare uno strumento concreto di controllo della qualità.